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  1482  19.9hd  1597  equsexd  1664  sbcof2  1738  aev  1740  sbequi  1767  nfsbd  1899  mo2n  1976  eupickb  2029  r19.29af2  2508  spc2gv  2709  spc3gv  2711  eqvincg  2739  sbcco3g  2983  snelpwi  4030  opth1  4054  frind  4170  onin  4204  reusv1  4271  xpexg  4540  dmexg  4685  rnexg  4686  relfld  4946  funimaexglem  5083  funimaexg  5084  fabexg  5182  nfvres  5321  funimass4  5339  funconstss  5401  f1oresrab  5447  resfunexg  5500  f1eqcocnv  5552  isores1  5575  isoini  5579  isose  5582  isopolem  5583  isosolem  5585  eusvobj2  5620  acexmidlemcase  5629  oprabid  5663  offval  5845  resfunexgALT  5863  offval3  5887  1stvalg  5895  2ndvalg  5896  1stcof  5916  2ndcof  5917  cnvf1o  5972  tposf12  6016  smores3  6040  smoiso  6049  tfr0dm  6069  tfrlemibxssdm  6074  tfrlemi14d  6080  tfrexlem  6081  tfr1onlemssrecs  6086  tfr1onlemsucfn  6087  tfr1onlemsucaccv  6088  tfr1onlembxssdm  6090  tfr1onlemres  6096  tfri1dALT  6098  tfrcllemssrecs  6099  tfrcllemsucfn  6100  tfrcllemsucaccv  6101  tfrcllembxssdm  6103  tfrcllemres  6109  rdgss  6130  nnsucsssuc  6235  swoord1  6301  swoord2  6302  iinerm  6344  eroveu  6363  pmresg  6413  en1uniel  6501  fopwdom  6532  xpen  6541  ssenen  6547  isinfinf  6593  ac6sfi  6594  preimaf1ofi  6639  sbthlem1  6645  supubti  6673  suplubti  6674  isotilem  6680  supisolem  6682  supisoex  6683  supisoti  6684  ordiso2  6707  djur  6736  eldju1st  6741  eldju2ndl  6742  updjud  6752  djudom  6766  en2other2  6801  addclnq  6913  mulclnq  6914  1qec  6926  prarloclemarch2  6957  enq0tr  6972  addclnq0  6989  mulclnq0  6990  nq0m0r  6994  prarloclemlo  7032  prarloc  7041  genpml  7055  genpmu  7056  addnqprl  7067  addnqpru  7068  recnnpr  7086  prmuloc2  7105  1idpru  7129  ltexprlemm  7138  ltexprlemloc  7145  recexprlemm  7162  recexprlem1ssl  7171  caucvgprlemnkj  7204  caucvgprlemnbj  7205  caucvgprlemm  7206  caucvgprlemopl  7207  caucvgprlemlol  7208  caucvgprlemladdfu  7215  caucvgprlemladdrl  7216  caucvgprprlemk  7221  caucvgprprlemloccalc  7222  caucvgprprlemnkltj  7227  caucvgprprlemnjltk  7229  caucvgprprlemml  7232  caucvgprprlemmu  7233  caucvgprprlemlol  7236  caucvgprprlemexb  7245  caucvgprprlem1  7247  addclsr  7278  mulclsr  7279  prsrcl  7308  caucvgsrlemoffcau  7322  peano5nnnn  7406  mulap0r  8068  nn1suc  8413  prime  8815  zindd  8834  xrlttri3  9236  fzopth  9443  fzsuc  9450  fzpred  9451  fzp1ss  9454  fztp  9459  fseq1p1m1  9475  1fv  9515  elfzom1elp1fzo  9578  ssfzo12  9600  fzosplitsn  9609  divfl0  9668  modqid  9721  modqmuladdim  9739  frecuzrdgtcl  9784  frecuzrdgfunlem  9791  frecfzennn  9798  frecfzen2  9799  iseqvalt  9838  seq3val  9839  iseqsplit  9873  iseqf1olemqcl  9880  iseqf1olemnab  9882  iseqf1olemmo  9886  iseqf1olemqk  9888  seq3f1olemstep  9895  iseqid3s  9903  faclbnd  10114  faclbnd3  10116  bcm1k  10133  hashfz1  10156  focdmex  10160  hashfz  10194  hashfzp1  10197  hashfacen  10206  leisorel  10207  cjcj  10282  caucvgre  10379  r19.2uz  10391  resqrexlemgt0  10418  ltabs  10485  isummolemnm  10733  isummolem2a  10735  fsumf1o  10746  fisum0diag2  10804  modfsummodlemstep  10814  fsumparts  10827  nn0o  10989  zsupcllemstep  11023  zsupcllemex  11024  infssuzledc  11028  gcdmultiplez  11092  dvdssq  11102  eucialg  11123  lcmgcdnn  11146  dvdsnprmd  11189  prm2orodd  11190  qnumdenbi  11252  nn0gcdsq  11260  phibnd  11275  hashdvds  11279  phimullem  11283  hashgcdlem  11285  unennn  11292  bj-inex  11444  bj-sucexg  11459  bj-peano4  11496  setindis  11508  bdsetindis  11510  bj-inf2vnlem1  11511  nnsf  11541  nninfalllemn  11544  nninfall  11546  nninfsellemeq  11552