![]() |
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 317 | . 2 ⊢ ((𝜑 ↔ 𝜓) → (¬ 𝜑 ↔ ¬ 𝜓)) |
3 | id 22 | . . 3 ⊢ ((¬ 𝜑 ↔ ¬ 𝜓) → (¬ 𝜑 ↔ ¬ 𝜓)) | |
4 | 3 | con4bid 316 | . 2 ⊢ ((¬ 𝜑 ↔ ¬ 𝜓) → (𝜑 ↔ 𝜓)) |
5 | 2, 4 | impbii 208 | 1 ⊢ ((𝜑 ↔ 𝜓) ↔ (¬ 𝜑 ↔ ¬ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 |
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 206 |
This theorem is referenced by: notbii 319 con4bii 320 con2bi 352 nbn2 369 pm5.32 572 norass 1531 hadnot 1596 had0 1598 cbvexdw 2330 cbvexd 2402 rexbiOLD 3095 rexprg 4705 isocnv3 7344 suppimacnv 8188 sumodd 16390 f1omvdco3 19447 ist0cld 33648 onsuct0 36153 bj-cbvexdv 36505 wl-3xornot 37188 ifpbi1 43144 ifpbi13 43156 abciffcbatnabciffncba 46544 abciffcbatnabciffncbai 46545 ichn 47028 |
Copyright terms: Public domain | W3C validator |