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

Theorem con2bii 323
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 194 . . 3  |-  ( -. 
ps 
<-> 
ph )
32con1bii 322 . 2  |-  ( -. 
ph 
<->  ps )
43bicomi 194 1  |-  ( ps  <->  -. 
ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 177
This theorem is referenced by:  xor3  347  imnan  412  annim  415  anor  476  pm4.53  479  pm4.55  481  oran  483  3ianor  951  nanan  1298  xnor  1315  xorass  1317  xorneg1  1320  xorneg  1322  alnex  1552  exnal  1583  2exnexn  1590  equs3  1654  19.3v  1677  19.9vOLD  1710  equsexOLD  2003  nne  2605  dfral2  2717  dfrex2  2718  r19.35  2855  ddif  3479  dfun2  3576  dfin2  3577  difin  3578  dfnul2  3630  rab0  3648  disj4  3676  onuninsuci  4820  omopthi  6900  dfsup2  7447  dfsup2OLD  7448  rankxplim3  7805  alephgeom  7963  fin1a2lem7  8286  fin41  8324  reclem2pr  8925  1re  9090  ltnlei  9194  divalglem8  12920  elcls  17137  ist1-2  17411  fin1aufil  17964  dchrelbas3  21022  avril1  21757  dftr6  25373  snnzb  25402  sltval2  25611  sltres  25619  nodenselem4  25639  nodenselem7  25642  nofulllem5  25661  dfon3  25737  dffun10  25759  brub  25799  axcontlem12  25914  heiborlem1  26520  heiborlem6  26525  heiborlem8  26527  wopprc  27101  f1omvdco3  27369  equsexNEW7  29490  cdleme0nex  31087
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 178
  Copyright terms: Public domain W3C validator