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  1562  sp  1716  necon2ad  2494  spc2gv  2871  spc3gv  2873  soisoi  5825  isomin  5834  riotaclbg  6344  boxcutc  6859  sdomel  7008  onsdominel  7010  preleq  7318  cantnfreslem  7377  cflim2  7889  cfslbn  7893  cofsmo  7895  fincssdom  7949  fin23lem25  7950  fin23lem26  7951  fin1a2s  8040  pwfseqlem4  8284  ltapr  8669  suplem2pr  8677  qsqueeze  10528  hashbnd  11343  hashclb  11352  sadcaddlem  12648  pc2dvds  12931  infpnlem1  12957  odcl2  14878  ufilmax  17602  ufileu  17614  filufint  17615  hausflim  17676  flimfnfcls  17723  alexsubALTlem3  17743  alexsubALTlem4  17744  reconnlem2  18332  lebnumlem3  18461  itg1ge0a  19066  itg2seq  19097  m1lgs  20601  ex-natded5.13-2  20803  wfi  24207  frind  24243  axlowdimlem14  24583  meran1  24850  iintlem1  25610  lvsovso2  25627  nn0prpw  26239  heiborlem1  26535  mpt2xopynvov0g  28080  bnj23  28744  a12study10  29136  a12study10n  29137  ax9lem3  29142
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator