Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > notbi | Structured version Visualization version GIF version |
Description: Contraposition. Theorem *4.11 of [WhiteheadRussell] p. 117. (Contributed by NM, 21-May-1994.) (Proof shortened by Wolf Lammen, 12-Jun-2013.) |
Ref | Expression |
---|---|
notbi | ⊢ ((𝜑 ↔ 𝜓) ↔ (¬ 𝜑 ↔ ¬ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . . 3 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 ↔ 𝜓)) | |
2 | 1 | notbid 321 | . 2 ⊢ ((𝜑 ↔ 𝜓) → (¬ 𝜑 ↔ ¬ 𝜓)) |
3 | id 22 | . . 3 ⊢ ((¬ 𝜑 ↔ ¬ 𝜓) → (¬ 𝜑 ↔ ¬ 𝜓)) | |
4 | 3 | con4bid 320 | . 2 ⊢ ((¬ 𝜑 ↔ ¬ 𝜓) → (𝜑 ↔ 𝜓)) |
5 | 2, 4 | impbii 212 | 1 ⊢ ((𝜑 ↔ 𝜓) ↔ (¬ 𝜑 ↔ ¬ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 209 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 210 |
This theorem is referenced by: notbii 323 con4bii 324 con2bi 357 nbn2 374 pm5.32 577 norass 1539 hadnot 1609 had0 1611 cbvexdw 2340 cbvexd 2407 rexbi 3154 vtoclgft 3458 rexprg 4598 isocnv3 7119 suppimacnv 7894 sumodd 15912 f1omvdco3 18795 ist0cld 31451 onsuct0 34316 bj-cbvexdv 34668 wl-3xornot 35338 ifpbi1 40710 ifpbi13 40722 abciffcbatnabciffncba 44039 abciffcbatnabciffncbai 44040 ichn 44524 |
Copyright terms: Public domain | W3C validator |