Metamath Proof Explorer


Theorem 3impdi

Description: Importation inference (undistribute conjunction). (Contributed by NM, 14-Aug-1995)

Ref Expression
Hypothesis 3impdi.1 φψφχθ
Assertion 3impdi φψχθ

Proof

Step Hyp Ref Expression
1 3impdi.1 φψφχθ
2 1 anandis φψχθ
3 2 3impb φψχθ