MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  con2bii 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  1295  xnor  1312  xorass  1314  xorneg1  1317  xorneg  1319  alnex  1549  exnal  1580  2exnexn  1587  equs3  1651  19.3v  1673  19.9vOLD  1706  equsexOLD  1970  nne  2571  dfral2  2678  dfrex2  2679  r19.35  2815  ddif  3439  dfun2  3536  dfin2  3537  difin  3538  dfnul2  3590  rab0  3608  disj4  3636  onuninsuci  4779  omopthi  6859  dfsup2  7405  dfsup2OLD  7406  rankxplim3  7761  alephgeom  7919  fin1a2lem7  8242  fin41  8280  reclem2pr  8881  1re  9046  ltnlei  9150  divalglem8  12875  elcls  17092  ist1-2  17365  fin1aufil  17917  dchrelbas3  20975  avril1  21710  dftr6  25321  sltval2  25524  sltres  25532  nodenselem4  25552  nodenselem7  25555  nofulllem5  25574  dfon3  25646  dffun10  25667  elfuns  25668  axcontlem12  25818  heiborlem1  26410  heiborlem6  26415  heiborlem8  26417  wopprc  26991  f1omvdco3  27260  equsexNEW7  29196  cdleme0nex  30772
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