This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem keephyp3v

Description: Keep a hypothesis containing 3 class variables. (Contributed by NM, 27-Sep-1999)

Ref Expression
Hypotheses keephyp3v.1 ⊢ ( 𝐴 = if ( 𝜑 , 𝐴 , 𝐷 ) → ( 𝜌 ↔ 𝜒 ) )
keephyp3v.2 ⊢ ( 𝐵 = if ( 𝜑 , 𝐵 , 𝑅 ) → ( 𝜒 ↔ 𝜃 ) )
keephyp3v.3 ⊢ ( 𝐶 = if ( 𝜑 , 𝐶 , 𝑆 ) → ( 𝜃 ↔ 𝜏 ) )
keephyp3v.4 ⊢ ( 𝐷 = if ( 𝜑 , 𝐴 , 𝐷 ) → ( 𝜂 ↔ 𝜁 ) )
keephyp3v.5 ⊢ ( 𝑅 = if ( 𝜑 , 𝐵 , 𝑅 ) → ( 𝜁 ↔ 𝜎 ) )
keephyp3v.6 ⊢ ( 𝑆 = if ( 𝜑 , 𝐶 , 𝑆 ) → ( 𝜎 ↔ 𝜏 ) )
keephyp3v.7 ⊢ 𝜌
keephyp3v.8 ⊢ 𝜂
Assertion keephyp3v 𝜏

Proof

Step Hyp Ref Expression
1 keephyp3v.1 ⊢ ( 𝐴 = if ( 𝜑 , 𝐴 , 𝐷 ) → ( 𝜌 ↔ 𝜒 ) )
2 keephyp3v.2 ⊢ ( 𝐵 = if ( 𝜑 , 𝐵 , 𝑅 ) → ( 𝜒 ↔ 𝜃 ) )
3 keephyp3v.3 ⊢ ( 𝐶 = if ( 𝜑 , 𝐶 , 𝑆 ) → ( 𝜃 ↔ 𝜏 ) )
4 keephyp3v.4 ⊢ ( 𝐷 = if ( 𝜑 , 𝐴 , 𝐷 ) → ( 𝜂 ↔ 𝜁 ) )
5 keephyp3v.5 ⊢ ( 𝑅 = if ( 𝜑 , 𝐵 , 𝑅 ) → ( 𝜁 ↔ 𝜎 ) )
6 keephyp3v.6 ⊢ ( 𝑆 = if ( 𝜑 , 𝐶 , 𝑆 ) → ( 𝜎 ↔ 𝜏 ) )
7 keephyp3v.7 ⊢ 𝜌
8 keephyp3v.8 ⊢ 𝜂
9 iftrue ⊢ ( 𝜑 → if ( 𝜑 , 𝐴 , 𝐷 ) = 𝐴 )
10 9 eqcomd ⊢ ( 𝜑 → 𝐴 = if ( 𝜑 , 𝐴 , 𝐷 ) )
11 10 1 syl ⊢ ( 𝜑 → ( 𝜌 ↔ 𝜒 ) )
12 iftrue ⊢ ( 𝜑 → if ( 𝜑 , 𝐵 , 𝑅 ) = 𝐵 )
13 12 eqcomd ⊢ ( 𝜑 → 𝐵 = if ( 𝜑 , 𝐵 , 𝑅 ) )
14 13 2 syl ⊢ ( 𝜑 → ( 𝜒 ↔ 𝜃 ) )
15 iftrue ⊢ ( 𝜑 → if ( 𝜑 , 𝐶 , 𝑆 ) = 𝐶 )
16 15 eqcomd ⊢ ( 𝜑 → 𝐶 = if ( 𝜑 , 𝐶 , 𝑆 ) )
17 16 3 syl ⊢ ( 𝜑 → ( 𝜃 ↔ 𝜏 ) )
18 11 14 17 3bitrd ⊢ ( 𝜑 → ( 𝜌 ↔ 𝜏 ) )
19 7 18 mpbii ⊢ ( 𝜑 → 𝜏 )
20 iffalse ⊢ ( ¬ 𝜑 → if ( 𝜑 , 𝐴 , 𝐷 ) = 𝐷 )
21 20 eqcomd ⊢ ( ¬ 𝜑 → 𝐷 = if ( 𝜑 , 𝐴 , 𝐷 ) )
22 21 4 syl ⊢ ( ¬ 𝜑 → ( 𝜂 ↔ 𝜁 ) )
23 iffalse ⊢ ( ¬ 𝜑 → if ( 𝜑 , 𝐵 , 𝑅 ) = 𝑅 )
24 23 eqcomd ⊢ ( ¬ 𝜑 → 𝑅 = if ( 𝜑 , 𝐵 , 𝑅 ) )
25 24 5 syl ⊢ ( ¬ 𝜑 → ( 𝜁 ↔ 𝜎 ) )
26 iffalse ⊢ ( ¬ 𝜑 → if ( 𝜑 , 𝐶 , 𝑆 ) = 𝑆 )
27 26 eqcomd ⊢ ( ¬ 𝜑 → 𝑆 = if ( 𝜑 , 𝐶 , 𝑆 ) )
28 27 6 syl ⊢ ( ¬ 𝜑 → ( 𝜎 ↔ 𝜏 ) )
29 22 25 28 3bitrd ⊢ ( ¬ 𝜑 → ( 𝜂 ↔ 𝜏 ) )
30 8 29 mpbii ⊢ ( ¬ 𝜑 → 𝜏 )
31 19 30 pm2.61i ⊢ 𝜏