Metamath Proof Explorer


Theorem expd

Description: Exportation deduction. (Contributed by NM, 20-Aug-1993) (Proof shortened by Wolf Lammen, 28-Jul-2022)

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

Proof

Step Hyp Ref Expression
1 expd.1 φ ψ χ θ
2 1 expdcom ψ χ φ θ
3 2 com3r φ ψ χ θ