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  2469  cla42gv  2846  cla43gv  2848  soisoi  5759  isomin  5768  riotaclbg  6312  boxcutc  6827  sdomel  6976  onsdominel  6978  preleq  7286  cantnfreslem  7345  cflim2  7857  cfslbn  7861  cofsmo  7863  fincssdom  7917  fin23lem25  7918  fin23lem26  7919  fin1a2s  8008  pwfseqlem4  8252  ltapr  8637  suplem2pr  8645  qsqueeze  10495  hashbnd  11310  hashclb  11319  sadcaddlem  12611  pc2dvds  12894  infpnlem1  12920  odcl2  14841  ufilmax  17565  ufileu  17577  filufint  17578  hausflim  17639  flimfnfcls  17686  alexsubALTlem3  17706  alexsubALTlem4  17707  reconnlem2  18295  lebnumlem3  18424  itg1ge0a  19029  itg2seq  19060  m1lgs  20564  ex-natded5.13-2  20792  wfi  23577  frind  23613  axlowdimlem14  23959  meran1  24226  iintlem1  24978  lvsovso2  24995  nn0prpw  25607  heiborlem1  25903  bnj23  27876  ax12o10lem3X  28284  ax12o10lem3K  28285  a12study10  28386  a12study10n  28387  ax9lem3  28392
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator