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-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  4syl  18  simpl2im  378  hbim  1477  19.9hd  1592  equsexd  1657  sbcof2  1731  aev  1733  sbequi  1760  nfsbd  1892  mo2n  1969  eupickb  2022  r19.29af2  2496  spc2gv  2688  spc3gv  2690  eqvincg  2719  sbcco3g  2959  snelpwi  3967  opth1  3991  frind  4107  onin  4141  reusv1  4208  xpexg  4470  dmexg  4614  rnexg  4615  relfld  4866  funimaexglem  5002  funimaexg  5003  fabexg  5097  nfvres  5227  funimass4  5245  funconstss  5306  f1oresrab  5350  resfunexg  5403  f1eqcocnv  5451  isores1  5474  isoini  5477  isose  5480  isopolem  5481  isosolem  5483  eusvobj2  5518  acexmidlemcase  5527  oprabid  5557  offval  5739  resfunexgALT  5757  offval3  5781  1stvalg  5789  2ndvalg  5790  1stcof  5810  2ndcof  5811  cnvf1o  5866  tposf12  5907  smores3  5931  smoiso  5940  tfr0  5960  tfrlemibxssdm  5964  tfrlemi14d  5970  tfrexlem  5971  rdgss  5993  frecsuclemdm  6011  nnsucsssuc  6094  swoord1  6158  swoord2  6159  iinerm  6201  eroveu  6220  en1uniel  6307  fopwdom  6333  ac6sfi  6379  supubti  6412  suplubti  6413  isotilem  6419  supisolem  6421  supisoex  6422  supisoti  6423  ordiso2  6446  addclnq  6565  mulclnq  6566  1qec  6578  prarloclemarch2  6609  enq0tr  6624  addclnq0  6641  mulclnq0  6642  nq0m0r  6646  prarloclemlo  6684  prarloc  6693  genpml  6707  genpmu  6708  addnqprl  6719  addnqpru  6720  recnnpr  6738  prmuloc2  6757  1idpru  6781  ltexprlemm  6790  ltexprlemloc  6797  recexprlemm  6814  recexprlem1ssl  6823  caucvgprlemnkj  6856  caucvgprlemnbj  6857  caucvgprlemm  6858  caucvgprlemopl  6859  caucvgprlemlol  6860  caucvgprlemladdfu  6867  caucvgprlemladdrl  6868  caucvgprprlemk  6873  caucvgprprlemloccalc  6874  caucvgprprlemnkltj  6879  caucvgprprlemnjltk  6881  caucvgprprlemml  6884  caucvgprprlemmu  6885  caucvgprprlemlol  6888  caucvgprprlemexb  6897  caucvgprprlem1  6899  addclsr  6930  mulclsr  6931  prsrcl  6960  caucvgsrlemoffcau  6974  peano5nnnn  7058  mulap0r  7715  nn1suc  8058  prime  8446  zindd  8465  xrlttri3  8872  fzopth  9079  fzsuc  9086  fzpred  9087  fzp1ss  9090  fztp  9095  fseq1p1m1  9111  1fv  9149  elfzom1elp1fzo  9211  ssfzo12  9233  fzosplitsn  9242  divfl0  9298  modqid  9351  modqmuladdim  9369  frecuzrdgcl  9415  frecuzrdgsuc  9417  frecfzennn  9419  frecfzen2  9420  iseqsplit  9458  iseqid3s  9466  faclbnd  9668  faclbnd3  9670  bcm1k  9687  cjcj  9770  caucvgre  9867  r19.2uz  9879  resqrexlemgt0  9906  ltabs  9973  nn0o  10307  zsupcllemstep  10341  zsupcllemex  10342  infssuzledc  10346  gcdmultiplez  10410  dvdssq  10420  eucialg  10441  lcmgcdnn  10464  dvdsnprmd  10507  prm2orodd  10508  bj-inex  10698  bj-sucexg  10713  bj-peano4  10750  setindis  10762  bdsetindis  10764  bj-inf2vnlem1  10765