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 φψφχ