Description: Biconditional form of expcomd . (Contributed by Alan Sare, 22-Jul-2012) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | expcomdg | ⊢ ( ( 𝜑 → ( ( 𝜓 ∧ 𝜒 ) → 𝜃 ) ) ↔ ( 𝜑 → ( 𝜒 → ( 𝜓 → 𝜃 ) ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ancomst | ⊢ ( ( ( 𝜓 ∧ 𝜒 ) → 𝜃 ) ↔ ( ( 𝜒 ∧ 𝜓 ) → 𝜃 ) ) | |
2 | impexp | ⊢ ( ( ( 𝜒 ∧ 𝜓 ) → 𝜃 ) ↔ ( 𝜒 → ( 𝜓 → 𝜃 ) ) ) | |
3 | 1 2 | bitri | ⊢ ( ( ( 𝜓 ∧ 𝜒 ) → 𝜃 ) ↔ ( 𝜒 → ( 𝜓 → 𝜃 ) ) ) |
4 | 3 | imbi2i | ⊢ ( ( 𝜑 → ( ( 𝜓 ∧ 𝜒 ) → 𝜃 ) ) ↔ ( 𝜑 → ( 𝜒 → ( 𝜓 → 𝜃 ) ) ) ) |