Metamath Proof Explorer

Theorem imdistan

Description: Distribution of implication with conjunction. (Contributed by NM, 31-May-1999) (Proof shortened by Wolf Lammen, 6-Dec-2012)

Ref Expression
Assertion imdistan φ ψ χ φ ψ φ χ


Step Hyp Ref Expression
1 pm5.42 φ ψ χ φ ψ φ χ
2 impexp φ ψ φ χ φ ψ φ χ
3 1 2 bitr4i φ ψ χ φ ψ φ χ