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 | |- ( -. ph -> ( -. ps -> ( ph <-> ps ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nbn2 | |- ( -. ph -> ( -. ps <-> ( ph <-> ps ) ) ) |
|
| 2 | 1 | biimpd | |- ( -. ph -> ( -. ps -> ( ph <-> ps ) ) ) |