Description: An implication and its reverse are equivalent exactly when both operands are equivalent. The right hand side resembles that of dfbi2 , but <-> is a weaker operator than /\ . Note that an implication and its reverse can never be simultaneously false, because of pm2.521 . (Contributed by Wolf Lammen, 18-Dec-2023)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | impimprbi | ⊢ ( ( 𝜑 ↔ 𝜓 ) ↔ ( ( 𝜑 → 𝜓 ) ↔ ( 𝜓 → 𝜑 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfbi2 | ⊢ ( ( 𝜑 ↔ 𝜓 ) ↔ ( ( 𝜑 → 𝜓 ) ∧ ( 𝜓 → 𝜑 ) ) ) | |
| 2 | pm5.1 | ⊢ ( ( ( 𝜑 → 𝜓 ) ∧ ( 𝜓 → 𝜑 ) ) → ( ( 𝜑 → 𝜓 ) ↔ ( 𝜓 → 𝜑 ) ) ) | |
| 3 | 1 2 | sylbi | ⊢ ( ( 𝜑 ↔ 𝜓 ) → ( ( 𝜑 → 𝜓 ) ↔ ( 𝜓 → 𝜑 ) ) ) |
| 4 | impbi | ⊢ ( ( 𝜑 → 𝜓 ) → ( ( 𝜓 → 𝜑 ) → ( 𝜑 ↔ 𝜓 ) ) ) | |
| 5 | pm2.521 | ⊢ ( ¬ ( 𝜑 → 𝜓 ) → ( 𝜓 → 𝜑 ) ) | |
| 6 | 5 | pm2.24d | ⊢ ( ¬ ( 𝜑 → 𝜓 ) → ( ¬ ( 𝜓 → 𝜑 ) → ( 𝜑 ↔ 𝜓 ) ) ) |
| 7 | 4 6 | bija | ⊢ ( ( ( 𝜑 → 𝜓 ) ↔ ( 𝜓 → 𝜑 ) ) → ( 𝜑 ↔ 𝜓 ) ) |
| 8 | 3 7 | impbii | ⊢ ( ( 𝜑 ↔ 𝜓 ) ↔ ( ( 𝜑 → 𝜓 ) ↔ ( 𝜓 → 𝜑 ) ) ) |