Description: Two propositions are equivalent if they are both false. Closed form of 2false . Equivalent to a biimpr -like version of the xor-connective. (Contributed by Wolf Lammen, 13-May-2013)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | pm5.21im | ⊢ ( ¬ 𝜑 → ( ¬ 𝜓 → ( 𝜑 ↔ 𝜓 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nbn2 | ⊢ ( ¬ 𝜑 → ( ¬ 𝜓 ↔ ( 𝜑 ↔ 𝜓 ) ) ) | |
| 2 | 1 | biimpd | ⊢ ( ¬ 𝜑 → ( ¬ 𝜓 → ( 𝜑 ↔ 𝜓 ) ) ) |