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

Theorem con1bii 344
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 302 . . 3 (𝜑 ↔ ¬ ¬ 𝜑)
2 con1bii.1 . . 3 𝜑𝜓)
31, 2xchbinx 322 . 2 (𝜑 ↔ ¬ 𝜓)
43bicomi 212 1 𝜓𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 194
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 195
This theorem is referenced by:  con2bii  345  xor  930  3oran  1049  2nexaln  1735  nnel  2796  npss  3583  symdifass  3718  dfnul3  3780  snprc  4100  dffv2  6064  kmlem3  8732  axpowndlem3  9175  nnunb  11042  rpnnen2lem12  14660  dsmmacl  19805  ntreq0  20592  largei  28299  spc2d  28486  ballotlem2  29685  dffr5  30739  brsset  31002  brtxpsd  31007  dfrecs2  31063  dfint3  31065  con1bii2  32187  notbinot1  32923  elpadd0  33988  pm10.252  37464  pm10.253  37465  2exanali  37491
  Copyright terms: Public domain W3C validator