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

Theorem con2bii 347
Description: A contraposition inference. (Contributed by NM, 12-Mar-1993.)
Hypothesis
Ref Expression
con2bii.1 (𝜑 ↔ ¬ 𝜓)
Assertion
Ref Expression
con2bii (𝜓 ↔ ¬ 𝜑)

Proof of Theorem con2bii
StepHypRef Expression
1 con2bii.1 . . . 4 (𝜑 ↔ ¬ 𝜓)
21bicomi 214 . . 3 𝜓𝜑)
32con1bii 346 . 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:  xor3  372  imnan  438  annim  441  anor  510  pm4.53  513  pm4.55  515  oran  517  3ianor  1053  nanan  1446  xnor  1463  xorneg  1473  alnex  1703  exnal  1751  2exnexn  1769  equs3  1877  19.3v  1899  nne  2800  rexnal  2994  dfrex2  2995  r2exlem  3057  r19.35  3081  ddif  3725  dfun2  3842  dfin2  3843  difin  3844  dfnul2  3898  rab0OLD  3935  disj4  4002  snnzb  4229  onuninsuci  6988  omopthi  7683  dfsup2  8295  rankxplim3  8689  alephgeom  8850  fin1a2lem7  9173  fin41  9211  reclem2pr  9815  1re  9984  ltnlei  10103  divalglem8  15042  f1omvdco3  17785  elcls  20782  ist1-2  21056  fin1aufil  21641  dchrelbas3  24858  tgdim01  25297  axcontlem12  25750  avril1  27167  dftr6  31339  sltval2  31498  sltres  31506  nodenselem4  31528  nodenselem7  31531  nofulllem5  31550  dfon3  31614  dffun10  31636  brub  31676  bj-exnalimn  32225  bj-modal4e  32320  con2bii2  32785  heiborlem1  33209  heiborlem6  33214  heiborlem8  33216  cdleme0nex  35024  wopprc  37044  1nevenALTV  40870
  Copyright terms: Public domain W3C validator