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  1584  spOLD  1764  axi11e  2408  necon2ad  2641  spc2gv  3026  spc3gv  3028  soisoi  6034  isomin  6043  mpt2xopynvov0g  6451  riotaclbg  6575  boxcutc  7091  sdomel  7240  onsdominel  7242  preleq  7556  cantnfreslem  7615  cflim2  8127  cfslbn  8131  cofsmo  8133  fincssdom  8187  fin23lem25  8188  fin23lem26  8189  fin1a2s  8278  pwfseqlem4  8521  ltapr  8906  suplem2pr  8914  qsqueeze  10771  hashbnd  11607  hashclb  11624  hashgt0elex  11653  hashgt12el  11665  hashgt12el2  11666  pc2dvds  13235  infpnlem1  13261  odcl2  15184  ufilmax  17922  ufileu  17934  filufint  17935  hausflim  17996  flimfnfcls  18043  alexsubALTlem3  18063  alexsubALTlem4  18064  reconnlem2  18841  lebnumlem3  18971  itg1ge0a  19586  itg2seq  19617  m1lgs  21129  usgraidx2v  21395  cusgrafilem3  21473  cusgrafi  21474  usgrcyclnl1  21610  wfi  25457  frind  25493  axlowdimlem14  25837  meran1  26104  nn0prpw  26258  heiborlem1  26452  eu2ndop1stv  27889  bnj23  28835
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator