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

Theorem con4d 97
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 15 1  |-  ( ph  ->  ( ch  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.21d  98  pm2.18  102  con2d  107  con1d  116  mt4d  130  impcon4bid  196  con4bid  284  exim  1565  sp  1728  necon2ad  2507  spc2gv  2884  spc3gv  2886  soisoi  5841  isomin  5850  riotaclbg  6360  boxcutc  6875  sdomel  7024  onsdominel  7026  preleq  7334  cantnfreslem  7393  cflim2  7905  cfslbn  7909  cofsmo  7911  fincssdom  7965  fin23lem25  7966  fin23lem26  7967  fin1a2s  8056  pwfseqlem4  8300  ltapr  8685  suplem2pr  8693  qsqueeze  10544  hashbnd  11359  hashclb  11368  sadcaddlem  12664  pc2dvds  12947  infpnlem1  12973  odcl2  14894  ufilmax  17618  ufileu  17630  filufint  17631  hausflim  17692  flimfnfcls  17739  alexsubALTlem3  17759  alexsubALTlem4  17760  reconnlem2  18348  lebnumlem3  18477  itg1ge0a  19082  itg2seq  19113  m1lgs  20617  ex-natded5.13-2  20819  wfi  24278  frind  24314  axlowdimlem14  24655  meran1  24922  iintlem1  25713  lvsovso2  25730  nn0prpw  26342  heiborlem1  26638  eu2ndop1stv  28083  mpt2xopynvov0g  28196  hashgt12el  28218  hashgt12el2  28219  usgrcyclnl1  28386  bnj23  29060  a12study10  29758  a12study10n  29759  ax9lem3  29764
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator