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

Theorem con1bii 358
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 316 . . 3 (𝜑 ↔ ¬ ¬ 𝜑)
2 con1bii.1 . . 3 𝜑𝜓)
31, 2xchbinx 335 . 2 (𝜑 ↔ ¬ 𝜓)
43bicomi 225 1 𝜓𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 207
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 208
This theorem is referenced by:  xor  1008  3anor  1100  3oran  1101  2nexaln  1821  2exanali  1851  nnel  3129  spc2d  3600  npss  4084  dfnul3  4292  snprc  4645  dffv2  6749  kmlem3  9566  axpowndlem3  10009  nnunb  11881  rpnnen2lem12  15566  dsmmacl  20813  ntreq0  21613  largei  29971  ballotlem2  31645  dffr5  32886  noetalem3  33116  brsset  33247  brtxpsd  33252  dfrecs2  33308  dfint3  33310  con1bii2  34495  notbinot1  35238  elpadd0  36825  pm10.252  40570  pm10.253  40571
  Copyright terms: Public domain W3C validator