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

Theorem con2bii 332
Description: A contraposition inference. (Contributed by NM, 12-Mar-1993.)
Hypothesis
Ref Expression
con2bii.1  |-  ( ph  <->  -. 
ps )
Assertion
Ref Expression
con2bii  |-  ( ps  <->  -. 
ph )

Proof of Theorem con2bii
StepHypRef Expression
1 con2bii.1 . . . 4  |-  ( ph  <->  -. 
ps )
21bicomi 202 . . 3  |-  ( -. 
ps 
<-> 
ph )
32con1bii 331 . 2  |-  ( -. 
ph 
<->  ps )
43bicomi 202 1  |-  ( ps  <->  -. 
ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184
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 185
This theorem is referenced by:  xor3  357  imnan  422  annim  425  anor  489  pm4.53  492  pm4.55  494  oran  496  3ianor  982  nanan  1335  xnor  1352  xorass  1354  xorneg1  1360  xorneg  1362  alnex  1588  exnal  1618  2exnexn  1632  equs3  1696  19.3v  1718  nne  2617  dfral2  2732  dfrex2  2733  r19.35  2872  ddif  3493  dfun2  3590  dfin2  3591  difin  3592  dfnul2  3644  rab0  3663  disj4  3732  snnzb  3945  onuninsuci  6456  omopthi  7101  dfsup2  7697  dfsup2OLD  7698  rankxplim3  8093  alephgeom  8257  fin1a2lem7  8580  fin41  8618  reclem2pr  9222  1re  9390  ltnlei  9500  divalglem8  13609  f1omvdco3  15960  elcls  18682  ist1-2  18956  fin1aufil  19510  dchrelbas3  22582  axcontlem12  23226  avril1  23661  dftr6  27565  sltval2  27802  sltres  27810  nodenselem4  27830  nodenselem7  27833  nofulllem5  27852  dfon3  27928  dffun10  27950  brub  27990  heiborlem1  28715  heiborlem6  28720  heiborlem8  28722  wopprc  29384  bj-exnalimn  32169  cdleme0nex  33939
  Copyright terms: Public domain W3C validator