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  1545  nfal  1576  19.9hd  1662  equsexd  1729  sbcof2  1810  aev  1812  sbequi  1839  nfsbd  1977  mo2n  2054  eupickb  2107  r19.29af2  2617  spc2gv  2828  spc3gv  2830  eqvincg  2861  sbcco3g  3114  ssrmof  3218  exmidsssnc  4203  exmid1stab  4208  snelpwi  4212  opth1  4236  frind  4352  onin  4386  abnexg  4446  reusv1  4458  xpexg  4740  dmexg  4891  rnexg  4892  elrelimasn  4994  relfld  5157  funimaexglem  5299  funimaexg  5300  fabexg  5403  fsnd  5504  nfvres  5548  funimass4  5566  elfvmptrab1  5610  funconstss  5634  f1oresrab  5681  resfunexg  5737  f1eqcocnv  5791  isores1  5814  isoini  5818  isose  5821  isopolem  5822  isosolem  5824  eusvobj2  5860  acexmidlemcase  5869  oprabid  5906  offval  6089  resfunexgALT  6108  offval3  6134  1stvalg  6142  2ndvalg  6143  1stcof  6163  2ndcof  6164  cnvf1o  6225  tposf12  6269  smores3  6293  smoiso  6302  tfr0dm  6322  tfrlemibxssdm  6327  tfrlemi14d  6333  tfrexlem  6334  tfr1onlemssrecs  6339  tfr1onlemsucfn  6340  tfr1onlemsucaccv  6341  tfr1onlembxssdm  6343  tfr1onlemres  6349  tfri1dALT  6351  tfrcllemssrecs  6352  tfrcllemsucfn  6353  tfrcllemsucaccv  6354  tfrcllembxssdm  6356  tfrcllemres  6362  rdgss  6383  nnsucsssuc  6492  nntr2  6503  swoord1  6563  swoord2  6564  iinerm  6606  eroveu  6625  pmresg  6675  en1uniel  6803  fopwdom  6835  xpen  6844  ssenen  6850  isinfinf  6896  ac6sfi  6897  preimaf1ofi  6949  sbthlem1  6955  fi0  6973  fiss  6975  supubti  6997  suplubti  6998  isotilem  7004  supisolem  7006  supisoex  7007  supisoti  7008  ordiso2  7033  eldju1st  7069  eldju2ndl  7070  updjud  7080  djudom  7091  ctmlemr  7106  enumctlemm  7112  nnnninfeq  7125  ctssexmid  7147  nninfwlpoimlemginf  7173  exmidonfinlem  7191  en2other2  7194  exmidaclem  7206  cc2lem  7264  cc3  7266  addclnq  7373  mulclnq  7374  1qec  7386  prarloclemarch2  7417  enq0tr  7432  addclnq0  7449  mulclnq0  7450  nq0m0r  7454  prarloclemlo  7492  prarloc  7501  genpml  7515  genpmu  7516  addnqprl  7527  addnqpru  7528  recnnpr  7546  prmuloc2  7565  1idpru  7589  ltexprlemm  7598  ltexprlemloc  7605  recexprlemm  7622  recexprlem1ssl  7631  caucvgprlemnkj  7664  caucvgprlemnbj  7665  caucvgprlemm  7666  caucvgprlemopl  7667  caucvgprlemlol  7668  caucvgprlemladdfu  7675  caucvgprlemladdrl  7676  caucvgprprlemk  7681  caucvgprprlemloccalc  7682  caucvgprprlemnkltj  7687  caucvgprprlemnjltk  7689  caucvgprprlemml  7692  caucvgprprlemmu  7693  caucvgprprlemlol  7696  caucvgprprlemexb  7705  caucvgprprlem1  7707  suplocexprlemml  7714  suplocexprlemlub  7722  addclsr  7751  mulclsr  7752  prsrcl  7782  caucvgsrlemoffcau  7796  peano5nnnn  7890  mulap0r  8571  nn1suc  8937  prime  9351  zindd  9370  xrlttri3  9796  xnn0xadd0  9866  fzopth  10060  fzsuc  10068  fzpred  10069  fzp1ss  10072  fztp  10077  fseq1p1m1  10093  1fv  10138  elfzom1elp1fzo  10201  ssfzo12  10223  fzosplitsn  10232  divfl0  10295  modqid  10348  modqmuladdim  10366  frecuzrdgtcl  10411  frecuzrdgfunlem  10418  frecfzennn  10425  frecfzen2  10426  seq3val  10457  seqvalcd  10458  iseqf1olemqcl  10485  iseqf1olemnab  10487  iseqf1olemmo  10491  iseqf1olemqk  10493  seq3f1olemstep  10500  seq3id3  10506  faclbnd  10720  faclbnd3  10722  bcm1k  10739  hashfz1  10762  hashfz  10800  hashfzp1  10803  fiubm  10807  hashfacen  10815  leisorel  10816  cjcj  10891  caucvgre  10989  r19.2uz  11001  resqrexlemgt0  11028  ltabs  11095  xrmaxiflemab  11254  xrmaxiflemlub  11255  nnf1o  11383  summodclem2a  11388  fsumf1o  11397  fisum0diag2  11454  modfsummodlemstep  11464  fsumparts  11477  clim2prod  11546  prodfap0  11552  prodmodclem2a  11583  fprodssdc  11597  fprodcllem  11613  ef0lem  11667  resinval  11722  recosval  11723  demoivreALT  11780  nn0o  11911  zsupcllemstep  11945  zsupcllemex  11946  infssuzledc  11950  gcdmultiplez  12021  dvdssq  12031  eucalg  12058  lcmgcdnn  12081  dvdsnprmd  12124  prm2orodd  12125  isprm5lem  12140  qnumdenbi  12191  nn0gcdsq  12199  phibnd  12216  hashdvds  12220  phimullem  12224  prmdiveq  12235  hashgcdlem  12237  modprm0  12253  nnnn0modprm0  12254  modprmn0modprm0  12255  oddprm  12258  prm23lt5  12262  pcprendvds  12289  pcidlem  12321  pcmpt  12340  pcfac  12347  infpnlem2  12357  prmunb  12359  1arith  12364  unennn  12397  ennnfonelemk  12400  ennnfonelemjn  12402  ennnfonelemhf1o  12413  ennnfonelemex  12414  ennnfonelemf1  12418  ennnfonelemrn  12419  qnnen  12431  unbendc  12454  setsfun0  12497  srngbased  12604  srngplusgd  12605  srngmulrd  12606  srnginvld  12607  lmodbased  12622  lmodplusgd  12623  lmodscad  12624  lmodvscad  12625  ipsbased  12634  ipsaddgd  12635  ipsmulrd  12636  ipsscad  12637  ipsvscad  12638  ipsipd  12639  tgval  12710  isnsgrp  12811  ismnd  12819  dfgrp2e  12902  subgintm  13056  srgisid  13167  srg1zr  13168  oppr1g  13250  dvdsr02  13272  isunitd  13273  crngunit  13278  unitpropdg  13315  subrguss  13355  subrgunit  13358  subrgugrp  13359  subrgintm  13362  cldval  13569  ntrfval  13570  clsfval  13571  neifval  13610  neif  13611  neival  13613  cnclima  13693  cncnpi  13698  cnrest2  13706  cnrest2r  13707  cnptoprest  13709  cnpdis  13712  txvalex  13724  txval  13725  txcnmpt  13743  txdis  13747  cnmpt1t  13755  cnmpt2t  13763  hmeocnv  13777  hmeontr  13783  txhmeo  13789  xmetunirn  13828  xmettpos  13840  metn0  13848  xmetres  13852  metres  13853  blrnps  13881  blrn  13882  blin2  13902  blbas  13903  xmeterval  13905  xmettxlem  13979  xmettx  13980  metcnpi  13985  reldvg  14118  dvaddxx  14137  dvmulxx  14138  dviaddf  14139  dvimulf  14140  dvfre  14144  dveflem  14157  sinq12gt0  14221  rprelogbdiv  14345  logbgcd1irr  14355  lgslem4  14374  lgsdirprm  14405  lgseisenlem1  14420  lgseisenlem2  14421  m1lgs  14422  2lgsoddprmlem2  14424  bj-inex  14629  bj-sucexg  14644  bj-peano4  14677  setindis  14689  bdsetindis  14691  bj-inf2vnlem1  14692  nnsf  14724  nninfall  14728  nninfsellemeq  14733  sbthom  14744