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  390  hbim  1598  nfal  1629  19.9hd  1714  equsexd  1782  sbcof2  1863  aev  1865  sbequi  1892  nfsbd  2037  mo2n  2114  eupickb  2168  r19.29af2  2691  spc2gv  2916  spc3gv  2918  eqvincg  2950  sbcco3g  3205  ssrmof  3311  exmidsssnc  4335  exmid1stab  4340  snelpwi  4346  opth1  4371  frind  4492  onin  4526  abnexg  4587  reusv1  4599  xpexg  4884  reldmm  4995  dmexg  5041  rnexg  5042  elrelimasn  5148  relfld  5311  funimaexglem  5459  funimaexg  5460  fabexg  5574  fsnd  5679  elfvm  5723  nfvres  5726  funimass4  5747  elfvmptrab1  5794  funconstss  5818  f1oresrab  5864  resfunexg  5927  f1eqcocnv  5987  isores1  6010  isoini  6014  isose  6017  isopolem  6018  isosolem  6020  eusvobj2  6061  acexmidlemcase  6070  oprabid  6107  offval  6300  resfunexgALT  6327  offval3  6357  1stvalg  6366  2ndvalg  6367  1stcof  6387  2ndcof  6388  cnvf1o  6451  tposf12  6530  smores3  6554  smoiso  6563  tfr0dm  6583  tfrlemibxssdm  6588  tfrlemi14d  6594  tfrexlem  6595  tfr1onlemssrecs  6600  tfr1onlemsucfn  6601  tfr1onlemsucaccv  6602  tfr1onlembxssdm  6604  tfr1onlemres  6610  tfri1dALT  6612  tfrcllemssrecs  6613  tfrcllemsucfn  6614  tfrcllemsucaccv  6615  tfrcllembxssdm  6617  tfrcllemres  6623  rdgss  6644  nnsucsssuc  6755  nntr2  6766  swoord1  6826  swoord2  6827  iinerm  6871  eroveu  6890  pmresg  6947  en1uniel  7081  dom1o  7106  pw2f1odclem  7124  fopwdom  7126  xpen  7135  mapunen  7141  ssenen  7142  isinfinf  7191  ac6sfi  7192  preimaf1ofi  7258  sbthlem1  7264  fczfsuppd  7287  fi0  7299  fiss  7301  supubti  7329  suplubti  7330  isotilem  7336  supisolem  7338  supisoex  7339  supisoti  7340  ordiso2  7365  eldju1st  7401  eldju2ndl  7402  updjud  7412  djudom  7423  ctmlemr  7438  enumctlemm  7444  nnnninfeq  7458  ctssexmid  7480  nninfwlpoimlemginf  7506  exmidonfinlem  7535  en2other2  7538  exmidaclem  7554  cc2lem  7622  cc3  7624  addclnq  7732  mulclnq  7733  1qec  7745  prarloclemarch2  7776  enq0tr  7791  addclnq0  7808  mulclnq0  7809  nq0m0r  7813  prarloclemlo  7851  prarloc  7860  genpml  7874  genpmu  7875  addnqprl  7886  addnqpru  7887  recnnpr  7905  prmuloc2  7924  1idpru  7948  ltexprlemm  7957  ltexprlemloc  7964  recexprlemm  7981  recexprlem1ssl  7990  caucvgprlemnkj  8023  caucvgprlemnbj  8024  caucvgprlemm  8025  caucvgprlemopl  8026  caucvgprlemlol  8027  caucvgprlemladdfu  8034  caucvgprlemladdrl  8035  caucvgprprlemk  8040  caucvgprprlemloccalc  8041  caucvgprprlemnkltj  8046  caucvgprprlemnjltk  8048  caucvgprprlemml  8051  caucvgprprlemmu  8052  caucvgprprlemlol  8055  caucvgprprlemexb  8064  caucvgprprlem1  8066  suplocexprlemml  8073  suplocexprlemlub  8081  addclsr  8110  mulclsr  8111  prsrcl  8141  caucvgsrlemoffcau  8155  peano5nnnn  8249  mulap0r  8933  nn1suc  9302  prime  9724  zindd  9743  xrlttri3  10178  xnn0xadd0  10248  fzopth  10445  fzsuc  10453  fzpred  10455  fzp1ss  10458  fztp  10463  fseq1p1m1  10479  1fv  10524  elfzom1elp1fzo  10598  ssfzo12  10620  fzosplitsn  10629  zsupcllemstep  10640  zsupcllemex  10641  infssuzledc  10645  divfl0  10709  fldiv4lem1div2uz2  10719  modqid  10764  modqmuladdim  10782  frecuzrdgtcl  10827  frecuzrdgfunlem  10834  frecfzennn  10841  frecfzen2  10842  seq3val  10875  seqvalcd  10876  seqsplitg  10904  iseqf1olemqcl  10914  iseqf1olemnab  10916  iseqf1olemmo  10920  iseqf1olemqk  10922  seq3f1olemstep  10929  seqf1oglem2  10935  seq3id3  10939  seqhomog  10945  faclbnd  11157  faclbnd3  11159  bcm1k  11176  hashfz1  11200  hashfz  11240  hashfzp1  11243  fiubm  11249  hashfacen  11262  leisorel  11267  wrdexb  11294  wrdsymb  11310  wrdred1hash  11326  lsw0  11330  lswex  11334  ccat0  11342  ccatval2  11344  ccatw2s1leng  11384  ccats1val2  11386  swrds1  11418  swrdlsw  11419  ccats1pfxeqrex  11465  pfxccatin12lem1  11478  swrdccatin2  11479  swrdccat  11485  cats1fvd  11516  s1s2d  11544  s1s3d  11545  cjcj  11626  caucvgre  11725  r19.2uz  11737  resqrexlemgt0  11764  ltabs  11831  xrmaxiflemab  11991  xrmaxiflemlub  11992  nnf1o  12121  summodclem2a  12126  fsumf1o  12135  fisum0diag2  12192  modfsummodlemstep  12202  fsumparts  12215  clim2prod  12284  prodfap0  12290  prodmodclem2a  12321  fprodssdc  12335  fprodcllem  12351  ef0lem  12405  resinval  12460  recosval  12461  demoivreALT  12519  nn0o  12652  gcdmultiplez  12776  dvdssq  12786  nninfct  12796  eucalg  12815  lcmgcdnn  12838  dvdsnprmd  12881  prm2orodd  12882  isprm5lem  12897  qnumdenbi  12948  nn0gcdsq  12956  phibnd  12973  hashdvds  12977  phimullem  12981  prmdiveq  12992  hashgcdlem  12994  modprm0  13011  nnnn0modprm0  13012  modprmn0modprm0  13013  oddprm  13016  prm23lt5  13020  pcprendvds  13047  pcidlem  13080  pcmpt  13100  pcfac  13107  infpnlem2  13117  prmunb  13119  1arith  13124  4sqlem19  13166  ballotfilemfp1  13209  ballotfilemic  13228  ballotfilem1c  13229  ballotfilemsima  13237  ballotfilemrv  13241  ballotfilemro  13244  ballotfilemfrc  13248  ballotfilemfrci  13249  ballotfilemfrceq  13250  ballotfilemfrcn0  13251  ballotfilemrinv0  13254  unennn  13266  ennnfonelemk  13269  ennnfonelemjn  13271  ennnfonelemhf1o  13282  ennnfonelemex  13283  ennnfonelemf1  13287  ennnfonelemrn  13288  qnnen  13300  unbendc  13323  setsfun0  13366  srngbased  13478  srngplusgd  13479  srngmulrd  13480  srnginvld  13481  lmodbased  13496  lmodplusgd  13497  lmodscad  13498  lmodvscad  13499  ipsbased  13508  ipsaddgd  13509  ipsmulrd  13510  ipsscad  13511  ipsvscad  13512  ipsipd  13513  tgval  13593  gzsumval2  13691  isnsgrp  13698  ismnd  13709  dfgrp2e  13810  subgintm  13978  eqg0el  14009  ecqusaddcl  14019  kerf1ghm  14054  gzsumconst  14120  gsumvalfi  14129  gsumf1ofi  14137  prdsbas3  14164  imasrng  14230  srgisid  14264  qusring2  14344  oppr1g  14361  dvdsr02  14385  isunitd  14386  crngunit  14391  unitpropdg  14428  elrhmunit  14457  subrngintm  14493  subrguss  14517  subrgunit  14520  subrgugrp  14521  subrgintm  14524  drngunz  14591  lmodfopnelem1  14633  rmodislmodlem  14659  rmodislmod  14660  lssuni  14672  islss3  14688  lss0v  14739  sraval  14746  rnglidlmmgm  14805  2idllidld  14815  2idlridld  14816  rng2idl0  14828  rng2idlsubg0  14831  zrh0  14932  znle  14944  zndvds0  14957  znf1o  14958  znleval  14960  znfi  14962  znhash  14963  znunit  14966  psrbaglecl  14983  psrbasg  14988  psradd  14993  psr0cl  14995  mpladd  15018  cldval  15123  ntrfval  15124  clsfval  15125  neifval  15164  neif  15165  neival  15167  cnclima  15247  cncnpi  15252  cnrest2  15260  cnrest2r  15261  cnptoprest  15263  cnpdis  15266  txvalex  15278  txval  15279  txcnmpt  15297  txdis  15301  cnmpt1t  15309  cnmpt2t  15317  hmeocnv  15331  hmeontr  15337  txhmeo  15343  xmetunirn  15382  xmettpos  15394  metn0  15402  xmetres  15406  metres  15407  blrnps  15435  blrn  15436  blin2  15456  blbas  15457  xmeterval  15459  xmettxlem  15533  xmettx  15534  metcnpi  15539  reldvg  15703  dvaddxx  15727  dvmulxx  15728  dviaddf  15729  dvimulf  15730  dvfre  15734  dvmptid  15740  dveflem  15750  elply2  15759  plyreres  15788  sinq12gt0  15854  logfac  15918  rprelogbdiv  15982  logbgcd1irr  15992  fsumdvdsmul  16019  lgslem4  16036  lgsdirprm  16067  gausslemma2dlem0a  16082  gausslemma2dlem0f  16087  gausslemma2dlem0i  16090  gausslemma2dlem1a  16091  gausslemma2dlem1cl  16092  gausslemma2dlem5  16099  gausslemma2dlem6  16100  gausslemma2d  16102  lgseisenlem1  16103  lgseisenlem2  16104  lgseisenlem3  16105  lgseisen  16107  lgsquadlem1  16110  m1lgs  16118  2lgslem1a  16121  2lgslem1c  16123  2lgsoddprmlem2  16139  edgval  16215  edgstruct  16219  umgrnloopv  16269  umgredgprv  16270  upgr1edc  16276  umgredgne  16305  usgredgssen  16317  umgr2edg1  16364  uspgredg2vlem  16375  uspgr1edc  16395  uhgrspansubgrlem  16431  wlkm  16494  wlkvtxiedg  16500  wlkvtxiedgg  16501  wlk1walkdom  16514  g0wlk0  16525  wlkres  16534  trlf1  16543  trlreslem  16544  trlres  16545  clwwlkg  16548  clwwlkccatlem  16555  clwwlknon  16584  eupthfi  16606  eupthseg  16607  eupthres  16612  trlsegvdeglem1  16615  trlsegvdeglem7  16621  trlsegvdegfi  16622  eupth2lem3lem2fi  16624  eupth2lem3lem3fi  16625  eupth2lem3lem6fi  16626  eupth2lem3lem4fi  16628  eupth2lem3lem7fi  16629  eupth2lem3fi  16631  eupth2lemsfi  16633  eupth2fi  16634  konigsbergssiedgwen  16641  bj-inex  16847  bj-sucexg  16862  bj-peano4  16895  setindis  16907  bdsetindis  16909  bj-inf2vnlem1  16910  nnsf  16953  nninfall  16957  nninfsellemeq  16962  sbthom  16976