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

Metamath Proof Explorer

Theorem dedth2h

Description: Weak deduction theorem eliminating two hypotheses. This theorem is simpler to use than dedth2v but requires that each hypothesis have exactly one class variable. See also comments in dedth . (Contributed by NM, 15-May-1999)

Ref Expression
Hypotheses dedth2h.1 ⊢ A = if φ A C → χ ↔ θ
dedth2h.2 ⊢ B = if ψ B D → θ ↔ τ
dedth2h.3 ⊢ τ
Assertion dedth2h ⊢ φ ∧ ψ → χ

Proof

Step Hyp Ref Expression
1 dedth2h.1 ⊢ A = if φ A C → χ ↔ θ
2 dedth2h.2 ⊢ B = if ψ B D → θ ↔ τ
3 dedth2h.3 ⊢ τ
4 1 imbi2d ⊢ A = if φ A C → ψ → χ ↔ ψ → θ
5 2 3 dedth ⊢ ψ → θ
6 4 5 dedth ⊢ φ → ψ → χ
7 6 imp ⊢ φ ∧ ψ → χ