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

Proof

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