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  1593  nfal  1624  19.9hd  1710  equsexd  1777  sbcof2  1858  aev  1860  sbequi  1887  nfsbd  2030  mo2n  2107  eupickb  2161  r19.29af2  2673  spc2gv  2897  spc3gv  2899  eqvincg  2930  sbcco3g  3185  ssrmof  3290  exmidsssnc  4293  exmid1stab  4298  snelpwi  4303  opth1  4328  frind  4449  onin  4483  abnexg  4543  reusv1  4555  xpexg  4840  reldmm  4950  dmexg  4996  rnexg  4997  elrelimasn  5102  relfld  5265  funimaexglem  5413  funimaexg  5414  fabexg  5524  fsnd  5628  elfvm  5672  nfvres  5675  funimass4  5696  elfvmptrab1  5741  funconstss  5765  f1oresrab  5812  resfunexg  5875  f1eqcocnv  5932  isores1  5955  isoini  5959  isose  5962  isopolem  5963  isosolem  5965  eusvobj2  6004  acexmidlemcase  6013  oprabid  6050  offval  6243  resfunexgALT  6270  offval3  6296  1stvalg  6305  2ndvalg  6306  1stcof  6326  2ndcof  6327  cnvf1o  6390  tposf12  6435  smores3  6459  smoiso  6468  tfr0dm  6488  tfrlemibxssdm  6493  tfrlemi14d  6499  tfrexlem  6500  tfr1onlemssrecs  6505  tfr1onlemsucfn  6506  tfr1onlemsucaccv  6507  tfr1onlembxssdm  6509  tfr1onlemres  6515  tfri1dALT  6517  tfrcllemssrecs  6518  tfrcllemsucfn  6519  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllemres  6528  rdgss  6549  nnsucsssuc  6660  nntr2  6671  swoord1  6731  swoord2  6732  iinerm  6776  eroveu  6795  pmresg  6845  en1uniel  6978  dom1o  7002  pw2f1odclem  7020  fopwdom  7022  xpen  7031  ssenen  7037  isinfinf  7086  ac6sfi  7087  preimaf1ofi  7150  sbthlem1  7156  fi0  7174  fiss  7176  supubti  7198  suplubti  7199  isotilem  7205  supisolem  7207  supisoex  7208  supisoti  7209  ordiso2  7234  eldju1st  7270  eldju2ndl  7271  updjud  7281  djudom  7292  ctmlemr  7307  enumctlemm  7313  nnnninfeq  7327  ctssexmid  7349  nninfwlpoimlemginf  7375  exmidonfinlem  7404  en2other2  7407  exmidaclem  7423  cc2lem  7485  cc3  7487  addclnq  7595  mulclnq  7596  1qec  7608  prarloclemarch2  7639  enq0tr  7654  addclnq0  7671  mulclnq0  7672  nq0m0r  7676  prarloclemlo  7714  prarloc  7723  genpml  7737  genpmu  7738  addnqprl  7749  addnqpru  7750  recnnpr  7768  prmuloc2  7787  1idpru  7811  ltexprlemm  7820  ltexprlemloc  7827  recexprlemm  7844  recexprlem1ssl  7853  caucvgprlemnkj  7886  caucvgprlemnbj  7887  caucvgprlemm  7888  caucvgprlemopl  7889  caucvgprlemlol  7890  caucvgprlemladdfu  7897  caucvgprlemladdrl  7898  caucvgprprlemk  7903  caucvgprprlemloccalc  7904  caucvgprprlemnkltj  7909  caucvgprprlemnjltk  7911  caucvgprprlemml  7914  caucvgprprlemmu  7915  caucvgprprlemlol  7918  caucvgprprlemexb  7927  caucvgprprlem1  7929  suplocexprlemml  7936  suplocexprlemlub  7944  addclsr  7973  mulclsr  7974  prsrcl  8004  caucvgsrlemoffcau  8018  peano5nnnn  8112  mulap0r  8795  nn1suc  9162  prime  9579  zindd  9598  xrlttri3  10032  xnn0xadd0  10102  fzopth  10296  fzsuc  10304  fzpred  10305  fzp1ss  10308  fztp  10313  fseq1p1m1  10329  1fv  10374  elfzom1elp1fzo  10448  ssfzo12  10470  fzosplitsn  10479  zsupcllemstep  10490  zsupcllemex  10491  infssuzledc  10495  divfl0  10557  fldiv4lem1div2uz2  10567  modqid  10612  modqmuladdim  10630  frecuzrdgtcl  10675  frecuzrdgfunlem  10682  frecfzennn  10689  frecfzen2  10690  seq3val  10723  seqvalcd  10724  seqsplitg  10752  iseqf1olemqcl  10762  iseqf1olemnab  10764  iseqf1olemmo  10768  iseqf1olemqk  10770  seq3f1olemstep  10777  seqf1oglem2  10783  seq3id3  10787  seqhomog  10793  faclbnd  11004  faclbnd3  11006  bcm1k  11023  hashfz1  11046  hashfz  11086  hashfzp1  11089  fiubm  11093  hashfacen  11101  leisorel  11102  wrdexb  11129  wrdsymb  11145  wrdred1hash  11161  lsw0  11165  lswex  11169  ccat0  11177  ccatval2  11179  ccatw2s1leng  11219  ccats1val2  11221  swrds1  11253  swrdlsw  11254  ccats1pfxeqrex  11300  pfxccatin12lem1  11313  swrdccatin2  11314  swrdccat  11320  cats1fvd  11351  s1s2d  11379  s1s3d  11380  cjcj  11461  caucvgre  11559  r19.2uz  11571  resqrexlemgt0  11598  ltabs  11665  xrmaxiflemab  11825  xrmaxiflemlub  11826  nnf1o  11955  summodclem2a  11960  fsumf1o  11969  fisum0diag2  12026  modfsummodlemstep  12036  fsumparts  12049  clim2prod  12118  prodfap0  12124  prodmodclem2a  12155  fprodssdc  12169  fprodcllem  12185  ef0lem  12239  resinval  12294  recosval  12295  demoivreALT  12353  nn0o  12486  gcdmultiplez  12610  dvdssq  12620  nninfct  12630  eucalg  12649  lcmgcdnn  12672  dvdsnprmd  12715  prm2orodd  12716  isprm5lem  12731  qnumdenbi  12782  nn0gcdsq  12790  phibnd  12807  hashdvds  12811  phimullem  12815  prmdiveq  12826  hashgcdlem  12828  modprm0  12845  nnnn0modprm0  12846  modprmn0modprm0  12847  oddprm  12850  prm23lt5  12854  pcprendvds  12881  pcidlem  12914  pcmpt  12934  pcfac  12941  infpnlem2  12951  prmunb  12953  1arith  12958  4sqlem19  13000  unennn  13036  ennnfonelemk  13039  ennnfonelemjn  13041  ennnfonelemhf1o  13052  ennnfonelemex  13053  ennnfonelemf1  13057  ennnfonelemrn  13058  qnnen  13070  unbendc  13093  setsfun0  13136  srngbased  13248  srngplusgd  13249  srngmulrd  13250  srnginvld  13251  lmodbased  13266  lmodplusgd  13267  lmodscad  13268  lmodvscad  13269  ipsbased  13278  ipsaddgd  13279  ipsmulrd  13280  ipsscad  13281  ipsvscad  13282  ipsipd  13283  tgval  13363  prdsbas3  13388  isnsgrp  13507  ismnd  13520  dfgrp2e  13629  subgintm  13803  eqg0el  13834  ecqusaddcl  13844  kerf1ghm  13879  gsumfzconst  13946  imasrng  13988  srgisid  14018  srg1zr  14019  qusring2  14098  oppr1g  14114  dvdsr02  14138  isunitd  14139  crngunit  14144  unitpropdg  14181  elrhmunit  14210  subrngintm  14245  subrguss  14269  subrgunit  14272  subrgugrp  14273  subrgintm  14276  lmodfopnelem1  14357  rmodislmodlem  14383  rmodislmod  14384  lssuni  14396  islss3  14412  lss0v  14463  sraval  14470  rnglidlmmgm  14529  2idllidld  14539  2idlridld  14540  rng2idl0  14552  rng2idlsubg0  14555  zrh0  14658  znle  14670  zndvds0  14683  znf1o  14684  znleval  14686  znfi  14688  znhash  14689  znunit  14692  psrbasg  14707  psradd  14712  psr0cl  14714  mpladd  14737  cldval  14842  ntrfval  14843  clsfval  14844  neifval  14883  neif  14884  neival  14886  cnclima  14966  cncnpi  14971  cnrest2  14979  cnrest2r  14980  cnptoprest  14982  cnpdis  14985  txvalex  14997  txval  14998  txcnmpt  15016  txdis  15020  cnmpt1t  15028  cnmpt2t  15036  hmeocnv  15050  hmeontr  15056  txhmeo  15062  xmetunirn  15101  xmettpos  15113  metn0  15121  xmetres  15125  metres  15126  blrnps  15154  blrn  15155  blin2  15175  blbas  15176  xmeterval  15178  xmettxlem  15252  xmettx  15253  metcnpi  15258  reldvg  15422  dvaddxx  15446  dvmulxx  15447  dviaddf  15448  dvimulf  15449  dvfre  15453  dvmptid  15459  dveflem  15469  elply2  15478  plyreres  15507  sinq12gt0  15573  rprelogbdiv  15700  logbgcd1irr  15710  fsumdvdsmul  15734  lgslem4  15751  lgsdirprm  15782  gausslemma2dlem0a  15797  gausslemma2dlem0f  15802  gausslemma2dlem0i  15805  gausslemma2dlem1a  15806  gausslemma2dlem1cl  15807  gausslemma2dlem5  15814  gausslemma2dlem6  15815  gausslemma2d  15817  lgseisenlem1  15818  lgseisenlem2  15819  lgseisenlem3  15820  lgseisen  15822  lgsquadlem1  15825  m1lgs  15833  2lgslem1a  15836  2lgslem1c  15838  2lgsoddprmlem2  15854  edgval  15930  edgstruct  15934  umgrnloopv  15984  umgredgprv  15985  upgr1edc  15991  umgredgne  16020  usgredgssen  16032  umgr2edg1  16079  uspgredg2vlem  16090  uspgr1edc  16110  uhgrspansubgrlem  16146  wlkm  16209  wlkvtxiedg  16215  wlkvtxiedgg  16216  wlk1walkdom  16229  g0wlk0  16240  wlkres  16249  trlf1  16258  trlreslem  16259  trlres  16260  clwwlkg  16263  clwwlkccatlem  16270  clwwlknon  16299  eupthfi  16321  eupthseg  16322  eupthres  16327  trlsegvdeglem1  16330  trlsegvdeglem7  16336  trlsegvdegfi  16337  eupth2lem3lem2fi  16339  eupth2lem3lem3fi  16340  eupth2lem3lem6fi  16341  eupth2lem3lem4fi  16343  eupth2lem3lem7fi  16344  eupth2lem3fi  16346  eupth2lemsfi  16348  eupth2fi  16349  konigsbergssiedgwen  16356  bj-inex  16553  bj-sucexg  16568  bj-peano4  16601  setindis  16613  bdsetindis  16615  bj-inf2vnlem1  16616  nnsf  16658  nninfall  16662  nninfsellemeq  16667  sbthom  16681  gfsumval  16732