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

Theorem notbi 319
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 318 . 2 ((𝜑𝜓) → (¬ 𝜑 ↔ ¬ 𝜓))
3 id 22 . . 3 ((¬ 𝜑 ↔ ¬ 𝜓) → (¬ 𝜑 ↔ ¬ 𝜓))
43con4bid 317 . 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  320  con4bii  321  con2bi  354  nbn2  371  pm5.32  575  norass  1539  hadnot  1604  had0  1606  cbvexdw  2336  cbvexd  2408  rexbiOLD  3106  rexprg  4700  isocnv3  7326  suppimacnv  8156  sumodd  16328  f1omvdco3  19312  ist0cld  32802  onsuct0  35315  bj-cbvexdv  35667  wl-3xornot  36351  ifpbi1  42214  ifpbi13  42226  abciffcbatnabciffncba  45626  abciffcbatnabciffncbai  45627  ichn  46111
  Copyright terms: Public domain W3C validator