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

Theorem con1bii 357
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 315 . . 3 (𝜑 ↔ ¬ ¬ 𝜑)
2 con1bii.1 . . 3 𝜑𝜓)
31, 2xchbinx 334 . 2 (𝜑 ↔ ¬ 𝜓)
43bicomi 223 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:  xor  1014  3anor  1109  3oran  1110  2nexaln  1833  2exanali  1864  nnel  3057  spc2d  3560  npss  4069  dfnul3OLD  4287  snprc  4677  dffv2  6932  kmlem3  10022  axpowndlem3  10469  nnunb  12343  rpnnen2lem12  16043  dsmmacl  21076  ntreq0  22356  noetasuplem4  27012  noetainflem4  27016  largei  31014  ballotlem2  32868  dffr5  34121  brsset  34405  brtxpsd  34410  dfrecs2  34466  dfint3  34468  con1bii2  35734  notbinot1  36469  elpadd0  38203  pm10.252  42442  pm10.253  42443  ralfal  43177
  Copyright terms: Public domain W3C validator