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 ⊢ A = if φ A C → ψ ↔ χ
keephyp2v.2 ⊢ B = if φ B D → χ ↔ θ
keephyp2v.3 ⊢ C = if φ A C → τ ↔ η
keephyp2v.4 ⊢ D = if φ B D → η ↔ θ
keephyp2v.5 ⊢ ψ
keephyp2v.6 ⊢ τ
Assertion keephyp2v ⊢ θ

Proof

Step Hyp Ref Expression
1 keephyp2v.1 ⊢ A = if φ A C → ψ ↔ χ
2 keephyp2v.2 ⊢ B = if φ B D → χ ↔ θ
3 keephyp2v.3 ⊢ C = if φ A C → τ ↔ η
4 keephyp2v.4 ⊢ D = if φ B D → η ↔ θ
5 keephyp2v.5 ⊢ ψ
6 keephyp2v.6 ⊢ τ
7 iftrue ⊢ φ → if φ A C = A
8 7 eqcomd ⊢ φ → A = if φ A C
9 8 1 syl ⊢ φ → ψ ↔ χ
10 iftrue ⊢ φ → if φ B D = B
11 10 eqcomd ⊢ φ → B = if φ B D
12 11 2 syl ⊢ φ → χ ↔ θ
13 9 12 bitrd ⊢ φ → ψ ↔ θ
14 5 13 mpbii ⊢ φ → θ
15 iffalse ⊢ ¬ φ → if φ A C = C
16 15 eqcomd ⊢ ¬ φ → C = if φ A C
17 16 3 syl ⊢ ¬ φ → τ ↔ η
18 iffalse ⊢ ¬ φ → if φ B D = D
19 18 eqcomd ⊢ ¬ φ → D = if φ B D
20 19 4 syl ⊢ ¬ φ → η ↔ θ
21 17 20 bitrd ⊢ ¬ φ → τ ↔ θ
22 6 21 mpbii ⊢ ¬ φ → θ
23 14 22 pm2.61i ⊢ θ