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  384  hbim  1525  19.9hd  1641  equsexd  1708  sbcof2  1783  aev  1785  sbequi  1812  nfsbd  1951  mo2n  2028  eupickb  2081  r19.29af2  2575  spc2gv  2780  spc3gv  2782  eqvincg  2813  sbcco3g  3062  ssrmof  3165  exmidsssnc  4134  snelpwi  4142  opth1  4166  frind  4282  onin  4316  abnexg  4375  reusv1  4387  xpexg  4661  dmexg  4811  rnexg  4812  relfld  5075  funimaexglem  5214  funimaexg  5215  fabexg  5318  fsnd  5418  nfvres  5462  funimass4  5480  elfvmptrab1  5523  funconstss  5546  f1oresrab  5593  resfunexg  5649  f1eqcocnv  5700  isores1  5723  isoini  5727  isose  5730  isopolem  5731  isosolem  5733  eusvobj2  5768  acexmidlemcase  5777  oprabid  5811  offval  5997  resfunexgALT  6016  offval3  6040  1stvalg  6048  2ndvalg  6049  1stcof  6069  2ndcof  6070  cnvf1o  6130  tposf12  6174  smores3  6198  smoiso  6207  tfr0dm  6227  tfrlemibxssdm  6232  tfrlemi14d  6238  tfrexlem  6239  tfr1onlemssrecs  6244  tfr1onlemsucfn  6245  tfr1onlemsucaccv  6246  tfr1onlembxssdm  6248  tfr1onlemres  6254  tfri1dALT  6256  tfrcllemssrecs  6257  tfrcllemsucfn  6258  tfrcllemsucaccv  6259  tfrcllembxssdm  6261  tfrcllemres  6267  rdgss  6288  nnsucsssuc  6396  nntr2  6407  swoord1  6466  swoord2  6467  iinerm  6509  eroveu  6528  pmresg  6578  en1uniel  6706  fopwdom  6738  xpen  6747  ssenen  6753  isinfinf  6799  ac6sfi  6800  preimaf1ofi  6847  sbthlem1  6853  fi0  6871  fiss  6873  supubti  6894  suplubti  6895  isotilem  6901  supisolem  6903  supisoex  6904  supisoti  6905  ordiso2  6928  eldju1st  6964  eldju2ndl  6965  updjud  6975  djudom  6986  ctmlemr  7001  enumctlemm  7007  ctssexmid  7032  exmidonfinlem  7066  en2other2  7069  exmidaclem  7081  cc2lem  7098  cc3  7100  addclnq  7207  mulclnq  7208  1qec  7220  prarloclemarch2  7251  enq0tr  7266  addclnq0  7283  mulclnq0  7284  nq0m0r  7288  prarloclemlo  7326  prarloc  7335  genpml  7349  genpmu  7350  addnqprl  7361  addnqpru  7362  recnnpr  7380  prmuloc2  7399  1idpru  7423  ltexprlemm  7432  ltexprlemloc  7439  recexprlemm  7456  recexprlem1ssl  7465  caucvgprlemnkj  7498  caucvgprlemnbj  7499  caucvgprlemm  7500  caucvgprlemopl  7501  caucvgprlemlol  7502  caucvgprlemladdfu  7509  caucvgprlemladdrl  7510  caucvgprprlemk  7515  caucvgprprlemloccalc  7516  caucvgprprlemnkltj  7521  caucvgprprlemnjltk  7523  caucvgprprlemml  7526  caucvgprprlemmu  7527  caucvgprprlemlol  7530  caucvgprprlemexb  7539  caucvgprprlem1  7541  suplocexprlemml  7548  suplocexprlemlub  7556  addclsr  7585  mulclsr  7586  prsrcl  7616  caucvgsrlemoffcau  7630  peano5nnnn  7724  mulap0r  8401  nn1suc  8763  prime  9174  zindd  9193  xrlttri3  9613  xnn0xadd0  9680  fzopth  9872  fzsuc  9880  fzpred  9881  fzp1ss  9884  fztp  9889  fseq1p1m1  9905  1fv  9947  elfzom1elp1fzo  10010  ssfzo12  10032  fzosplitsn  10041  divfl0  10100  modqid  10153  modqmuladdim  10171  frecuzrdgtcl  10216  frecuzrdgfunlem  10223  frecfzennn  10230  frecfzen2  10231  seq3val  10262  seqvalcd  10263  iseqf1olemqcl  10290  iseqf1olemnab  10292  iseqf1olemmo  10296  iseqf1olemqk  10298  seq3f1olemstep  10305  seq3id3  10311  faclbnd  10519  faclbnd3  10521  bcm1k  10538  hashfz1  10561  focdmex  10565  hashfz  10599  hashfzp1  10602  hashfacen  10611  leisorel  10612  cjcj  10687  caucvgre  10785  r19.2uz  10797  resqrexlemgt0  10824  ltabs  10891  xrmaxiflemab  11048  xrmaxiflemlub  11049  nnf1o  11177  summodclem2a  11182  fsumf1o  11191  fisum0diag2  11248  modfsummodlemstep  11258  fsumparts  11271  clim2prod  11340  prodfap0  11346  prodmodclem2a  11377  ef0lem  11403  resinval  11458  recosval  11459  demoivreALT  11516  nn0o  11640  zsupcllemstep  11674  zsupcllemex  11675  infssuzledc  11679  gcdmultiplez  11745  dvdssq  11755  eucalg  11776  lcmgcdnn  11799  dvdsnprmd  11842  prm2orodd  11843  qnumdenbi  11906  nn0gcdsq  11914  phibnd  11929  hashdvds  11933  phimullem  11937  hashgcdlem  11939  unennn  11946  ennnfonelemk  11949  ennnfonelemjn  11951  ennnfonelemhf1o  11962  ennnfonelemex  11963  ennnfonelemf1  11967  ennnfonelemrn  11968  qnnen  11980  setsfun0  12034  srngbased  12121  srngplusgd  12122  srngmulrd  12123  srnginvld  12124  lmodbased  12132  lmodplusgd  12133  lmodscad  12134  lmodvscad  12135  ipsbased  12140  ipsaddgd  12141  ipsmulrd  12142  ipsscad  12143  ipsvscad  12144  ipsipd  12145  tgval  12257  cldval  12307  ntrfval  12308  clsfval  12309  neifval  12348  neif  12349  neival  12351  cnclima  12431  cncnpi  12436  cnrest2  12444  cnrest2r  12445  cnptoprest  12447  cnpdis  12450  txvalex  12462  txval  12463  txcnmpt  12481  txdis  12485  cnmpt1t  12493  cnmpt2t  12501  hmeocnv  12515  hmeontr  12521  txhmeo  12527  xmetunirn  12566  xmettpos  12578  metn0  12586  xmetres  12590  metres  12591  blrnps  12619  blrn  12620  blin2  12640  blbas  12641  xmeterval  12643  xmettxlem  12717  xmettx  12718  metcnpi  12723  reldvg  12856  dvaddxx  12875  dvmulxx  12876  dviaddf  12877  dvimulf  12878  dvfre  12882  dveflem  12895  sinq12gt0  12959  rprelogbdiv  13082  logbgcd1irr  13092  bj-inex  13276  bj-sucexg  13291  bj-peano4  13324  setindis  13336  bdsetindis  13338  bj-inf2vnlem1  13339  exmid1stab  13368  nnsf  13374  nninfalllemn  13377  nninfall  13379  nninfsellemeq  13385  sbthom  13396