Metamath Proof Explorer


Theorem exp41

Description: An exportation inference. (Contributed by NM, 26-Apr-1994)

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

Proof

Step Hyp Ref Expression
1 exp41.1 φψχθτ
2 1 ex φψχθτ
3 2 exp31 φψχθτ