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  953  3anor  1075  3oran  1077  2nexaln  1797  nnel  2935  npss  3750  symdifass  3886  dfnul3  3951  snprc  4285  dffv2  6310  kmlem3  9012  axpowndlem3  9459  nnunb  11326  rpnnen2lem12  14998  dsmmacl  20133  ntreq0  20929  largei  29254  spc2d  29441  ballotlem2  30678  dffr5  31769  noetalem3  31990  brsset  32121  brtxpsd  32126  dfrecs2  32182  dfint3  32184  con1bii2  33309  notbinot1  34008  elpadd0  35413  pm10.252  38877  pm10.253  38878  2exanali  38904
 Copyright terms: Public domain W3C validator