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  2460  cla42gv  2808  cla43gv  2810  soisoi  5677  isomin  5686  riotaclbg  6230  boxcutc  6745  sdomel  6893  onsdominel  6895  preleq  7202  cantnfreslem  7261  cflim2  7773  cfslbn  7777  cofsmo  7779  fincssdom  7833  fin23lem25  7834  fin23lem26  7835  fin1a2s  7924  pwfseqlem4  8164  ltapr  8549  suplem2pr  8557  qsqueeze  10406  hashbnd  11221  hashclb  11230  sadcaddlem  12522  pc2dvds  12805  infpnlem1  12831  odcl2  14713  ufilmax  17434  ufileu  17446  filufint  17447  hausflim  17508  flimfnfcls  17555  alexsubALTlem3  17575  alexsubALTlem4  17576  reconnlem2  18164  lebnumlem3  18293  itg1ge0a  18898  itg2seq  18929  m1lgs  20433  ex-natded5.13-2  20661  wfi  23375  frind  23411  axlowdimlem14  23757  meran1  24024  iintlem1  24776  lvsovso2  24793  nn0prpw  25405  heiborlem1  25701  bnj23  27433  ax12o10lem3X  27835  ax12o10lem3K  27836  a12study10  27937  a12study10n  27938  ax9lem3  27943
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator