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

Theorem con1bii 345
Description: A contraposition inference. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 13-Oct-2012.)
Hypothesis
Ref Expression
con1bii.1 𝜑𝜓)
Assertion
Ref Expression
con1bii 𝜓𝜑)

Proof of Theorem con1bii
StepHypRef Expression
1 notnotb 304 . . 3 (𝜑 ↔ ¬ ¬ 𝜑)
2 con1bii.1 . . 3 𝜑𝜓)
31, 2xchbinx 323 . 2 (𝜑 ↔ ¬ 𝜓)
43bicomi 214 1 𝜓𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196
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 197
This theorem is referenced by:  con2bii  346  xor  989  3anor  1097  3oran  1099  2nexaln  1905  nnel  3055  npss  3868  symdifass  4003  dfnul3  4067  snprc  4390  dffv2  6414  kmlem3  9177  axpowndlem3  9624  nnunb  11491  rpnnen2lem12  15161  dsmmacl  20303  ntreq0  21103  largei  29467  spc2d  29654  ballotlem2  30891  dffr5  31982  noetalem3  32203  brsset  32334  brtxpsd  32339  dfrecs2  32395  dfint3  32397  con1bii2  33517  notbinot1  34211  elpadd0  35618  pm10.252  39087  pm10.253  39088  2exanali  39114
  Copyright terms: Public domain W3C validator