Metamath Proof Explorer

Theorem pm5.32dav

Description: Distribution of implication over biconditional (deduction form). Variant of pm5.32da . (Contributed by Zhi Wang, 30-Aug-2024)

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

Proof

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