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  1559  nfal  1590  19.9hd  1676  equsexd  1743  sbcof2  1824  aev  1826  sbequi  1853  nfsbd  1996  mo2n  2073  eupickb  2126  r19.29af2  2637  spc2gv  2855  spc3gv  2857  eqvincg  2888  sbcco3g  3142  ssrmof  3247  exmidsssnc  4237  exmid1stab  4242  snelpwi  4246  opth1  4270  frind  4388  onin  4422  abnexg  4482  reusv1  4494  xpexg  4778  dmexg  4931  rnexg  4932  elrelimasn  5036  relfld  5199  funimaexglem  5342  funimaexg  5343  fabexg  5446  fsnd  5548  elfvm  5592  nfvres  5593  funimass4  5612  elfvmptrab1  5657  funconstss  5681  f1oresrab  5728  resfunexg  5784  f1eqcocnv  5839  isores1  5862  isoini  5866  isose  5869  isopolem  5870  isosolem  5872  eusvobj2  5909  acexmidlemcase  5918  oprabid  5955  offval  6145  resfunexgALT  6167  offval3  6193  1stvalg  6202  2ndvalg  6203  1stcof  6223  2ndcof  6224  cnvf1o  6285  tposf12  6329  smores3  6353  smoiso  6362  tfr0dm  6382  tfrlemibxssdm  6387  tfrlemi14d  6393  tfrexlem  6394  tfr1onlemssrecs  6399  tfr1onlemsucfn  6400  tfr1onlemsucaccv  6401  tfr1onlembxssdm  6403  tfr1onlemres  6409  tfri1dALT  6411  tfrcllemssrecs  6412  tfrcllemsucfn  6413  tfrcllemsucaccv  6414  tfrcllembxssdm  6416  tfrcllemres  6422  rdgss  6443  nnsucsssuc  6552  nntr2  6563  swoord1  6623  swoord2  6624  iinerm  6668  eroveu  6687  pmresg  6737  en1uniel  6865  pw2f1odclem  6897  fopwdom  6899  xpen  6908  ssenen  6914  isinfinf  6960  ac6sfi  6961  preimaf1ofi  7019  sbthlem1  7025  fi0  7043  fiss  7045  supubti  7067  suplubti  7068  isotilem  7074  supisolem  7076  supisoex  7077  supisoti  7078  ordiso2  7103  eldju1st  7139  eldju2ndl  7140  updjud  7150  djudom  7161  ctmlemr  7176  enumctlemm  7182  nnnninfeq  7196  ctssexmid  7218  nninfwlpoimlemginf  7244  exmidonfinlem  7263  en2other2  7266  exmidaclem  7278  cc2lem  7336  cc3  7338  addclnq  7445  mulclnq  7446  1qec  7458  prarloclemarch2  7489  enq0tr  7504  addclnq0  7521  mulclnq0  7522  nq0m0r  7526  prarloclemlo  7564  prarloc  7573  genpml  7587  genpmu  7588  addnqprl  7599  addnqpru  7600  recnnpr  7618  prmuloc2  7637  1idpru  7661  ltexprlemm  7670  ltexprlemloc  7677  recexprlemm  7694  recexprlem1ssl  7703  caucvgprlemnkj  7736  caucvgprlemnbj  7737  caucvgprlemm  7738  caucvgprlemopl  7739  caucvgprlemlol  7740  caucvgprlemladdfu  7747  caucvgprlemladdrl  7748  caucvgprprlemk  7753  caucvgprprlemloccalc  7754  caucvgprprlemnkltj  7759  caucvgprprlemnjltk  7761  caucvgprprlemml  7764  caucvgprprlemmu  7765  caucvgprprlemlol  7768  caucvgprprlemexb  7777  caucvgprprlem1  7779  suplocexprlemml  7786  suplocexprlemlub  7794  addclsr  7823  mulclsr  7824  prsrcl  7854  caucvgsrlemoffcau  7868  peano5nnnn  7962  mulap0r  8645  nn1suc  9012  prime  9428  zindd  9447  xrlttri3  9875  xnn0xadd0  9945  fzopth  10139  fzsuc  10147  fzpred  10148  fzp1ss  10151  fztp  10156  fseq1p1m1  10172  1fv  10217  elfzom1elp1fzo  10281  ssfzo12  10303  fzosplitsn  10312  zsupcllemstep  10322  zsupcllemex  10323  infssuzledc  10327  divfl0  10389  fldiv4lem1div2uz2  10399  modqid  10444  modqmuladdim  10462  frecuzrdgtcl  10507  frecuzrdgfunlem  10514  frecfzennn  10521  frecfzen2  10522  seq3val  10555  seqvalcd  10556  seqsplitg  10584  iseqf1olemqcl  10594  iseqf1olemnab  10596  iseqf1olemmo  10600  iseqf1olemqk  10602  seq3f1olemstep  10609  seqf1oglem2  10615  seq3id3  10619  seqhomog  10625  faclbnd  10836  faclbnd3  10838  bcm1k  10855  hashfz1  10878  hashfz  10916  hashfzp1  10919  fiubm  10923  hashfacen  10931  leisorel  10932  wrdexb  10950  wrdsymb  10965  wrdred1hash  10981  cjcj  11051  caucvgre  11149  r19.2uz  11161  resqrexlemgt0  11188  ltabs  11255  xrmaxiflemab  11415  xrmaxiflemlub  11416  nnf1o  11544  summodclem2a  11549  fsumf1o  11558  fisum0diag2  11615  modfsummodlemstep  11625  fsumparts  11638  clim2prod  11707  prodfap0  11713  prodmodclem2a  11744  fprodssdc  11758  fprodcllem  11774  ef0lem  11828  resinval  11883  recosval  11884  demoivreALT  11942  nn0o  12075  gcdmultiplez  12199  dvdssq  12209  nninfct  12219  eucalg  12238  lcmgcdnn  12261  dvdsnprmd  12304  prm2orodd  12305  isprm5lem  12320  qnumdenbi  12371  nn0gcdsq  12379  phibnd  12396  hashdvds  12400  phimullem  12404  prmdiveq  12415  hashgcdlem  12417  modprm0  12434  nnnn0modprm0  12435  modprmn0modprm0  12436  oddprm  12439  prm23lt5  12443  pcprendvds  12470  pcidlem  12503  pcmpt  12523  pcfac  12530  infpnlem2  12540  prmunb  12542  1arith  12547  4sqlem19  12589  unennn  12625  ennnfonelemk  12628  ennnfonelemjn  12630  ennnfonelemhf1o  12641  ennnfonelemex  12642  ennnfonelemf1  12646  ennnfonelemrn  12647  qnnen  12659  unbendc  12682  setsfun0  12725  srngbased  12835  srngplusgd  12836  srngmulrd  12837  srnginvld  12838  lmodbased  12853  lmodplusgd  12854  lmodscad  12855  lmodvscad  12856  ipsbased  12865  ipsaddgd  12866  ipsmulrd  12867  ipsscad  12868  ipsvscad  12869  ipsipd  12870  tgval  12950  isnsgrp  13075  ismnd  13086  dfgrp2e  13186  subgintm  13354  eqg0el  13385  ecqusaddcl  13395  kerf1ghm  13430  gsumfzconst  13497  imasrng  13538  srgisid  13568  srg1zr  13569  qusring2  13648  oppr1g  13664  dvdsr02  13687  isunitd  13688  crngunit  13693  unitpropdg  13730  elrhmunit  13759  subrngintm  13794  subrguss  13818  subrgunit  13821  subrgugrp  13822  subrgintm  13825  lmodfopnelem1  13906  rmodislmodlem  13932  rmodislmod  13933  lssuni  13945  islss3  13961  lss0v  14012  sraval  14019  rnglidlmmgm  14078  2idllidld  14088  2idlridld  14089  rng2idl0  14101  rng2idlsubg0  14104  zrh0  14207  znle  14219  zndvds0  14232  znf1o  14233  znleval  14235  znfi  14237  znhash  14238  znunit  14241  psrbasg  14253  psradd  14257  cldval  14361  ntrfval  14362  clsfval  14363  neifval  14402  neif  14403  neival  14405  cnclima  14485  cncnpi  14490  cnrest2  14498  cnrest2r  14499  cnptoprest  14501  cnpdis  14504  txvalex  14516  txval  14517  txcnmpt  14535  txdis  14539  cnmpt1t  14547  cnmpt2t  14555  hmeocnv  14569  hmeontr  14575  txhmeo  14581  xmetunirn  14620  xmettpos  14632  metn0  14640  xmetres  14644  metres  14645  blrnps  14673  blrn  14674  blin2  14694  blbas  14695  xmeterval  14697  xmettxlem  14771  xmettx  14772  metcnpi  14777  reldvg  14941  dvaddxx  14965  dvmulxx  14966  dviaddf  14967  dvimulf  14968  dvfre  14972  dvmptid  14978  dveflem  14988  elply2  14997  plyreres  15026  sinq12gt0  15092  rprelogbdiv  15219  logbgcd1irr  15229  fsumdvdsmul  15253  lgslem4  15270  lgsdirprm  15301  gausslemma2dlem0a  15316  gausslemma2dlem0f  15321  gausslemma2dlem0i  15324  gausslemma2dlem1a  15325  gausslemma2dlem1cl  15326  gausslemma2dlem5  15333  gausslemma2dlem6  15334  gausslemma2d  15336  lgseisenlem1  15337  lgseisenlem2  15338  lgseisenlem3  15339  lgseisen  15341  lgsquadlem1  15344  m1lgs  15352  2lgslem1a  15355  2lgslem1c  15357  2lgsoddprmlem2  15373  bj-inex  15579  bj-sucexg  15594  bj-peano4  15627  setindis  15639  bdsetindis  15641  bj-inf2vnlem1  15642  nnsf  15678  nninfall  15682  nninfsellemeq  15687  sbthom  15699