MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  notbi Structured version   Visualization version   GIF version

Theorem notbi 318
Description: Contraposition. Theorem *4.11 of [WhiteheadRussell] p. 117. (Contributed by NM, 21-May-1994.) (Proof shortened by Wolf Lammen, 12-Jun-2013.)
Assertion
Ref Expression
notbi ((𝜑𝜓) ↔ (¬ 𝜑 ↔ ¬ 𝜓))

Proof of Theorem notbi
StepHypRef Expression
1 id 22 . . 3 ((𝜑𝜓) → (𝜑𝜓))
21notbid 317 . 2 ((𝜑𝜓) → (¬ 𝜑 ↔ ¬ 𝜓))
3 id 22 . . 3 ((¬ 𝜑 ↔ ¬ 𝜓) → (¬ 𝜑 ↔ ¬ 𝜓))
43con4bid 316 . 2 ((¬ 𝜑 ↔ ¬ 𝜓) → (𝜑𝜓))
52, 4impbii 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