Theorem 3syl 17

Description: Inference chaining two syllogisms. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
3syl.1	|- ( ph -> ps )
3syl.2	|- ( ps -> ch )
3syl.3	|- ( ch -> th )

Assertion

Ref	Expression
3syl	|- ( ph -> th )

Proof of Theorem 3syl

Step	Hyp	Ref	Expression
1		3syl.1	. . 3 |- ( ph -> ps )
2		3syl.2	. . 3 |- ( ps -> ch )
3	1, 2	syl 14	. 2 |- ( ph -> ch )
4		3syl.3	. 2 |- ( ch -> th )
5	3, 4	syl 14	1 |- ( ph -> th )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  4syl  18  simpl2im  379  hbim  1483  19.9hd  1598  equsexd  1665  sbcof2  1739  aev  1741  sbequi  1768  nfsbd  1900  mo2n  1977  eupickb  2030  r19.29af2  2509  spc2gv  2710  spc3gv  2712  eqvincg  2742  sbcco3g  2986  snelpwi  4048  opth1  4072  frind  4188  onin  4222  abnexg  4281  reusv1  4293  xpexg  4565  dmexg  4710  rnexg  4711  relfld  4972  funimaexglem  5110  funimaexg  5111  fabexg  5211  nfvres  5350  funimass4  5368  funconstss  5431  f1oresrab  5477  resfunexg  5532  f1eqcocnv  5584  isores1  5607  isoini  5611  isose  5614  isopolem  5615  isosolem  5617  eusvobj2  5652  acexmidlemcase  5661  oprabid  5695  offval  5877  resfunexgALT  5895  offval3  5919  1stvalg  5927  2ndvalg  5928  1stcof  5948  2ndcof  5949  cnvf1o  6004  tposf12  6048  smores3  6072  smoiso  6081  tfr0dm  6101  tfrlemibxssdm  6106  tfrlemi14d  6112  tfrexlem  6113  tfr1onlemssrecs  6118  tfr1onlemsucfn  6119  tfr1onlemsucaccv  6120  tfr1onlembxssdm  6122  tfr1onlemres  6128  tfri1dALT  6130  tfrcllemssrecs  6131  tfrcllemsucfn  6132  tfrcllemsucaccv  6133  tfrcllembxssdm  6135  tfrcllemres  6141  rdgss  6162  nnsucsssuc  6267  swoord1  6335  swoord2  6336  iinerm  6378  eroveu  6397  pmresg  6447  en1uniel  6575  fopwdom  6606  xpen  6615  ssenen  6621  isinfinf  6667  ac6sfi  6668  preimaf1ofi  6714  sbthlem1  6720  supubti  6748  suplubti  6749  isotilem  6755  supisolem  6757  supisoex  6758  supisoti  6759  ordiso2  6782  djur  6811  eldju1st  6816  eldju2ndl  6817  updjud  6827  djudom  6837  ctmlemr  6844  enumctlemm  6846  en2other2  6883  addclnq  6995  mulclnq  6996  1qec  7008  prarloclemarch2  7039  enq0tr  7054  addclnq0  7071  mulclnq0  7072  nq0m0r  7076  prarloclemlo  7114  prarloc  7123  genpml  7137  genpmu  7138  addnqprl  7149  addnqpru  7150  recnnpr  7168  prmuloc2  7187  1idpru  7211  ltexprlemm  7220  ltexprlemloc  7227  recexprlemm  7244  recexprlem1ssl  7253  caucvgprlemnkj  7286  caucvgprlemnbj  7287  caucvgprlemm  7288  caucvgprlemopl  7289  caucvgprlemlol  7290  caucvgprlemladdfu  7297  caucvgprlemladdrl  7298  caucvgprprlemk  7303  caucvgprprlemloccalc  7304  caucvgprprlemnkltj  7309  caucvgprprlemnjltk  7311  caucvgprprlemml  7314  caucvgprprlemmu  7315  caucvgprprlemlol  7318  caucvgprprlemexb  7327  caucvgprprlem1  7329  addclsr  7360  mulclsr  7361  prsrcl  7390  caucvgsrlemoffcau  7404  peano5nnnn  7488  mulap0r  8153  nn1suc  8502  prime  8906  zindd  8925  xrlttri3  9328  fzopth  9536  fzsuc  9544  fzpred  9545  fzp1ss  9548  fztp  9553  fseq1p1m1  9569  1fv  9611  elfzom1elp1fzo  9674  ssfzo12  9696  fzosplitsn  9705  divfl0  9764  modqid  9817  modqmuladdim  9835  frecuzrdgtcl  9880  frecuzrdgfunlem  9887  frecfzennn  9894  frecfzen2  9895  iseqvalt  9934  seq3val  9935  iseqsplit  9969  iseqf1olemqcl  9976  iseqf1olemnab  9978  iseqf1olemmo  9982  iseqf1olemqk  9984  seq3f1olemstep  9991  iseqid3s  9999  faclbnd  10210  faclbnd3  10212  bcm1k  10229  hashfz1  10252  focdmex  10256  hashfz  10290  hashfzp1  10293  hashfacen  10302  leisorel  10303  cjcj  10378  caucvgre  10475  r19.2uz  10487  resqrexlemgt0  10514  ltabs  10581  isummolemnm  10830  isummolem2a  10832  fsumf1o  10843  fisum0diag2  10902  modfsummodlemstep  10912  fsumparts  10925  ef0lem  11011  resinval  11067  recosval  11068  demoivreALT  11124  nn0o  11246  zsupcllemstep  11280  zsupcllemex  11281  infssuzledc  11285  gcdmultiplez  11349  dvdssq  11359  eucalg  11380  lcmgcdnn  11403  dvdsnprmd  11446  prm2orodd  11447  qnumdenbi  11509  nn0gcdsq  11517  phibnd  11532  hashdvds  11536  phimullem  11540  hashgcdlem  11542  unennn  11549  setsfun0  11591  srngbased  11678  srngplusgd  11679  srngmulrd  11680  srnginvld  11681  lmodbased  11689  lmodplusgd  11690  lmodscad  11691  lmodvscad  11692  ipsbased  11697  ipsaddgd  11698  ipsmulrd  11699  ipsscad  11700  ipsvscad  11701  ipsipd  11702  tgval  11810  cldval  11860  ntrfval  11861  clsfval  11862  bj-inex  12071  bj-sucexg  12086  bj-peano4  12123  setindis  12135  bdsetindis  12137  bj-inf2vnlem1  12138  nnsf  12167  nninfalllemn  12170  nninfall  12172  nninfsellemeq  12178