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

Metamath Proof Explorer

Theorem keephyp2v

Description: Keep a hypothesis containing 2 class variables (for use with the weak deduction theorem dedth ). (Contributed by NM, 16-Apr-2005)

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

Proof

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