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

Theorem con4d 100
Description: Deduction derived from axiom ax-3 8. (Contributed by NM, 26-Mar-1995.)
Hypothesis
Ref Expression
con4d.1  |-  ( ph  ->  ( -.  ps  ->  -. 
ch ) )
Assertion
Ref Expression
con4d  |-  ( ph  ->  ( ch  ->  ps ) )

Proof of Theorem con4d
StepHypRef Expression
1 con4d.1 . 2  |-  ( ph  ->  ( -.  ps  ->  -. 
ch ) )
2 ax-3 8 . 2  |-  ( ( -.  ps  ->  -.  ch )  ->  ( ch 
->  ps ) )
31, 2syl 16 1  |-  ( ph  ->  ( ch  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.21d  101  pm2.18  105  con2d  110  con1d  119  mt4d  133  impcon4bid  198  con4bid  286  exim  1585  spOLD  1765  necon2ad  2654  spc2gv  3041  spc3gv  3043  soisoi  6051  isomin  6060  mpt2xopynvov0g  6468  riotaclbg  6592  boxcutc  7108  sdomel  7257  onsdominel  7259  preleq  7575  cantnfreslem  7634  cflim2  8148  cfslbn  8152  cofsmo  8154  fincssdom  8208  fin23lem25  8209  fin23lem26  8210  fin1a2s  8299  pwfseqlem4  8542  ltapr  8927  suplem2pr  8935  qsqueeze  10792  hashbnd  11629  hashclb  11646  hashgt0elex  11675  hashgt12el  11687  hashgt12el2  11688  pc2dvds  13257  infpnlem1  13283  odcl2  15206  ufilmax  17944  ufileu  17956  filufint  17957  hausflim  18018  flimfnfcls  18065  alexsubALTlem3  18085  alexsubALTlem4  18086  reconnlem2  18863  lebnumlem3  18993  itg1ge0a  19606  itg2seq  19637  m1lgs  21151  usgraidx2v  21417  cusgrafilem3  21495  cusgrafi  21496  usgrcyclnl1  21632  wfi  25487  frind  25523  axlowdimlem14  25899  meran1  26166  nn0prpw  26340  heiborlem1  26534  eu2ndop1stv  27970  swrdvalodmlem1  28221  bnj23  29157
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator