Metamath Proof Explorer

Theorem pm5.32ri

Description: Distribution of implication over biconditional (inference form). (Contributed by NM, 12-Mar-1995)

Ref Expression
Hypothesis pm5.32i.1 ⊢ φ → ψ ↔ χ
Assertion pm5.32ri ⊢ ψ ∧ φ ↔ χ ∧ φ

Proof

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