Metamath Proof Explorer


Theorem imdistani

Description: Distribution of implication with conjunction. (Contributed by NM, 1-Aug-1994)

Ref Expression
Hypothesis imdistani.1 φ ψ χ
Assertion imdistani φ ψ φ χ

Proof

Step Hyp Ref Expression
1 imdistani.1 φ ψ χ
2 1 anc2li φ ψ φ χ
3 2 imp φ ψ φ χ