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  971  3anor  1097  3oran  1099  2nexaln  1898  nnel  3036  npss  3851  symdifass  3988  dfnul3  4053  snprc  4389  dffv2  6425  kmlem3  9158  axpowndlem3  9605  nnunb  11472  rpnnen2lem12  15145  dsmmacl  20279  ntreq0  21075  largei  29427  spc2d  29614  ballotlem2  30851  dffr5  31942  noetalem3  32163  brsset  32294  brtxpsd  32299  dfrecs2  32355  dfint3  32357  con1bii2  33482  notbinot1  34183  elpadd0  35590  pm10.252  39054  pm10.253  39055  2exanali  39081
  Copyright terms: Public domain W3C validator