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

Metamath Proof Explorer

Theorem elimhyp4v

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

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

Proof

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