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  1594  nfal  1625  19.9hd  1710  equsexd  1778  sbcof2  1859  aev  1861  sbequi  1888  nfsbd  2031  mo2n  2108  eupickb  2162  r19.29af2  2683  spc2gv  2908  spc3gv  2910  eqvincg  2941  sbcco3g  3196  ssrmof  3301  exmidsssnc  4316  exmid1stab  4321  snelpwi  4327  opth1  4352  frind  4473  onin  4507  abnexg  4567  reusv1  4579  xpexg  4864  reldmm  4975  dmexg  5021  rnexg  5022  elrelimasn  5128  relfld  5291  funimaexglem  5439  funimaexg  5440  fabexg  5554  fsnd  5659  elfvm  5703  nfvres  5706  funimass4  5727  elfvmptrab1  5772  funconstss  5796  f1oresrab  5842  resfunexg  5905  f1eqcocnv  5964  isores1  5987  isoini  5991  isose  5994  isopolem  5995  isosolem  5997  eusvobj2  6036  acexmidlemcase  6045  oprabid  6082  offval  6274  resfunexgALT  6301  offval3  6327  1stvalg  6336  2ndvalg  6337  1stcof  6357  2ndcof  6358  cnvf1o  6421  tposf12  6500  smores3  6524  smoiso  6533  tfr0dm  6553  tfrlemibxssdm  6558  tfrlemi14d  6564  tfrexlem  6565  tfr1onlemssrecs  6570  tfr1onlemsucfn  6571  tfr1onlemsucaccv  6572  tfr1onlembxssdm  6574  tfr1onlemres  6580  tfri1dALT  6582  tfrcllemssrecs  6583  tfrcllemsucfn  6584  tfrcllemsucaccv  6585  tfrcllembxssdm  6587  tfrcllemres  6593  rdgss  6614  nnsucsssuc  6725  nntr2  6736  swoord1  6796  swoord2  6797  iinerm  6841  eroveu  6860  pmresg  6910  en1uniel  7044  dom1o  7069  pw2f1odclem  7087  fopwdom  7089  xpen  7098  mapunen  7104  ssenen  7105  isinfinf  7154  ac6sfi  7155  preimaf1ofi  7221  sbthlem1  7227  fczfsuppd  7250  fi0  7262  fiss  7264  supubti  7290  suplubti  7291  isotilem  7297  supisolem  7299  supisoex  7300  supisoti  7301  ordiso2  7326  eldju1st  7362  eldju2ndl  7363  updjud  7373  djudom  7384  ctmlemr  7399  enumctlemm  7405  nnnninfeq  7419  ctssexmid  7441  nninfwlpoimlemginf  7467  exmidonfinlem  7496  en2other2  7499  exmidaclem  7515  cc2lem  7580  cc3  7582  addclnq  7690  mulclnq  7691  1qec  7703  prarloclemarch2  7734  enq0tr  7749  addclnq0  7766  mulclnq0  7767  nq0m0r  7771  prarloclemlo  7809  prarloc  7818  genpml  7832  genpmu  7833  addnqprl  7844  addnqpru  7845  recnnpr  7863  prmuloc2  7882  1idpru  7906  ltexprlemm  7915  ltexprlemloc  7922  recexprlemm  7939  recexprlem1ssl  7948  caucvgprlemnkj  7981  caucvgprlemnbj  7982  caucvgprlemm  7983  caucvgprlemopl  7984  caucvgprlemlol  7985  caucvgprlemladdfu  7992  caucvgprlemladdrl  7993  caucvgprprlemk  7998  caucvgprprlemloccalc  7999  caucvgprprlemnkltj  8004  caucvgprprlemnjltk  8006  caucvgprprlemml  8009  caucvgprprlemmu  8010  caucvgprprlemlol  8013  caucvgprprlemexb  8022  caucvgprprlem1  8024  suplocexprlemml  8031  suplocexprlemlub  8039  addclsr  8068  mulclsr  8069  prsrcl  8099  caucvgsrlemoffcau  8113  peano5nnnn  8207  mulap0r  8889  nn1suc  9256  prime  9677  zindd  9696  xrlttri3  10130  xnn0xadd0  10200  fzopth  10395  fzsuc  10403  fzpred  10404  fzp1ss  10407  fztp  10412  fseq1p1m1  10428  1fv  10473  elfzom1elp1fzo  10547  ssfzo12  10569  fzosplitsn  10578  zsupcllemstep  10589  zsupcllemex  10590  infssuzledc  10594  divfl0  10656  fldiv4lem1div2uz2  10666  modqid  10711  modqmuladdim  10729  frecuzrdgtcl  10774  frecuzrdgfunlem  10781  frecfzennn  10788  frecfzen2  10789  seq3val  10822  seqvalcd  10823  seqsplitg  10851  iseqf1olemqcl  10861  iseqf1olemnab  10863  iseqf1olemmo  10867  iseqf1olemqk  10869  seq3f1olemstep  10876  seqf1oglem2  10882  seq3id3  10886  seqhomog  10892  faclbnd  11103  faclbnd3  11105  bcm1k  11122  hashfz1  11146  hashfz  11186  hashfzp1  11189  fiubm  11195  hashfacen  11208  leisorel  11209  wrdexb  11236  wrdsymb  11252  wrdred1hash  11268  lsw0  11272  lswex  11276  ccat0  11284  ccatval2  11286  ccatw2s1leng  11326  ccats1val2  11328  swrds1  11360  swrdlsw  11361  ccats1pfxeqrex  11407  pfxccatin12lem1  11420  swrdccatin2  11421  swrdccat  11427  cats1fvd  11458  s1s2d  11486  s1s3d  11487  cjcj  11568  caucvgre  11666  r19.2uz  11678  resqrexlemgt0  11705  ltabs  11772  xrmaxiflemab  11932  xrmaxiflemlub  11933  nnf1o  12062  summodclem2a  12067  fsumf1o  12076  fisum0diag2  12133  modfsummodlemstep  12143  fsumparts  12156  clim2prod  12225  prodfap0  12231  prodmodclem2a  12262  fprodssdc  12276  fprodcllem  12292  ef0lem  12346  resinval  12401  recosval  12402  demoivreALT  12460  nn0o  12593  gcdmultiplez  12717  dvdssq  12727  nninfct  12737  eucalg  12756  lcmgcdnn  12779  dvdsnprmd  12822  prm2orodd  12823  isprm5lem  12838  qnumdenbi  12889  nn0gcdsq  12897  phibnd  12914  hashdvds  12918  phimullem  12922  prmdiveq  12933  hashgcdlem  12935  modprm0  12952  nnnn0modprm0  12953  modprmn0modprm0  12954  oddprm  12957  prm23lt5  12961  pcprendvds  12988  pcidlem  13021  pcmpt  13041  pcfac  13048  infpnlem2  13058  prmunb  13060  1arith  13065  4sqlem19  13107  unennn  13148  ennnfonelemk  13151  ennnfonelemjn  13153  ennnfonelemhf1o  13164  ennnfonelemex  13165  ennnfonelemf1  13169  ennnfonelemrn  13170  qnnen  13182  unbendc  13205  setsfun0  13248  srngbased  13360  srngplusgd  13361  srngmulrd  13362  srnginvld  13363  lmodbased  13378  lmodplusgd  13379  lmodscad  13380  lmodvscad  13381  ipsbased  13390  ipsaddgd  13391  ipsmulrd  13392  ipsscad  13393  ipsvscad  13394  ipsipd  13395  tgval  13475  prdsbas3  13500  isnsgrp  13619  ismnd  13632  dfgrp2e  13741  subgintm  13915  eqg0el  13946  ecqusaddcl  13956  kerf1ghm  13991  gsumfzconst  14058  imasrng  14100  srgisid  14130  srg1zr  14131  qusring2  14210  oppr1g  14226  dvdsr02  14250  isunitd  14251  crngunit  14256  unitpropdg  14293  elrhmunit  14322  subrngintm  14357  subrguss  14381  subrgunit  14384  subrgugrp  14385  subrgintm  14388  lmodfopnelem1  14472  rmodislmodlem  14498  rmodislmod  14499  lssuni  14511  islss3  14527  lss0v  14578  sraval  14585  rnglidlmmgm  14644  2idllidld  14654  2idlridld  14655  rng2idl0  14667  rng2idlsubg0  14670  zrh0  14773  znle  14785  zndvds0  14798  znf1o  14799  znleval  14801  znfi  14803  znhash  14804  znunit  14807  psrbaglecl  14824  psrbasg  14829  psradd  14834  psr0cl  14836  mpladd  14859  cldval  14964  ntrfval  14965  clsfval  14966  neifval  15005  neif  15006  neival  15008  cnclima  15088  cncnpi  15093  cnrest2  15101  cnrest2r  15102  cnptoprest  15104  cnpdis  15107  txvalex  15119  txval  15120  txcnmpt  15138  txdis  15142  cnmpt1t  15150  cnmpt2t  15158  hmeocnv  15172  hmeontr  15178  txhmeo  15184  xmetunirn  15223  xmettpos  15235  metn0  15243  xmetres  15247  metres  15248  blrnps  15276  blrn  15277  blin2  15297  blbas  15298  xmeterval  15300  xmettxlem  15374  xmettx  15375  metcnpi  15380  reldvg  15544  dvaddxx  15568  dvmulxx  15569  dviaddf  15570  dvimulf  15571  dvfre  15575  dvmptid  15581  dveflem  15591  elply2  15600  plyreres  15629  sinq12gt0  15695  rprelogbdiv  15822  logbgcd1irr  15832  fsumdvdsmul  15859  lgslem4  15876  lgsdirprm  15907  gausslemma2dlem0a  15922  gausslemma2dlem0f  15927  gausslemma2dlem0i  15930  gausslemma2dlem1a  15931  gausslemma2dlem1cl  15932  gausslemma2dlem5  15939  gausslemma2dlem6  15940  gausslemma2d  15942  lgseisenlem1  15943  lgseisenlem2  15944  lgseisenlem3  15945  lgseisen  15947  lgsquadlem1  15950  m1lgs  15958  2lgslem1a  15961  2lgslem1c  15963  2lgsoddprmlem2  15979  edgval  16055  edgstruct  16059  umgrnloopv  16109  umgredgprv  16110  upgr1edc  16116  umgredgne  16145  usgredgssen  16157  umgr2edg1  16204  uspgredg2vlem  16215  uspgr1edc  16235  uhgrspansubgrlem  16271  wlkm  16334  wlkvtxiedg  16340  wlkvtxiedgg  16341  wlk1walkdom  16354  g0wlk0  16365  wlkres  16374  trlf1  16383  trlreslem  16384  trlres  16385  clwwlkg  16388  clwwlkccatlem  16395  clwwlknon  16424  eupthfi  16446  eupthseg  16447  eupthres  16452  trlsegvdeglem1  16455  trlsegvdeglem7  16461  trlsegvdegfi  16462  eupth2lem3lem2fi  16464  eupth2lem3lem3fi  16465  eupth2lem3lem6fi  16466  eupth2lem3lem4fi  16468  eupth2lem3lem7fi  16469  eupth2lem3fi  16471  eupth2lemsfi  16473  eupth2fi  16474  konigsbergssiedgwen  16481  bj-inex  16677  bj-sucexg  16692  bj-peano4  16725  setindis  16737  bdsetindis  16739  bj-inf2vnlem1  16740  nnsf  16783  nninfall  16787  nninfsellemeq  16792  sbthom  16806  gfsumval  16862