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  1989  mo2n  2066  eupickb  2119  r19.29af2  2630  spc2gv  2843  spc3gv  2845  eqvincg  2876  sbcco3g  3129  ssrmof  3233  exmidsssnc  4221  exmid1stab  4226  snelpwi  4230  opth1  4254  frind  4370  onin  4404  abnexg  4464  reusv1  4476  xpexg  4758  dmexg  4909  rnexg  4910  elrelimasn  5012  relfld  5175  funimaexglem  5318  funimaexg  5319  fabexg  5422  fsnd  5523  nfvres  5567  funimass4  5586  elfvmptrab1  5630  funconstss  5654  f1oresrab  5701  resfunexg  5757  f1eqcocnv  5812  isores1  5835  isoini  5839  isose  5842  isopolem  5843  isosolem  5845  eusvobj2  5881  acexmidlemcase  5890  oprabid  5927  offval  6113  resfunexgALT  6132  offval3  6158  1stvalg  6166  2ndvalg  6167  1stcof  6187  2ndcof  6188  cnvf1o  6249  tposf12  6293  smores3  6317  smoiso  6326  tfr0dm  6346  tfrlemibxssdm  6351  tfrlemi14d  6357  tfrexlem  6358  tfr1onlemssrecs  6363  tfr1onlemsucfn  6364  tfr1onlemsucaccv  6365  tfr1onlembxssdm  6367  tfr1onlemres  6373  tfri1dALT  6375  tfrcllemssrecs  6376  tfrcllemsucfn  6377  tfrcllemsucaccv  6378  tfrcllembxssdm  6380  tfrcllemres  6386  rdgss  6407  nnsucsssuc  6516  nntr2  6527  swoord1  6587  swoord2  6588  iinerm  6632  eroveu  6651  pmresg  6701  en1uniel  6829  pw2f1odclem  6861  fopwdom  6863  xpen  6872  ssenen  6878  isinfinf  6924  ac6sfi  6925  preimaf1ofi  6979  sbthlem1  6985  fi0  7003  fiss  7005  supubti  7027  suplubti  7028  isotilem  7034  supisolem  7036  supisoex  7037  supisoti  7038  ordiso2  7063  eldju1st  7099  eldju2ndl  7100  updjud  7110  djudom  7121  ctmlemr  7136  enumctlemm  7142  nnnninfeq  7155  ctssexmid  7177  nninfwlpoimlemginf  7203  exmidonfinlem  7221  en2other2  7224  exmidaclem  7236  cc2lem  7294  cc3  7296  addclnq  7403  mulclnq  7404  1qec  7416  prarloclemarch2  7447  enq0tr  7462  addclnq0  7479  mulclnq0  7480  nq0m0r  7484  prarloclemlo  7522  prarloc  7531  genpml  7545  genpmu  7546  addnqprl  7557  addnqpru  7558  recnnpr  7576  prmuloc2  7595  1idpru  7619  ltexprlemm  7628  ltexprlemloc  7635  recexprlemm  7652  recexprlem1ssl  7661  caucvgprlemnkj  7694  caucvgprlemnbj  7695  caucvgprlemm  7696  caucvgprlemopl  7697  caucvgprlemlol  7698  caucvgprlemladdfu  7705  caucvgprlemladdrl  7706  caucvgprprlemk  7711  caucvgprprlemloccalc  7712  caucvgprprlemnkltj  7717  caucvgprprlemnjltk  7719  caucvgprprlemml  7722  caucvgprprlemmu  7723  caucvgprprlemlol  7726  caucvgprprlemexb  7735  caucvgprprlem1  7737  suplocexprlemml  7744  suplocexprlemlub  7752  addclsr  7781  mulclsr  7782  prsrcl  7812  caucvgsrlemoffcau  7826  peano5nnnn  7920  mulap0r  8601  nn1suc  8967  prime  9381  zindd  9400  xrlttri3  9826  xnn0xadd0  9896  fzopth  10090  fzsuc  10098  fzpred  10099  fzp1ss  10102  fztp  10107  fseq1p1m1  10123  1fv  10168  elfzom1elp1fzo  10231  ssfzo12  10253  fzosplitsn  10262  divfl0  10326  modqid  10379  modqmuladdim  10397  frecuzrdgtcl  10442  frecuzrdgfunlem  10449  frecfzennn  10456  frecfzen2  10457  seq3val  10488  seqvalcd  10489  iseqf1olemqcl  10516  iseqf1olemnab  10518  iseqf1olemmo  10522  iseqf1olemqk  10524  seq3f1olemstep  10531  seq3id3  10537  faclbnd  10752  faclbnd3  10754  bcm1k  10771  hashfz1  10794  hashfz  10832  hashfzp1  10835  fiubm  10839  hashfacen  10847  leisorel  10848  cjcj  10923  caucvgre  11021  r19.2uz  11033  resqrexlemgt0  11060  ltabs  11127  xrmaxiflemab  11286  xrmaxiflemlub  11287  nnf1o  11415  summodclem2a  11420  fsumf1o  11429  fisum0diag2  11486  modfsummodlemstep  11496  fsumparts  11509  clim2prod  11578  prodfap0  11584  prodmodclem2a  11615  fprodssdc  11629  fprodcllem  11645  ef0lem  11699  resinval  11754  recosval  11755  demoivreALT  11812  nn0o  11943  zsupcllemstep  11977  zsupcllemex  11978  infssuzledc  11982  gcdmultiplez  12053  dvdssq  12063  eucalg  12090  lcmgcdnn  12113  dvdsnprmd  12156  prm2orodd  12157  isprm5lem  12172  qnumdenbi  12223  nn0gcdsq  12231  phibnd  12248  hashdvds  12252  phimullem  12256  prmdiveq  12267  hashgcdlem  12269  modprm0  12285  nnnn0modprm0  12286  modprmn0modprm0  12287  oddprm  12290  prm23lt5  12294  pcprendvds  12321  pcidlem  12354  pcmpt  12374  pcfac  12381  infpnlem2  12391  prmunb  12393  1arith  12398  4sqlem19  12440  unennn  12447  ennnfonelemk  12450  ennnfonelemjn  12452  ennnfonelemhf1o  12463  ennnfonelemex  12464  ennnfonelemf1  12468  ennnfonelemrn  12469  qnnen  12481  unbendc  12504  setsfun0  12547  srngbased  12655  srngplusgd  12656  srngmulrd  12657  srnginvld  12658  lmodbased  12673  lmodplusgd  12674  lmodscad  12675  lmodvscad  12676  ipsbased  12685  ipsaddgd  12686  ipsmulrd  12687  ipsscad  12688  ipsvscad  12689  ipsipd  12690  tgval  12764  isnsgrp  12866  ismnd  12877  dfgrp2e  12969  subgintm  13134  eqg0el  13165  ecqusaddcl  13175  kerf1ghm  13210  imasrng  13307  srgisid  13337  srg1zr  13338  qusring2  13413  oppr1g  13429  dvdsr02  13452  isunitd  13453  crngunit  13458  unitpropdg  13495  elrhmunit  13524  subrngintm  13556  subrguss  13580  subrgunit  13583  subrgugrp  13584  subrgintm  13587  lmodfopnelem1  13637  rmodislmodlem  13663  rmodislmod  13664  lssuni  13676  islss3  13692  lss0v  13743  sraval  13750  rnglidlmmgm  13809  2idllidld  13818  2idlridld  13819  rng2idl0  13831  rng2idlsubg0  13834  zrh0  13919  znle  13930  psrbasg  13948  cldval  14051  ntrfval  14052  clsfval  14053  neifval  14092  neif  14093  neival  14095  cnclima  14175  cncnpi  14180  cnrest2  14188  cnrest2r  14189  cnptoprest  14191  cnpdis  14194  txvalex  14206  txval  14207  txcnmpt  14225  txdis  14229  cnmpt1t  14237  cnmpt2t  14245  hmeocnv  14259  hmeontr  14265  txhmeo  14271  xmetunirn  14310  xmettpos  14322  metn0  14330  xmetres  14334  metres  14335  blrnps  14363  blrn  14364  blin2  14384  blbas  14385  xmeterval  14387  xmettxlem  14461  xmettx  14462  metcnpi  14467  reldvg  14600  dvaddxx  14619  dvmulxx  14620  dviaddf  14621  dvimulf  14622  dvfre  14626  dveflem  14639  sinq12gt0  14703  rprelogbdiv  14827  logbgcd1irr  14837  lgslem4  14857  lgsdirprm  14888  lgseisenlem1  14903  lgseisenlem2  14904  m1lgs  14905  2lgsoddprmlem2  14907  bj-inex  15112  bj-sucexg  15127  bj-peano4  15160  setindis  15172  bdsetindis  15174  bj-inf2vnlem1  15175  nnsf  15208  nninfall  15212  nninfsellemeq  15217  sbthom  15228