Metamath Proof Explorer


Theorem 3expd

Description: Exportation deduction for triple conjunction. (Contributed by NM, 26-Oct-2006)

Ref Expression
Hypothesis 3expd.1 φψχθτ
Assertion 3expd φψχθτ

Proof

Step Hyp Ref Expression
1 3expd.1 φψχθτ
2 1 com12 ψχθφτ
3 2 3exp ψχθφτ
4 3 com4r φψχθτ