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

Metamath Proof Explorer

Theorem dedth3v

Description: Weak deduction theorem for eliminating a hypothesis with 3 class variables. See comments in dedth2v . (Contributed by NM, 13-Aug-1999) (Proof shortened by Eric Schmidt, 28-Jul-2009)

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

Proof

Step Hyp Ref Expression
1 dedth3v.1 ⊢ A = if φ A D → ψ ↔ χ
2 dedth3v.2 ⊢ B = if φ B R → χ ↔ θ
3 dedth3v.3 ⊢ C = if φ C S → θ ↔ τ
4 dedth3v.4 ⊢ τ
5 1 2 3 4 dedth3h ⊢ φ ∧ φ ∧ φ → ψ
6 5 3anidm12 ⊢ φ ∧ φ → ψ
7 6 anidms ⊢ φ → ψ