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  1732  2exnexn  1749  equs3  1825  19.3v  1847  nne  2690  rexnal  2882  dfrex2  2883  r2exlem  2945  r19.35  2969  ddif  3608  dfun2  3724  dfin2  3725  difin  3726  dfnul2  3779  rab0OLD  3813  disj4  3880  snnzb  4101  onuninsuci  6807  omopthi  7499  dfsup2  8108  rankxplim3  8502  alephgeom  8663  fin1a2lem7  8986  fin41  9024  reclem2pr  9624  1re  9793  ltnlei  9908  divalglem8  14830  f1omvdco3  17582  elcls  20588  ist1-2  20862  fin1aufil  21447  dchrelbas3  24653  tgdim01  25092  axcontlem12  25546  avril1  26450  dftr6  30736  sltval2  30889  sltres  30897  nodenselem4  30919  nodenselem7  30922  nofulllem5  30941  dfon3  31005  dffun10  31027  brub  31067  bj-exnalimn  31632  bj-modal4e  31727  con2bii2  32188  heiborlem1  32655  heiborlem6  32660  heiborlem8  32662  cdleme0nex  34470  wopprc  36490  1nevenALTV  40035
  Copyright terms: Public domain W3C validator