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

Theorem con4d 99
Description: Deduction derived from axiom ax-3 7. (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 7 . 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  100  pm2.18  104  con2d  109  con1d  118  mt4d  132  impcon4bid  197  con4bid  285  exim  1581  spOLD  1756  axi11e  2359  necon2ad  2591  spc2gv  2975  spc3gv  2977  soisoi  5980  isomin  5989  mpt2xopynvov0g  6394  riotaclbg  6518  boxcutc  7034  sdomel  7183  onsdominel  7185  preleq  7498  cantnfreslem  7557  cflim2  8069  cfslbn  8073  cofsmo  8075  fincssdom  8129  fin23lem25  8130  fin23lem26  8131  fin1a2s  8220  pwfseqlem4  8463  ltapr  8848  suplem2pr  8856  qsqueeze  10712  hashbnd  11544  hashclb  11561  hashgt0elex  11590  hashgt12el  11602  hashgt12el2  11603  pc2dvds  13172  infpnlem1  13198  odcl2  15121  ufilmax  17853  ufileu  17865  filufint  17866  hausflim  17927  flimfnfcls  17974  alexsubALTlem3  17994  alexsubALTlem4  17995  reconnlem2  18722  lebnumlem3  18852  itg1ge0a  19463  itg2seq  19494  m1lgs  21006  usgraidx2v  21271  cusgrafilem3  21349  cusgrafi  21350  usgrcyclnl1  21468  wfi  25224  frind  25260  axlowdimlem14  25601  meran1  25868  nn0prpw  26010  heiborlem1  26204  eu2ndop1stv  27641  bnj23  28414  a12study10  29112  a12study10n  29113  ax9lem3  29118
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator