Metamath Proof Explorer

Theorem dedth4h

Description: Weak deduction theorem eliminating four hypotheses. See comments in dedth2h . (Contributed by NM, 16-May-1999)

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

Proof

Step Hyp Ref Expression
1 dedth4h.1 ⊢ A = if φ A R → τ ↔ η
2 dedth4h.2 ⊢ B = if ψ B S → η ↔ ζ
3 dedth4h.3 ⊢ C = if χ C F → ζ ↔ σ
4 dedth4h.4 ⊢ D = if θ D G → σ ↔ ρ
5 dedth4h.5 ⊢ ρ
6 1 imbi2d ⊢ A = if φ A R → χ ∧ θ → τ ↔ χ ∧ θ → η
7 2 imbi2d ⊢ B = if ψ B S → χ ∧ θ → η ↔ χ ∧ θ → ζ
8 3 4 5 dedth2h ⊢ χ ∧ θ → ζ
9 6 7 8 dedth2h ⊢ φ ∧ ψ → χ ∧ θ → τ
10 9 imp ⊢ φ ∧ ψ ∧ χ ∧ θ → τ