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

Theorem con2bii 341
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 209 . . 3 𝜓𝜑)
32con1bii 340 . 2 𝜑𝜓)
43bicomi 209 1 (𝜓 ↔ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 191
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 192
This theorem is referenced by:  xor3  366  imnan  431  annim  434  anor  503  pm4.53  506  pm4.55  508  oran  510  3ianor  1038  nanan  1430  xnor  1448  xorassOLD  1451  xorneg1OLD  1459  xorneg  1461  alnex  1694  exnal  1730  2exnexn  1746  equs3  1823  19.3v  1845  nne  2681  rexnal  2871  dfrex2  2872  r2exlem  2934  r19.35  2958  ddif  3590  dfun2  3705  dfin2  3706  difin  3707  dfnul2  3759  rab0  3791  disj4  3853  snnzb  4065  onuninsuci  6744  omopthi  7435  dfsup2  8043  rankxplim3  8437  alephgeom  8598  fin1a2lem7  8921  fin41  8959  reclem2pr  9558  1re  9727  ltnlei  9840  divalglem8  14542  f1omvdco3  17251  elcls  20246  ist1-2  20520  fin1aufil  21105  dchrelbas3  24327  tgdim01  24712  axcontlem12  25166  avril1  26061  dftr6  30541  sltval2  30694  sltres  30702  nodenselem4  30724  nodenselem7  30727  nofulllem5  30746  dfon3  30810  dffun10  30832  brub  30872  bj-exnalimn  31403  bj-modal4e  31493  con2bii2  31956  heiborlem1  32380  heiborlem6  32385  heiborlem8  32387  cdleme0nex  34096  wopprc  36125  1nevenALTV  39340
  Copyright terms: Public domain W3C validator