![]() |
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 353 nbn2 370 pm5.32 574 norass 1538 hadnot 1603 had0 1605 cbvexdw 2335 cbvexd 2407 rexbiOLD 3105 rexprg 4700 isocnv3 7331 suppimacnv 8161 sumodd 16335 f1omvdco3 19358 ist0cld 33099 onsuct0 35629 bj-cbvexdv 35981 wl-3xornot 36665 ifpbi1 42530 ifpbi13 42542 abciffcbatnabciffncba 45938 abciffcbatnabciffncbai 45939 ichn 46423 |
Copyright terms: Public domain | W3C validator |