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

Theorem con2bii 322
Description: A contraposition inference. (Contributed by NM, 5-Aug-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 193 . . 3  |-  ( -. 
ps 
<-> 
ph )
32con1bii 321 . 2  |-  ( -. 
ph 
<->  ps )
43bicomi 193 1  |-  ( ps  <->  -. 
ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176
This theorem is referenced by:  xor3  346  imnan  411  annim  414  anor  475  pm4.53  478  pm4.55  480  oran  482  3ianor  949  nanan  1289  xnor  1297  xorass  1299  xorneg1  1302  xorneg  1304  alnex  1533  exnal  1564  2exnexn  1570  equs3  1634  19.3v  1654  19.9vOLD  1682  equsex  1915  nne  2463  dfral2  2568  dfrex2  2569  r19.35  2700  ddif  3321  dfun2  3417  dfin2  3418  difin  3419  dfnul2  3470  rab0  3488  disj4  3516  onuninsuci  4647  omopthi  6671  dfsup2  7211  dfsup2OLD  7212  rankxplim3  7567  alephgeom  7725  ominf4  7954  fin1a2lem7  8048  fin41  8086  reclem2pr  8688  1re  8853  ltnlei  8955  divalglem8  12615  elcls  16826  ist1-2  17091  fin1aufil  17643  dchrelbas3  20493  avril1  20852  nmo  23160  dftr6  24178  sltval2  24381  sltres  24389  nodenselem4  24409  nodenselem7  24412  nofulllem5  24431  dfon3  24503  dffun10  24524  elfuns  24525  axcontlem12  24675  tnf  25055  boxeq  25090  heiborlem1  26638  heiborlem6  26643  heiborlem8  26645  wopprc  27226  f1omvdco3  27495  equsexNEW7  29467  equsexv-x12  29735  cdleme0nex  31101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator