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  1777  sbcof2  1858  aev  1860  sbequi  1887  nfsbd  2030  mo2n  2107  eupickb  2161  r19.29af2  2674  spc2gv  2898  spc3gv  2900  eqvincg  2931  sbcco3g  3186  ssrmof  3291  exmidsssnc  4299  exmid1stab  4304  snelpwi  4309  opth1  4334  frind  4455  onin  4489  abnexg  4549  reusv1  4561  xpexg  4846  reldmm  4956  dmexg  5002  rnexg  5003  elrelimasn  5109  relfld  5272  funimaexglem  5420  funimaexg  5421  fabexg  5532  fsnd  5637  elfvm  5681  nfvres  5684  funimass4  5705  elfvmptrab1  5750  funconstss  5774  f1oresrab  5820  resfunexg  5883  f1eqcocnv  5942  isores1  5965  isoini  5969  isose  5972  isopolem  5973  isosolem  5975  eusvobj2  6014  acexmidlemcase  6023  oprabid  6060  offval  6252  resfunexgALT  6279  offval3  6305  1stvalg  6314  2ndvalg  6315  1stcof  6335  2ndcof  6336  cnvf1o  6399  tposf12  6478  smores3  6502  smoiso  6511  tfr0dm  6531  tfrlemibxssdm  6536  tfrlemi14d  6542  tfrexlem  6543  tfr1onlemssrecs  6548  tfr1onlemsucfn  6549  tfr1onlemsucaccv  6550  tfr1onlembxssdm  6552  tfr1onlemres  6558  tfri1dALT  6560  tfrcllemssrecs  6561  tfrcllemsucfn  6562  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllemres  6571  rdgss  6592  nnsucsssuc  6703  nntr2  6714  swoord1  6774  swoord2  6775  iinerm  6819  eroveu  6838  pmresg  6888  en1uniel  7021  dom1o  7045  pw2f1odclem  7063  fopwdom  7065  xpen  7074  ssenen  7080  isinfinf  7129  ac6sfi  7130  preimaf1ofi  7193  sbthlem1  7199  fi0  7217  fiss  7219  supubti  7241  suplubti  7242  isotilem  7248  supisolem  7250  supisoex  7251  supisoti  7252  ordiso2  7277  eldju1st  7313  eldju2ndl  7314  updjud  7324  djudom  7335  ctmlemr  7350  enumctlemm  7356  nnnninfeq  7370  ctssexmid  7392  nninfwlpoimlemginf  7418  exmidonfinlem  7447  en2other2  7450  exmidaclem  7466  cc2lem  7528  cc3  7530  addclnq  7638  mulclnq  7639  1qec  7651  prarloclemarch2  7682  enq0tr  7697  addclnq0  7714  mulclnq0  7715  nq0m0r  7719  prarloclemlo  7757  prarloc  7766  genpml  7780  genpmu  7781  addnqprl  7792  addnqpru  7793  recnnpr  7811  prmuloc2  7830  1idpru  7854  ltexprlemm  7863  ltexprlemloc  7870  recexprlemm  7887  recexprlem1ssl  7896  caucvgprlemnkj  7929  caucvgprlemnbj  7930  caucvgprlemm  7931  caucvgprlemopl  7932  caucvgprlemlol  7933  caucvgprlemladdfu  7940  caucvgprlemladdrl  7941  caucvgprprlemk  7946  caucvgprprlemloccalc  7947  caucvgprprlemnkltj  7952  caucvgprprlemnjltk  7954  caucvgprprlemml  7957  caucvgprprlemmu  7958  caucvgprprlemlol  7961  caucvgprprlemexb  7970  caucvgprprlem1  7972  suplocexprlemml  7979  suplocexprlemlub  7987  addclsr  8016  mulclsr  8017  prsrcl  8047  caucvgsrlemoffcau  8061  peano5nnnn  8155  mulap0r  8837  nn1suc  9204  prime  9623  zindd  9642  xrlttri3  10076  xnn0xadd0  10146  fzopth  10341  fzsuc  10349  fzpred  10350  fzp1ss  10353  fztp  10358  fseq1p1m1  10374  1fv  10419  elfzom1elp1fzo  10493  ssfzo12  10515  fzosplitsn  10524  zsupcllemstep  10535  zsupcllemex  10536  infssuzledc  10540  divfl0  10602  fldiv4lem1div2uz2  10612  modqid  10657  modqmuladdim  10675  frecuzrdgtcl  10720  frecuzrdgfunlem  10727  frecfzennn  10734  frecfzen2  10735  seq3val  10768  seqvalcd  10769  seqsplitg  10797  iseqf1olemqcl  10807  iseqf1olemnab  10809  iseqf1olemmo  10813  iseqf1olemqk  10815  seq3f1olemstep  10822  seqf1oglem2  10828  seq3id3  10832  seqhomog  10838  faclbnd  11049  faclbnd3  11051  bcm1k  11068  hashfz1  11091  hashfz  11131  hashfzp1  11134  fiubm  11138  hashfacen  11146  leisorel  11147  wrdexb  11174  wrdsymb  11190  wrdred1hash  11206  lsw0  11210  lswex  11214  ccat0  11222  ccatval2  11224  ccatw2s1leng  11264  ccats1val2  11266  swrds1  11298  swrdlsw  11299  ccats1pfxeqrex  11345  pfxccatin12lem1  11358  swrdccatin2  11359  swrdccat  11365  cats1fvd  11396  s1s2d  11424  s1s3d  11425  cjcj  11506  caucvgre  11604  r19.2uz  11616  resqrexlemgt0  11643  ltabs  11710  xrmaxiflemab  11870  xrmaxiflemlub  11871  nnf1o  12000  summodclem2a  12005  fsumf1o  12014  fisum0diag2  12071  modfsummodlemstep  12081  fsumparts  12094  clim2prod  12163  prodfap0  12169  prodmodclem2a  12200  fprodssdc  12214  fprodcllem  12230  ef0lem  12284  resinval  12339  recosval  12340  demoivreALT  12398  nn0o  12531  gcdmultiplez  12655  dvdssq  12665  nninfct  12675  eucalg  12694  lcmgcdnn  12717  dvdsnprmd  12760  prm2orodd  12761  isprm5lem  12776  qnumdenbi  12827  nn0gcdsq  12835  phibnd  12852  hashdvds  12856  phimullem  12860  prmdiveq  12871  hashgcdlem  12873  modprm0  12890  nnnn0modprm0  12891  modprmn0modprm0  12892  oddprm  12895  prm23lt5  12899  pcprendvds  12926  pcidlem  12959  pcmpt  12979  pcfac  12986  infpnlem2  12996  prmunb  12998  1arith  13003  4sqlem19  13045  unennn  13081  ennnfonelemk  13084  ennnfonelemjn  13086  ennnfonelemhf1o  13097  ennnfonelemex  13098  ennnfonelemf1  13102  ennnfonelemrn  13103  qnnen  13115  unbendc  13138  setsfun0  13181  srngbased  13293  srngplusgd  13294  srngmulrd  13295  srnginvld  13296  lmodbased  13311  lmodplusgd  13312  lmodscad  13313  lmodvscad  13314  ipsbased  13323  ipsaddgd  13324  ipsmulrd  13325  ipsscad  13326  ipsvscad  13327  ipsipd  13328  tgval  13408  prdsbas3  13433  isnsgrp  13552  ismnd  13565  dfgrp2e  13674  subgintm  13848  eqg0el  13879  ecqusaddcl  13889  kerf1ghm  13924  gsumfzconst  13991  imasrng  14033  srgisid  14063  srg1zr  14064  qusring2  14143  oppr1g  14159  dvdsr02  14183  isunitd  14184  crngunit  14189  unitpropdg  14226  elrhmunit  14255  subrngintm  14290  subrguss  14314  subrgunit  14317  subrgugrp  14318  subrgintm  14321  lmodfopnelem1  14403  rmodislmodlem  14429  rmodislmod  14430  lssuni  14442  islss3  14458  lss0v  14509  sraval  14516  rnglidlmmgm  14575  2idllidld  14585  2idlridld  14586  rng2idl0  14598  rng2idlsubg0  14601  zrh0  14704  znle  14716  zndvds0  14729  znf1o  14730  znleval  14732  znfi  14734  znhash  14735  znunit  14738  psrbaglecl  14754  psrbasg  14758  psradd  14763  psr0cl  14765  mpladd  14788  cldval  14893  ntrfval  14894  clsfval  14895  neifval  14934  neif  14935  neival  14937  cnclima  15017  cncnpi  15022  cnrest2  15030  cnrest2r  15031  cnptoprest  15033  cnpdis  15036  txvalex  15048  txval  15049  txcnmpt  15067  txdis  15071  cnmpt1t  15079  cnmpt2t  15087  hmeocnv  15101  hmeontr  15107  txhmeo  15113  xmetunirn  15152  xmettpos  15164  metn0  15172  xmetres  15176  metres  15177  blrnps  15205  blrn  15206  blin2  15226  blbas  15227  xmeterval  15229  xmettxlem  15303  xmettx  15304  metcnpi  15309  reldvg  15473  dvaddxx  15497  dvmulxx  15498  dviaddf  15499  dvimulf  15500  dvfre  15504  dvmptid  15510  dveflem  15520  elply2  15529  plyreres  15558  sinq12gt0  15624  rprelogbdiv  15751  logbgcd1irr  15761  fsumdvdsmul  15788  lgslem4  15805  lgsdirprm  15836  gausslemma2dlem0a  15851  gausslemma2dlem0f  15856  gausslemma2dlem0i  15859  gausslemma2dlem1a  15860  gausslemma2dlem1cl  15861  gausslemma2dlem5  15868  gausslemma2dlem6  15869  gausslemma2d  15871  lgseisenlem1  15872  lgseisenlem2  15873  lgseisenlem3  15874  lgseisen  15876  lgsquadlem1  15879  m1lgs  15887  2lgslem1a  15890  2lgslem1c  15892  2lgsoddprmlem2  15908  edgval  15984  edgstruct  15988  umgrnloopv  16038  umgredgprv  16039  upgr1edc  16045  umgredgne  16074  usgredgssen  16086  umgr2edg1  16133  uspgredg2vlem  16144  uspgr1edc  16164  uhgrspansubgrlem  16200  wlkm  16263  wlkvtxiedg  16269  wlkvtxiedgg  16270  wlk1walkdom  16283  g0wlk0  16294  wlkres  16303  trlf1  16312  trlreslem  16313  trlres  16314  clwwlkg  16317  clwwlkccatlem  16324  clwwlknon  16353  eupthfi  16375  eupthseg  16376  eupthres  16381  trlsegvdeglem1  16384  trlsegvdeglem7  16390  trlsegvdegfi  16391  eupth2lem3lem2fi  16393  eupth2lem3lem3fi  16394  eupth2lem3lem6fi  16395  eupth2lem3lem4fi  16397  eupth2lem3lem7fi  16398  eupth2lem3fi  16400  eupth2lemsfi  16402  eupth2fi  16403  konigsbergssiedgwen  16410  bj-inex  16606  bj-sucexg  16621  bj-peano4  16654  setindis  16666  bdsetindis  16668  bj-inf2vnlem1  16669  nnsf  16714  nninfall  16718  nninfsellemeq  16723  sbthom  16737  gfsumval  16792