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

Metamath Proof Explorer

Theorem dedth3h

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

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

Proof

Step Hyp Ref Expression
1 dedth3h.1 ⊢ A = if φ A D → θ ↔ τ
2 dedth3h.2 ⊢ B = if ψ B R → τ ↔ η
3 dedth3h.3 ⊢ C = if χ C S → η ↔ ζ
4 dedth3h.4 ⊢ ζ
5 1 imbi2d ⊢ A = if φ A D → ψ ∧ χ → θ ↔ ψ ∧ χ → τ
6 2 3 4 dedth2h ⊢ ψ ∧ χ → τ
7 5 6 dedth ⊢ φ → ψ ∧ χ → θ
8 7 3impib ⊢ φ ∧ ψ ∧ χ → θ