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 ( ( 𝜑 → ( ( 𝜓𝜒 ) → 𝜃 ) ) ↔ ( 𝜑 → ( 𝜒 → ( 𝜓𝜃 ) ) ) )