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  1591  nfal  1622  19.9hd  1708  equsexd  1775  sbcof2  1856  aev  1858  sbequi  1885  nfsbd  2028  mo2n  2105  eupickb  2159  r19.29af2  2671  spc2gv  2895  spc3gv  2897  eqvincg  2928  sbcco3g  3183  ssrmof  3288  exmidsssnc  4291  exmid1stab  4296  snelpwi  4301  opth1  4326  frind  4447  onin  4481  abnexg  4541  reusv1  4553  xpexg  4838  reldmm  4948  dmexg  4994  rnexg  4995  elrelimasn  5100  relfld  5263  funimaexglem  5410  funimaexg  5411  fabexg  5521  fsnd  5624  elfvm  5668  nfvres  5671  funimass4  5692  elfvmptrab1  5737  funconstss  5761  f1oresrab  5808  resfunexg  5870  f1eqcocnv  5927  isores1  5950  isoini  5954  isose  5957  isopolem  5958  isosolem  5960  eusvobj2  5999  acexmidlemcase  6008  oprabid  6045  offval  6238  resfunexgALT  6265  offval3  6291  1stvalg  6300  2ndvalg  6301  1stcof  6321  2ndcof  6322  cnvf1o  6385  tposf12  6430  smores3  6454  smoiso  6463  tfr0dm  6483  tfrlemibxssdm  6488  tfrlemi14d  6494  tfrexlem  6495  tfr1onlemssrecs  6500  tfr1onlemsucfn  6501  tfr1onlemsucaccv  6502  tfr1onlembxssdm  6504  tfr1onlemres  6510  tfri1dALT  6512  tfrcllemssrecs  6513  tfrcllemsucfn  6514  tfrcllemsucaccv  6515  tfrcllembxssdm  6517  tfrcllemres  6523  rdgss  6544  nnsucsssuc  6655  nntr2  6666  swoord1  6726  swoord2  6727  iinerm  6771  eroveu  6790  pmresg  6840  en1uniel  6973  dom1o  6997  pw2f1odclem  7015  fopwdom  7017  xpen  7026  ssenen  7032  isinfinf  7079  ac6sfi  7080  preimaf1ofi  7141  sbthlem1  7147  fi0  7165  fiss  7167  supubti  7189  suplubti  7190  isotilem  7196  supisolem  7198  supisoex  7199  supisoti  7200  ordiso2  7225  eldju1st  7261  eldju2ndl  7262  updjud  7272  djudom  7283  ctmlemr  7298  enumctlemm  7304  nnnninfeq  7318  ctssexmid  7340  nninfwlpoimlemginf  7366  exmidonfinlem  7394  en2other2  7397  exmidaclem  7413  cc2lem  7475  cc3  7477  addclnq  7585  mulclnq  7586  1qec  7598  prarloclemarch2  7629  enq0tr  7644  addclnq0  7661  mulclnq0  7662  nq0m0r  7666  prarloclemlo  7704  prarloc  7713  genpml  7727  genpmu  7728  addnqprl  7739  addnqpru  7740  recnnpr  7758  prmuloc2  7777  1idpru  7801  ltexprlemm  7810  ltexprlemloc  7817  recexprlemm  7834  recexprlem1ssl  7843  caucvgprlemnkj  7876  caucvgprlemnbj  7877  caucvgprlemm  7878  caucvgprlemopl  7879  caucvgprlemlol  7880  caucvgprlemladdfu  7887  caucvgprlemladdrl  7888  caucvgprprlemk  7893  caucvgprprlemloccalc  7894  caucvgprprlemnkltj  7899  caucvgprprlemnjltk  7901  caucvgprprlemml  7904  caucvgprprlemmu  7905  caucvgprprlemlol  7908  caucvgprprlemexb  7917  caucvgprprlem1  7919  suplocexprlemml  7926  suplocexprlemlub  7934  addclsr  7963  mulclsr  7964  prsrcl  7994  caucvgsrlemoffcau  8008  peano5nnnn  8102  mulap0r  8785  nn1suc  9152  prime  9569  zindd  9588  xrlttri3  10022  xnn0xadd0  10092  fzopth  10286  fzsuc  10294  fzpred  10295  fzp1ss  10298  fztp  10303  fseq1p1m1  10319  1fv  10364  elfzom1elp1fzo  10437  ssfzo12  10459  fzosplitsn  10468  zsupcllemstep  10479  zsupcllemex  10480  infssuzledc  10484  divfl0  10546  fldiv4lem1div2uz2  10556  modqid  10601  modqmuladdim  10619  frecuzrdgtcl  10664  frecuzrdgfunlem  10671  frecfzennn  10678  frecfzen2  10679  seq3val  10712  seqvalcd  10713  seqsplitg  10741  iseqf1olemqcl  10751  iseqf1olemnab  10753  iseqf1olemmo  10757  iseqf1olemqk  10759  seq3f1olemstep  10766  seqf1oglem2  10772  seq3id3  10776  seqhomog  10782  faclbnd  10993  faclbnd3  10995  bcm1k  11012  hashfz1  11035  hashfz  11075  hashfzp1  11078  fiubm  11082  hashfacen  11090  leisorel  11091  wrdexb  11115  wrdsymb  11131  wrdred1hash  11147  lsw0  11151  lswex  11155  ccat0  11163  ccatval2  11165  ccatw2s1leng  11205  ccats1val2  11207  swrds1  11239  swrdlsw  11240  ccats1pfxeqrex  11286  pfxccatin12lem1  11299  swrdccatin2  11300  swrdccat  11306  cats1fvd  11337  cjcj  11434  caucvgre  11532  r19.2uz  11544  resqrexlemgt0  11571  ltabs  11638  xrmaxiflemab  11798  xrmaxiflemlub  11799  nnf1o  11927  summodclem2a  11932  fsumf1o  11941  fisum0diag2  11998  modfsummodlemstep  12008  fsumparts  12021  clim2prod  12090  prodfap0  12096  prodmodclem2a  12127  fprodssdc  12141  fprodcllem  12157  ef0lem  12211  resinval  12266  recosval  12267  demoivreALT  12325  nn0o  12458  gcdmultiplez  12582  dvdssq  12592  nninfct  12602  eucalg  12621  lcmgcdnn  12644  dvdsnprmd  12687  prm2orodd  12688  isprm5lem  12703  qnumdenbi  12754  nn0gcdsq  12762  phibnd  12779  hashdvds  12783  phimullem  12787  prmdiveq  12798  hashgcdlem  12800  modprm0  12817  nnnn0modprm0  12818  modprmn0modprm0  12819  oddprm  12822  prm23lt5  12826  pcprendvds  12853  pcidlem  12886  pcmpt  12906  pcfac  12913  infpnlem2  12923  prmunb  12925  1arith  12930  4sqlem19  12972  unennn  13008  ennnfonelemk  13011  ennnfonelemjn  13013  ennnfonelemhf1o  13024  ennnfonelemex  13025  ennnfonelemf1  13029  ennnfonelemrn  13030  qnnen  13042  unbendc  13065  setsfun0  13108  srngbased  13220  srngplusgd  13221  srngmulrd  13222  srnginvld  13223  lmodbased  13238  lmodplusgd  13239  lmodscad  13240  lmodvscad  13241  ipsbased  13250  ipsaddgd  13251  ipsmulrd  13252  ipsscad  13253  ipsvscad  13254  ipsipd  13255  tgval  13335  prdsbas3  13360  isnsgrp  13479  ismnd  13492  dfgrp2e  13601  subgintm  13775  eqg0el  13806  ecqusaddcl  13816  kerf1ghm  13851  gsumfzconst  13918  imasrng  13959  srgisid  13989  srg1zr  13990  qusring2  14069  oppr1g  14085  dvdsr02  14109  isunitd  14110  crngunit  14115  unitpropdg  14152  elrhmunit  14181  subrngintm  14216  subrguss  14240  subrgunit  14243  subrgugrp  14244  subrgintm  14247  lmodfopnelem1  14328  rmodislmodlem  14354  rmodislmod  14355  lssuni  14367  islss3  14383  lss0v  14434  sraval  14441  rnglidlmmgm  14500  2idllidld  14510  2idlridld  14511  rng2idl0  14523  rng2idlsubg0  14526  zrh0  14629  znle  14641  zndvds0  14654  znf1o  14655  znleval  14657  znfi  14659  znhash  14660  znunit  14663  psrbasg  14678  psradd  14683  psr0cl  14685  mpladd  14708  cldval  14813  ntrfval  14814  clsfval  14815  neifval  14854  neif  14855  neival  14857  cnclima  14937  cncnpi  14942  cnrest2  14950  cnrest2r  14951  cnptoprest  14953  cnpdis  14956  txvalex  14968  txval  14969  txcnmpt  14987  txdis  14991  cnmpt1t  14999  cnmpt2t  15007  hmeocnv  15021  hmeontr  15027  txhmeo  15033  xmetunirn  15072  xmettpos  15084  metn0  15092  xmetres  15096  metres  15097  blrnps  15125  blrn  15126  blin2  15146  blbas  15147  xmeterval  15149  xmettxlem  15223  xmettx  15224  metcnpi  15229  reldvg  15393  dvaddxx  15417  dvmulxx  15418  dviaddf  15419  dvimulf  15420  dvfre  15424  dvmptid  15430  dveflem  15440  elply2  15449  plyreres  15478  sinq12gt0  15544  rprelogbdiv  15671  logbgcd1irr  15681  fsumdvdsmul  15705  lgslem4  15722  lgsdirprm  15753  gausslemma2dlem0a  15768  gausslemma2dlem0f  15773  gausslemma2dlem0i  15776  gausslemma2dlem1a  15777  gausslemma2dlem1cl  15778  gausslemma2dlem5  15785  gausslemma2dlem6  15786  gausslemma2d  15788  lgseisenlem1  15789  lgseisenlem2  15790  lgseisenlem3  15791  lgseisen  15793  lgsquadlem1  15796  m1lgs  15804  2lgslem1a  15807  2lgslem1c  15809  2lgsoddprmlem2  15825  edgval  15901  edgstruct  15905  umgrnloopv  15955  umgredgprv  15956  upgr1edc  15962  umgredgne  15989  usgredgssen  16001  umgr2edg1  16048  uspgredg2vlem  16059  uspgr1edc  16079  wlkm  16136  wlkvtxiedg  16142  wlkvtxiedgg  16143  wlk1walkdom  16156  g0wlk0  16167  wlkres  16174  trlf1  16183  trlreslem  16184  trlres  16185  clwwlkg  16188  clwwlkccatlem  16195  clwwlknon  16224  eupthfi  16246  eupthseg  16247  eupthres  16252  bj-inex  16438  bj-sucexg  16453  bj-peano4  16486  setindis  16498  bdsetindis  16500  bj-inf2vnlem1  16501  nnsf  16543  nninfall  16547  nninfsellemeq  16552  sbthom  16566