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

Theorem notbi 322
 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 321 . 2 ((𝜑𝜓) → (¬ 𝜑 ↔ ¬ 𝜓))
3 id 22 . . 3 ((¬ 𝜑 ↔ ¬ 𝜓) → (¬ 𝜑 ↔ ¬ 𝜓))
43con4bid 320 . 2 ((¬ 𝜑 ↔ ¬ 𝜓) → (𝜑𝜓))
52, 4impbii 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  1534  hadnot  1604  had0  1606  cbvexdw  2351  cbvexd  2421  vtoclgft  3504  isocnv3  7068  suppimacnv  7828  sumodd  15732  f1omvdco3  18572  ist0cld  31186  onsuct0  33897  bj-cbvexdv  34232  wl-3xornot  34891  ifpbi1  40172  ifpbi13  40184  abciffcbatnabciffncba  43509  abciffcbatnabciffncbai  43510  ichn  43960
 Copyright terms: Public domain W3C validator