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  1872  19.3v  1894  nne  2794  rexnal  2991  dfrex2  2992  r2exlem  3054  r19.35  3078  ddif  3726  dfun2  3843  dfin2  3844  difin  3845  dfnul2  3899  rab0OLD  3936  disj4  4003  snnzb  4231  onuninsuci  7002  omopthi  7697  dfsup2  8310  rankxplim3  8704  alephgeom  8865  fin1a2lem7  9188  fin41  9226  reclem2pr  9830  1re  9999  ltnlei  10118  divalglem8  15066  f1omvdco3  17809  elcls  20817  ist1-2  21091  fin1aufil  21676  dchrelbas3  24897  tgdim01  25336  axcontlem12  25789  avril1  27207  dftr6  31401  sltval2  31563  sltres  31571  nodenselem4  31600  nodenselem7  31603  dfon3  31694  dffun10  31716  brub  31756  bj-exnalimn  32305  bj-modal4e  32400  con2bii2  32851  heiborlem1  33281  heiborlem6  33286  heiborlem8  33288  cdleme0nex  35096  wopprc  37116  1nevenALTV  40931
  Copyright terms: Public domain W3C validator