Metamath Proof Explorer

Theorem jcab

Description: Distributive law for implication over conjunction. Compare Theorem *4.76 of WhiteheadRussell p. 121. (Contributed by NM, 3-Apr-1994) (Proof shortened by Wolf Lammen, 27-Nov-2013)

Ref Expression
Assertion jcab ⊢ φ → ψ ∧ χ ↔ φ → ψ ∧ φ → χ

Proof

Step Hyp Ref Expression
1 simpl ⊢ ψ ∧ χ → ψ
2 1 imim2i ⊢ φ → ψ ∧ χ → φ → ψ
3 simpr ⊢ ψ ∧ χ → χ
4 3 imim2i ⊢ φ → ψ ∧ χ → φ → χ
5 2 4 jca ⊢ φ → ψ ∧ χ → φ → ψ ∧ φ → χ
6 pm3.43 ⊢ φ → ψ ∧ φ → χ → φ → ψ ∧ χ
7 5 6 impbii ⊢ φ → ψ ∧ χ ↔ φ → ψ ∧ φ → χ