Metamath Proof Explorer


Theorem 3expib

Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007)

Ref Expression
Hypothesis 3exp.1 φψχθ
Assertion 3expib φψχθ

Proof

Step Hyp Ref Expression
1 3exp.1 φψχθ
2 1 3exp φψχθ
3 2 impd φψχθ