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 ⊢ φ → ψ ∧ χ → θ ↔ φ → χ → ψ → θ