Metamath Proof Explorer


Theorem expdcom

Description: Commuted form of expd . (Contributed by Alan Sare, 18-Mar-2012) Shorten expd . (Revised by Wolf Lammen, 28-Jul-2022)

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

Proof

Step Hyp Ref Expression
1 expd.1 φ ψ χ θ
2 1 com12 ψ χ φ θ
3 2 ex ψ χ φ θ