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  3593  npss  4111  dfnul3OLD  4329  snprc  4722  dffv2  6987  kmlem3  10147  axpowndlem3  10594  nnunb  12468  rpnnen2lem12  16168  dsmmacl  21296  ntreq0  22581  noetasuplem4  27239  noetainflem4  27243  largei  31551  ballotlem2  33518  dffr5  34755  brsset  34892  brtxpsd  34897  dfrecs2  34953  dfint3  34955  con1bii2  36261  notbinot1  36995  elpadd0  38728  pm10.252  43168  pm10.253  43169  ralfal  43903
  Copyright terms: Public domain W3C validator