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

Theorem con2bii 324
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 195 . . 3  |-  ( -. 
ps 
<-> 
ph )
32con1bii 323 . 2  |-  ( -. 
ph 
<->  ps )
43bicomi 195 1  |-  ( ps  <->  -. 
ph )
Colors of variables: wff set class
Syntax hints:   -. wn 5    <-> wb 178
This theorem is referenced by:  xor3  348  imnan  413  annim  416  anor  477  pm4.53  480  pm4.55  482  oran  484  3ianor  951  nanan  1291  xnor  1299  xorass  1301  xorneg1  1304  xorneg  1306  alnex  1531  exnal  1562  2exnexn  1568  equs3  1626  19.9v  1664  equsex  1904  nne  2451  dfral2  2556  dfrex2  2557  r19.35  2688  ddif  3309  dfun2  3405  dfin2  3406  difin  3407  dfnul2  3458  rab0  3476  disj4  3504  onuninsuci  4630  omopthi  6650  dfsup2  7190  dfsup2OLD  7191  rankxplim3  7546  alephgeom  7704  ominf4  7933  fin1a2lem7  8027  fin41  8065  reclem2pr  8667  1re  8832  ltnlei  8934  divalglem8  12593  elcls  16804  ist1-2  17069  fin1aufil  17621  dchrelbas3  20471  avril1  20828  dftr6  23510  sltval2  23710  sltres  23718  axdenselem4  23739  axdenselem7  23742  axfelem15  23761  axfelem18  23764  axfelem22  23768  dfon3  23840  elfuns  23861  axcontlem12  24010  tnf  24350  boxeq  24385  heiborlem1  25934  heiborlem6  25939  heiborlem8  25941  wopprc  26522  f1omvdco3  26791  equsexv-x12  28380  cdleme0nex  29746
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179
  Copyright terms: Public domain W3C validator