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  1530  exnal  1561  2exnexn  1567  equs3  1625  19.9v  1663  equsex  1902  nne  2450  dfral2  2555  dfrex2  2556  r19.35  2687  ddif  3308  dfun2  3404  dfin2  3405  difin  3406  dfnul2  3457  rab0  3475  disj4  3503  onuninsuci  4631  omopthi  6655  dfsup2  7195  dfsup2OLD  7196  rankxplim3  7551  alephgeom  7709  ominf4  7938  fin1a2lem7  8032  fin41  8070  reclem2pr  8672  1re  8837  ltnlei  8939  divalglem8  12599  elcls  16810  ist1-2  17075  fin1aufil  17627  dchrelbas3  20477  avril1  20836  dftr6  23518  sltval2  23721  sltres  23729  nodenselem4  23749  nodenselem7  23752  nofulllem5  23771  dfon3  23843  dffun10  23864  elfuns  23865  axcontlem12  24014  tnf  24364  boxeq  24399  heiborlem1  25947  heiborlem6  25952  heiborlem8  25954  wopprc  26535  f1omvdco3  26804  equsexv-x12  28486  cdleme0nex  29852
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