Metamath Proof Explorer


Theorem expcomd

Description: Deduction form of expcom . (Contributed by Alan Sare, 22-Jul-2012)

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

Proof

Step Hyp Ref Expression
1 expcomd.1 φψχθ
2 1 expd φψχθ
3 2 com23 φχψθ