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

Theorem con2bii 330
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 329 . 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  355  imnan  420  annim  423  anor  487  pm4.53  490  pm4.55  492  oran  494  3ianor  988  nanan  1343  xnor  1364  xorassOLD  1367  xorneg1OLD  1375  xorneg  1377  alnex  1622  exnal  1656  2exnexn  1673  equs3  1742  19.3v  1763  nne  2583  rexnal  2830  dfral2OLD  2832  dfrex2  2833  r2exlem  2902  r19.35  2929  ddif  3550  dfun2  3658  dfin2  3659  difin  3660  dfnul2  3713  rab0  3733  disj4  3791  snnzb  4008  onuninsuci  6574  omopthi  7224  dfsup2  7817  dfsup2OLD  7818  rankxplim3  8212  alephgeom  8376  fin1a2lem7  8699  fin41  8737  reclem2pr  9337  1re  9506  ltnlei  9616  divalglem8  14060  f1omvdco3  16591  elcls  19660  ist1-2  19934  fin1aufil  20518  dchrelbas3  23630  tgdim01  24018  axcontlem12  24399  avril1  25292  dftr6  29345  sltval2  29581  sltres  29589  nodenselem4  29609  nodenselem7  29612  nofulllem5  29631  dfon3  29695  dffun10  29717  brub  29757  heiborlem1  30473  heiborlem6  30478  heiborlem8  30480  wopprc  31138  1nevenALTV  32533  bj-exnalimn  34568  cdleme0nex  36428
  Copyright terms: Public domain W3C validator