Metamath Proof Explorer


Theorem impl

Description: Export a wff from a left conjunct. (Contributed by Mario Carneiro, 9-Jul-2014)

Ref Expression
Hypothesis impl.1 φψχθ
Assertion impl φψχθ

Proof

Step Hyp Ref Expression
1 impl.1 φψχθ
2 1 expd φψχθ
3 2 imp31 φψχθ