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

Metamath Proof Explorer

Theorem elimhyp3v

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

Ref Expression
Hypotheses elimhyp3v.1 ⊢ A = if φ A D → φ ↔ χ
elimhyp3v.2 ⊢ B = if φ B R → χ ↔ θ
elimhyp3v.3 ⊢ C = if φ C S → θ ↔ τ
elimhyp3v.4 ⊢ D = if φ A D → η ↔ ζ
elimhyp3v.5 ⊢ R = if φ B R → ζ ↔ σ
elimhyp3v.6 ⊢ S = if φ C S → σ ↔ τ
elimhyp3v.7 ⊢ η
Assertion elimhyp3v ⊢ τ

Proof

Step Hyp Ref Expression
1 elimhyp3v.1 ⊢ A = if φ A D → φ ↔ χ
2 elimhyp3v.2 ⊢ B = if φ B R → χ ↔ θ
3 elimhyp3v.3 ⊢ C = if φ C S → θ ↔ τ
4 elimhyp3v.4 ⊢ D = if φ A D → η ↔ ζ
5 elimhyp3v.5 ⊢ R = if φ B R → ζ ↔ σ
6 elimhyp3v.6 ⊢ S = if φ C S → σ ↔ τ
7 elimhyp3v.7 ⊢ η
8 iftrue ⊢ φ → if φ A D = A
9 8 eqcomd ⊢ φ → A = if φ A D
10 9 1 syl ⊢ φ → φ ↔ χ
11 iftrue ⊢ φ → if φ B R = B
12 11 eqcomd ⊢ φ → B = if φ B R
13 12 2 syl ⊢ φ → χ ↔ θ
14 iftrue ⊢ φ → if φ C S = C
15 14 eqcomd ⊢ φ → C = if φ C S
16 15 3 syl ⊢ φ → θ ↔ τ
17 10 13 16 3bitrd ⊢ φ → φ ↔ τ
18 17 ibi ⊢ φ → τ
19 iffalse ⊢ ¬ φ → if φ A D = D
20 19 eqcomd ⊢ ¬ φ → D = if φ A D
21 20 4 syl ⊢ ¬ φ → η ↔ ζ
22 iffalse ⊢ ¬ φ → if φ B R = R
23 22 eqcomd ⊢ ¬ φ → R = if φ B R
24 23 5 syl ⊢ ¬ φ → ζ ↔ σ
25 iffalse ⊢ ¬ φ → if φ C S = S
26 25 eqcomd ⊢ ¬ φ → S = if φ C S
27 26 6 syl ⊢ ¬ φ → σ ↔ τ
28 21 24 27 3bitrd ⊢ ¬ φ → η ↔ τ
29 7 28 mpbii ⊢ ¬ φ → τ
30 18 29 pm2.61i ⊢ τ