Metamath Proof Explorer

Theorem pm5.3

Description: Theorem *5.3 of WhiteheadRussell p. 125. (Contributed by NM, 3-Jan-2005) (Proof shortened by Andrew Salmon, 7-May-2011)

Ref Expression
Assertion pm5.3 ⊢ φ ∧ ψ → χ ↔ φ ∧ ψ → φ ∧ χ

Proof

Step Hyp Ref Expression
1 simpl ⊢ φ ∧ ψ → φ
2 1 biantrurd ⊢ φ ∧ ψ → χ ↔ φ ∧ χ
3 2 pm5.74i ⊢ φ ∧ ψ → χ ↔ φ ∧ ψ → φ ∧ χ