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-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  4syl  18  simpl2im  386  hbim  1556  nfal  1587  19.9hd  1673  equsexd  1740  sbcof2  1821  aev  1823  sbequi  1850  nfsbd  1993  mo2n  2070  eupickb  2123  r19.29af2  2634  spc2gv  2851  spc3gv  2853  eqvincg  2884  sbcco3g  3138  ssrmof  3242  exmidsssnc  4232  exmid1stab  4237  snelpwi  4241  opth1  4265  frind  4383  onin  4417  abnexg  4477  reusv1  4489  xpexg  4773  dmexg  4926  rnexg  4927  elrelimasn  5031  relfld  5194  funimaexglem  5337  funimaexg  5338  fabexg  5441  fsnd  5543  elfvm  5587  nfvres  5588  funimass4  5607  elfvmptrab1  5652  funconstss  5676  f1oresrab  5723  resfunexg  5779  f1eqcocnv  5834  isores1  5857  isoini  5861  isose  5864  isopolem  5865  isosolem  5867  eusvobj2  5904  acexmidlemcase  5913  oprabid  5950  offval  6138  resfunexgALT  6160  offval3  6186  1stvalg  6195  2ndvalg  6196  1stcof  6216  2ndcof  6217  cnvf1o  6278  tposf12  6322  smores3  6346  smoiso  6355  tfr0dm  6375  tfrlemibxssdm  6380  tfrlemi14d  6386  tfrexlem  6387  tfr1onlemssrecs  6392  tfr1onlemsucfn  6393  tfr1onlemsucaccv  6394  tfr1onlembxssdm  6396  tfr1onlemres  6402  tfri1dALT  6404  tfrcllemssrecs  6405  tfrcllemsucfn  6406  tfrcllemsucaccv  6407  tfrcllembxssdm  6409  tfrcllemres  6415  rdgss  6436  nnsucsssuc  6545  nntr2  6556  swoord1  6616  swoord2  6617  iinerm  6661  eroveu  6680  pmresg  6730  en1uniel  6858  pw2f1odclem  6890  fopwdom  6892  xpen  6901  ssenen  6907  isinfinf  6953  ac6sfi  6954  preimaf1ofi  7010  sbthlem1  7016  fi0  7034  fiss  7036  supubti  7058  suplubti  7059  isotilem  7065  supisolem  7067  supisoex  7068  supisoti  7069  ordiso2  7094  eldju1st  7130  eldju2ndl  7131  updjud  7141  djudom  7152  ctmlemr  7167  enumctlemm  7173  nnnninfeq  7187  ctssexmid  7209  nninfwlpoimlemginf  7235  exmidonfinlem  7253  en2other2  7256  exmidaclem  7268  cc2lem  7326  cc3  7328  addclnq  7435  mulclnq  7436  1qec  7448  prarloclemarch2  7479  enq0tr  7494  addclnq0  7511  mulclnq0  7512  nq0m0r  7516  prarloclemlo  7554  prarloc  7563  genpml  7577  genpmu  7578  addnqprl  7589  addnqpru  7590  recnnpr  7608  prmuloc2  7627  1idpru  7651  ltexprlemm  7660  ltexprlemloc  7667  recexprlemm  7684  recexprlem1ssl  7693  caucvgprlemnkj  7726  caucvgprlemnbj  7727  caucvgprlemm  7728  caucvgprlemopl  7729  caucvgprlemlol  7730  caucvgprlemladdfu  7737  caucvgprlemladdrl  7738  caucvgprprlemk  7743  caucvgprprlemloccalc  7744  caucvgprprlemnkltj  7749  caucvgprprlemnjltk  7751  caucvgprprlemml  7754  caucvgprprlemmu  7755  caucvgprprlemlol  7758  caucvgprprlemexb  7767  caucvgprprlem1  7769  suplocexprlemml  7776  suplocexprlemlub  7784  addclsr  7813  mulclsr  7814  prsrcl  7844  caucvgsrlemoffcau  7858  peano5nnnn  7952  mulap0r  8634  nn1suc  9001  prime  9416  zindd  9435  xrlttri3  9863  xnn0xadd0  9933  fzopth  10127  fzsuc  10135  fzpred  10136  fzp1ss  10139  fztp  10144  fseq1p1m1  10160  1fv  10205  elfzom1elp1fzo  10269  ssfzo12  10291  fzosplitsn  10300  divfl0  10365  fldiv4lem1div2uz2  10375  modqid  10420  modqmuladdim  10438  frecuzrdgtcl  10483  frecuzrdgfunlem  10490  frecfzennn  10497  frecfzen2  10498  seq3val  10531  seqvalcd  10532  seqsplitg  10560  iseqf1olemqcl  10570  iseqf1olemnab  10572  iseqf1olemmo  10576  iseqf1olemqk  10578  seq3f1olemstep  10585  seqf1oglem2  10591  seq3id3  10595  seqhomog  10601  faclbnd  10812  faclbnd3  10814  bcm1k  10831  hashfz1  10854  hashfz  10892  hashfzp1  10895  fiubm  10899  hashfacen  10907  leisorel  10908  wrdexb  10926  wrdsymb  10941  wrdred1hash  10957  cjcj  11027  caucvgre  11125  r19.2uz  11137  resqrexlemgt0  11164  ltabs  11231  xrmaxiflemab  11390  xrmaxiflemlub  11391  nnf1o  11519  summodclem2a  11524  fsumf1o  11533  fisum0diag2  11590  modfsummodlemstep  11600  fsumparts  11613  clim2prod  11682  prodfap0  11688  prodmodclem2a  11719  fprodssdc  11733  fprodcllem  11749  ef0lem  11803  resinval  11858  recosval  11859  demoivreALT  11917  nn0o  12048  zsupcllemstep  12082  zsupcllemex  12083  infssuzledc  12087  gcdmultiplez  12158  dvdssq  12168  nninfct  12178  eucalg  12197  lcmgcdnn  12220  dvdsnprmd  12263  prm2orodd  12264  isprm5lem  12279  qnumdenbi  12330  nn0gcdsq  12338  phibnd  12355  hashdvds  12359  phimullem  12363  prmdiveq  12374  hashgcdlem  12376  modprm0  12392  nnnn0modprm0  12393  modprmn0modprm0  12394  oddprm  12397  prm23lt5  12401  pcprendvds  12428  pcidlem  12461  pcmpt  12481  pcfac  12488  infpnlem2  12498  prmunb  12500  1arith  12505  4sqlem19  12547  unennn  12554  ennnfonelemk  12557  ennnfonelemjn  12559  ennnfonelemhf1o  12570  ennnfonelemex  12571  ennnfonelemf1  12575  ennnfonelemrn  12576  qnnen  12588  unbendc  12611  setsfun0  12654  srngbased  12764  srngplusgd  12765  srngmulrd  12766  srnginvld  12767  lmodbased  12782  lmodplusgd  12783  lmodscad  12784  lmodvscad  12785  ipsbased  12794  ipsaddgd  12795  ipsmulrd  12796  ipsscad  12797  ipsvscad  12798  ipsipd  12799  tgval  12873  isnsgrp  12989  ismnd  13000  dfgrp2e  13100  subgintm  13268  eqg0el  13299  ecqusaddcl  13309  kerf1ghm  13344  gsumfzconst  13411  imasrng  13452  srgisid  13482  srg1zr  13483  qusring2  13562  oppr1g  13578  dvdsr02  13601  isunitd  13602  crngunit  13607  unitpropdg  13644  elrhmunit  13673  subrngintm  13708  subrguss  13732  subrgunit  13735  subrgugrp  13736  subrgintm  13739  lmodfopnelem1  13820  rmodislmodlem  13846  rmodislmod  13847  lssuni  13859  islss3  13875  lss0v  13926  sraval  13933  rnglidlmmgm  13992  2idllidld  14002  2idlridld  14003  rng2idl0  14015  rng2idlsubg0  14018  zrh0  14113  znle  14125  zndvds0  14138  znf1o  14139  znleval  14141  znfi  14143  znhash  14144  znunit  14147  psrbasg  14159  psradd  14163  cldval  14267  ntrfval  14268  clsfval  14269  neifval  14308  neif  14309  neival  14311  cnclima  14391  cncnpi  14396  cnrest2  14404  cnrest2r  14405  cnptoprest  14407  cnpdis  14410  txvalex  14422  txval  14423  txcnmpt  14441  txdis  14445  cnmpt1t  14453  cnmpt2t  14461  hmeocnv  14475  hmeontr  14481  txhmeo  14487  xmetunirn  14526  xmettpos  14538  metn0  14546  xmetres  14550  metres  14551  blrnps  14579  blrn  14580  blin2  14600  blbas  14601  xmeterval  14603  xmettxlem  14677  xmettx  14678  metcnpi  14683  reldvg  14833  dvaddxx  14852  dvmulxx  14853  dviaddf  14854  dvimulf  14855  dvfre  14859  dveflem  14872  elply2  14881  sinq12gt0  14965  rprelogbdiv  15089  logbgcd1irr  15099  lgslem4  15119  lgsdirprm  15150  gausslemma2dlem0a  15165  gausslemma2dlem0f  15170  gausslemma2dlem0i  15173  gausslemma2dlem1a  15174  gausslemma2dlem1cl  15175  gausslemma2dlem5  15182  gausslemma2dlem6  15183  gausslemma2d  15185  lgseisenlem1  15186  lgseisenlem2  15187  lgseisenlem3  15188  lgseisen  15190  lgsquadlem1  15191  m1lgs  15192  2lgsoddprmlem2  15194  bj-inex  15399  bj-sucexg  15414  bj-peano4  15447  setindis  15459  bdsetindis  15461  bj-inf2vnlem1  15462  nnsf  15495  nninfall  15499  nninfsellemeq  15504  sbthom  15516