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

Metamath Proof Explorer

Theorem elimhyp2v

Description: Eliminate a hypothesis containing 2 class variables. (Contributed by NM, 14-Aug-1999)

Ref Expression
Hypotheses elimhyp2v.1 ⊢ ( 𝐴 = if ( 𝜑 , 𝐴 , 𝐶 ) → ( 𝜑 ↔ 𝜒 ) )
elimhyp2v.2 ⊢ ( 𝐵 = if ( 𝜑 , 𝐵 , 𝐷 ) → ( 𝜒 ↔ 𝜃 ) )
elimhyp2v.3 ⊢ ( 𝐶 = if ( 𝜑 , 𝐴 , 𝐶 ) → ( 𝜏 ↔ 𝜂 ) )
elimhyp2v.4 ⊢ ( 𝐷 = if ( 𝜑 , 𝐵 , 𝐷 ) → ( 𝜂 ↔ 𝜃 ) )
elimhyp2v.5 ⊢ 𝜏
Assertion elimhyp2v 𝜃

Proof

Step Hyp Ref Expression
1 elimhyp2v.1 ⊢ ( 𝐴 = if ( 𝜑 , 𝐴 , 𝐶 ) → ( 𝜑 ↔ 𝜒 ) )
2 elimhyp2v.2 ⊢ ( 𝐵 = if ( 𝜑 , 𝐵 , 𝐷 ) → ( 𝜒 ↔ 𝜃 ) )
3 elimhyp2v.3 ⊢ ( 𝐶 = if ( 𝜑 , 𝐴 , 𝐶 ) → ( 𝜏 ↔ 𝜂 ) )
4 elimhyp2v.4 ⊢ ( 𝐷 = if ( 𝜑 , 𝐵 , 𝐷 ) → ( 𝜂 ↔ 𝜃 ) )
5 elimhyp2v.5 ⊢ 𝜏
6 iftrue ⊢ ( 𝜑 → if ( 𝜑 , 𝐴 , 𝐶 ) = 𝐴 )
7 6 eqcomd ⊢ ( 𝜑 → 𝐴 = if ( 𝜑 , 𝐴 , 𝐶 ) )
8 7 1 syl ⊢ ( 𝜑 → ( 𝜑 ↔ 𝜒 ) )
9 iftrue ⊢ ( 𝜑 → if ( 𝜑 , 𝐵 , 𝐷 ) = 𝐵 )
10 9 eqcomd ⊢ ( 𝜑 → 𝐵 = if ( 𝜑 , 𝐵 , 𝐷 ) )
11 10 2 syl ⊢ ( 𝜑 → ( 𝜒 ↔ 𝜃 ) )
12 8 11 bitrd ⊢ ( 𝜑 → ( 𝜑 ↔ 𝜃 ) )
13 12 ibi ⊢ ( 𝜑 → 𝜃 )
14 iffalse ⊢ ( ¬ 𝜑 → if ( 𝜑 , 𝐴 , 𝐶 ) = 𝐶 )
15 14 eqcomd ⊢ ( ¬ 𝜑 → 𝐶 = if ( 𝜑 , 𝐴 , 𝐶 ) )
16 15 3 syl ⊢ ( ¬ 𝜑 → ( 𝜏 ↔ 𝜂 ) )
17 iffalse ⊢ ( ¬ 𝜑 → if ( 𝜑 , 𝐵 , 𝐷 ) = 𝐷 )
18 17 eqcomd ⊢ ( ¬ 𝜑 → 𝐷 = if ( 𝜑 , 𝐵 , 𝐷 ) )
19 18 4 syl ⊢ ( ¬ 𝜑 → ( 𝜂 ↔ 𝜃 ) )
20 16 19 bitrd ⊢ ( ¬ 𝜑 → ( 𝜏 ↔ 𝜃 ) )
21 5 20 mpbii ⊢ ( ¬ 𝜑 → 𝜃 )
22 13 21 pm2.61i ⊢ 𝜃