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

Theorem con2bii 345
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 212 . . 3 𝜓𝜑)
32con1bii 344 . 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:  xor3  370  imnan  436  annim  439  anor  508  pm4.53  511  pm4.55  513  oran  515  3ianor  1047  nanan  1440  xnor  1457  xorneg  1467  alnex  1696  exnal  1743  2exnexn  1760  equs3  1861  19.3v  1883  nne  2784  rexnal  2976  dfrex2  2977  r2exlem  3039  r19.35  3063  ddif  3702  dfun2  3819  dfin2  3820  difin  3821  dfnul2  3874  rab0OLD  3908  disj4  3975  snnzb  4196  onuninsuci  6908  omopthi  7600  dfsup2  8209  rankxplim3  8603  alephgeom  8764  fin1a2lem7  9087  fin41  9125  reclem2pr  9725  1re  9894  ltnlei  10008  divalglem8  14906  f1omvdco3  17637  elcls  20628  ist1-2  20902  fin1aufil  21487  dchrelbas3  24679  tgdim01  25118  axcontlem12  25572  avril1  26476  dftr6  30698  sltval2  30858  sltres  30866  nodenselem4  30888  nodenselem7  30891  nofulllem5  30910  dfon3  30974  dffun10  30996  brub  31036  bj-exnalimn  31602  bj-modal4e  31697  con2bii2  32158  heiborlem1  32582  heiborlem6  32587  heiborlem8  32589  cdleme0nex  34397  wopprc  36417  1nevenALTV  39944
  Copyright terms: Public domain W3C validator