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  nmo  23144  dftr6  24107  sltval2  24310  sltres  24318  nodenselem4  24338  nodenselem7  24341  nofulllem5  24360  dfon3  24432  dffun10  24453  elfuns  24454  axcontlem12  24603  tnf  24952  boxeq  24987  heiborlem1  26535  heiborlem6  26540  heiborlem8  26542  wopprc  27123  f1omvdco3  27392  equsexv-x12  29113  cdleme0nex  30479
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