Metamath Proof Explorer

Theorem pm5.32rd

Description: Distribution of implication over biconditional (deduction form). (Contributed by NM, 25-Dec-2004)

Ref Expression
Hypothesis pm5.32d.1 ⊢ φ → ψ → χ ↔ θ
Assertion pm5.32rd ⊢ φ → χ ∧ ψ ↔ θ ∧ ψ

Proof

Step Hyp Ref Expression
1 pm5.32d.1 ⊢ φ → ψ → χ ↔ θ
2 1 pm5.32d ⊢ φ → ψ ∧ χ ↔ ψ ∧ θ
3 ancom ⊢ χ ∧ ψ ↔ ψ ∧ χ
4 ancom ⊢ θ ∧ ψ ↔ ψ ∧ θ
5 2 3 4 3bitr4g ⊢ φ → χ ∧ ψ ↔ θ ∧ ψ