Metamath Proof Explorer


Theorem 3imp2

Description: Importation to right triple conjunction. (Contributed by NM, 26-Oct-2006)

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

Proof

Step Hyp Ref Expression
1 3imp1.1 φψχθτ
2 1 3impd φψχθτ
3 2 imp φψχθτ