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

Metamath Proof Explorer

Theorem keephyp3v

Description: Keep a hypothesis containing 3 class variables. (Contributed by NM, 27-Sep-1999)

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

Proof

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