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 9. (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 9 . 2  |-  ( ( -.  ps  ->  -.  ch )  ->  ( ch 
->  ps ) )
31, 2syl 17 1  |-  ( ph  ->  ( ch  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6
This theorem is referenced by:  pm2.21d  100  pm2.18  104  con2d  109  con1d  118  mt4d  132  impcon4bid  198  con4bid  286  exim  1573  ax12o10lem3  1637  ax4  1691  necon2ad  2467  cla42gv  2822  cla43gv  2824  soisoi  5724  isomin  5733  riotaclbg  6277  boxcutc  6792  sdomel  6941  onsdominel  6943  preleq  7251  cantnfreslem  7310  cflim2  7822  cfslbn  7826  cofsmo  7828  fincssdom  7882  fin23lem25  7883  fin23lem26  7884  fin1a2s  7973  pwfseqlem4  8217  ltapr  8602  suplem2pr  8610  qsqueeze  10459  hashbnd  11274  hashclb  11283  sadcaddlem  12575  pc2dvds  12858  infpnlem1  12884  odcl2  14805  ufilmax  17529  ufileu  17541  filufint  17542  hausflim  17603  flimfnfcls  17650  alexsubALTlem3  17670  alexsubALTlem4  17671  reconnlem2  18259  lebnumlem3  18388  itg1ge0a  18993  itg2seq  19024  m1lgs  20528  ex-natded5.13-2  20756  wfi  23541  frind  23577  axlowdimlem14  23923  meran1  24190  iintlem1  24942  lvsovso2  24959  nn0prpw  25571  heiborlem1  25867  bnj23  27756  ax12o10lem3X  28164  ax12o10lem3K  28165  a12study10  28266  a12study10n  28267  ax9lem3  28272
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator