Metamath Proof Explorer


Theorem exp4a

Description: An exportation inference. (Contributed by NM, 26-Apr-1994) (Proof shortened by Wolf Lammen, 20-Jul-2021)

Ref Expression
Hypothesis exp4a.1 φψχθτ
Assertion exp4a φψχθτ

Proof

Step Hyp Ref Expression
1 exp4a.1 φψχθτ
2 1 imp φψχθτ
3 2 exp4b φψχθτ