Metamath Proof Explorer


Theorem expcomdg

Description: Biconditional form of expcomd . (Contributed by Alan Sare, 22-Jul-2012) (New usage is discouraged.)

Ref Expression
Assertion expcomdg φ ψ χ θ φ χ ψ θ

Proof

Step Hyp Ref Expression
1 ancomst ψ χ θ χ ψ θ
2 impexp χ ψ θ χ ψ θ
3 1 2 bitri ψ χ θ χ ψ θ
4 3 imbi2i φ ψ χ θ φ χ ψ θ