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 )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  4syl  18  simpl2im  390  hbim  1598  nfal  1629  19.9hd  1714  equsexd  1782  sbcof2  1863  aev  1865  sbequi  1892  nfsbd  2037  mo2n  2114  eupickb  2168  r19.29af2  2691  spc2gv  2916  spc3gv  2918  eqvincg  2950  sbcco3g  3205  ssrmof  3311  exmidsssnc  4342  exmid1stab  4347  snelpwi  4353  opth1  4378  frind  4499  onin  4533  abnexg  4594  reusv1  4606  xpexg  4891  reldmm  5002  dmexg  5048  rnexg  5049  elrelimasn  5156  relfld  5319  funimaexglem  5467  funimaexg  5468  fabexg  5582  fsnd  5687  elfvm  5732  nfvres  5735  funimass4  5756  elfvmptrab1  5804  funconstss  5830  f1oresrab  5876  resfunexg  5939  f1eqcocnv  6000  isores1  6023  isoini  6027  isose  6030  isopolem  6031  isosolem  6033  eusvobj2  6074  acexmidlemcase  6083  oprabid  6120  offval  6314  resfunexgALT  6341  offval3  6371  1stvalg  6380  2ndvalg  6381  1stcof  6401  2ndcof  6402  cnvf1o  6465  tposf12  6544  smores3  6568  smoiso  6577  tfr0dm  6597  tfrlemibxssdm  6602  tfrlemi14d  6608  tfrexlem  6609  tfr1onlemssrecs  6614  tfr1onlemsucfn  6615  tfr1onlemsucaccv  6616  tfr1onlembxssdm  6618  tfr1onlemres  6624  tfri1dALT  6626  tfrcllemssrecs  6627  tfrcllemsucfn  6628  tfrcllemsucaccv  6629  tfrcllembxssdm  6631  tfrcllemres  6637  rdgss  6658  nnsucsssuc  6769  nntr2  6780  swoord1  6840  swoord2  6841  iinerm  6885  eroveu  6904  pmresg  6961  en1uniel  7095  dom1o  7120  pw2f1odclem  7138  fopwdom  7140  xpen  7149  mapunen  7155  ssenen  7156  isinfinf  7205  ac6sfi  7206  preimaf1ofi  7273  sbthlem1  7279  fczfsuppd  7302  fi0  7314  fiss  7316  supubti  7345  suplubti  7346  isotilem  7352  supisolem  7354  supisoex  7355  supisoti  7356  ordiso2  7381  eldju1st  7417  eldju2ndl  7418  updjud  7428  djudom  7439  ctmlemr  7454  enumctlemm  7460  nnnninfeq  7474  ctssexmid  7496  nninfwlpoimlemginf  7522  exmidonfinlem  7551  en2other2  7554  exmidaclem  7570  cc2lem  7638  cc3  7640  addclnq  7748  mulclnq  7749  1qec  7761  prarloclemarch2  7792  enq0tr  7807  addclnq0  7824  mulclnq0  7825  nq0m0r  7829  prarloclemlo  7867  prarloc  7876  genpml  7890  genpmu  7891  addnqprl  7902  addnqpru  7903  recnnpr  7921  prmuloc2  7940  1idpru  7964  ltexprlemm  7973  ltexprlemloc  7980  recexprlemm  7997  recexprlem1ssl  8006  caucvgprlemnkj  8039  caucvgprlemnbj  8040  caucvgprlemm  8041  caucvgprlemopl  8042  caucvgprlemlol  8043  caucvgprlemladdfu  8050  caucvgprlemladdrl  8051  caucvgprprlemk  8056  caucvgprprlemloccalc  8057  caucvgprprlemnkltj  8062  caucvgprprlemnjltk  8064  caucvgprprlemml  8067  caucvgprprlemmu  8068  caucvgprprlemlol  8071  caucvgprprlemexb  8080  caucvgprprlem1  8082  suplocexprlemml  8089  suplocexprlemlub  8097  addclsr  8126  mulclsr  8127  prsrcl  8157  caucvgsrlemoffcau  8171  peano5nnnn  8265  mulap0r  8951  indv  9304  nn1suc  9332  prime  9756  zindd  9775  xrlttri3  10216  xnn0xadd0  10286  fzopth  10484  fzsuc  10492  fzpred  10494  fzp1ss  10497  fztp  10502  fseq1p1m1  10518  1fv  10563  elfzom1elp1fzo  10637  ssfzo12  10659  fzosplitsn  10668  zsupcllemstep  10679  zsupcllemex  10680  infssuzledc  10684  divfl0  10752  fldiv4lem1div2uz2  10762  modqid  10807  modqmuladdim  10825  frecuzrdgtcl  10870  frecuzrdgfunlem  10877  frecfzennn  10884  frecfzen2  10885  seq3val  10918  seqvalcd  10919  seqsplitg  10947  iseqf1olemqcl  10957  iseqf1olemnab  10959  iseqf1olemmo  10963  iseqf1olemqk  10965  seq3f1olemstep  10972  seqf1oglem2  10978  seq3id3  10982  seqhomog  10988  faclbnd  11201  faclbnd3  11203  bcm1k  11220  hashfz1  11244  hashfz  11284  hashfzp1  11287  fiubm  11293  hashfacen  11306  leisorel  11311  wrdexb  11338  wrdsymb  11354  wrdred1hash  11370  lsw0  11374  lswex  11378  ccat0  11386  ccatval2  11388  ccatw2s1leng  11428  ccats1val2  11430  swrds1  11462  swrdlsw  11463  ccats1pfxeqrex  11509  pfxccatin12lem1  11522  swrdccatin2  11523  swrdccat  11529  cats1fvd  11560  s1s2d  11588  s1s3d  11589  cjcj  11670  caucvgre  11769  r19.2uz  11781  resqrexlemgt0  11808  ltabs  11876  xrmaxiflemab  12038  xrmaxiflemlub  12039  nnf1o  12168  summodclem2a  12173  fsumf1o  12182  fisum0diag2  12239  modfsummodlemstep  12249  fsumparts  12262  clim2prod  12331  prodfap0  12337  prodmodclem2a  12368  fprodssdc  12382  fprodcllem  12398  ef0lem  12452  resinval  12507  recosval  12508  demoivreALT  12566  nn0o  12699  gcdmultiplez  12823  dvdssq  12833  nninfct  12843  eucalg  12862  lcmgcdnn  12885  dvdsnprmd  12928  prm2orodd  12929  isprm5lem  12945  qnumdenbi  12997  nn0gcdsq  13005  phibnd  13024  hashdvds  13028  phimullem  13032  prmdiveq  13043  hashgcdlem  13045  modprm0  13062  nnnn0modprm0  13063  modprmn0modprm0  13064  oddprm  13067  prm23lt5  13071  pcprendvds  13098  pcidlem  13131  pcmpt  13151  pcfac  13158  infpnlem2  13168  prmunb  13170  1arith  13175  4sqlem19  13217  ballotfilemfp1  13289  ballotfilemic  13308  ballotfilem1c  13309  ballotfilemsima  13317  ballotfilemrv  13321  ballotfilemro  13324  ballotfilemfrc  13328  ballotfilemfrci  13329  ballotfilemfrceq  13330  ballotfilemfrcn0  13331  ballotfilemrinv0  13334  unennn  13346  ennnfonelemk  13349  ennnfonelemjn  13351  ennnfonelemhf1o  13362  ennnfonelemex  13363  ennnfonelemf1  13367  ennnfonelemrn  13368  qnnen  13380  unbendc  13403  setsfun0  13446  srngbased  13560  srngplusgd  13561  srngmulrd  13562  srnginvld  13563  lmodbased  13578  lmodplusgd  13579  lmodscad  13580  lmodvscad  13581  ipsbased  13590  ipsaddgd  13591  ipsmulrd  13592  ipsscad  13593  ipsvscad  13594  ipsipd  13595  tgval  13675  gzsumval2  13773  isnsgrp  13780  ismnd  13791  dfgrp2e  13892  subgintm  14060  eqg0el  14091  ecqusaddcl  14101  kerf1ghm  14136  gzsumconst  14233  gsumvalfi  14242  gsumf1ofi  14250  gsumresfi  14263  gsum2dfilem2  14272  prdsbas3  14294  imasrng  14362  srgisid  14397  qusring2  14480  oppr1g  14497  dvdsr02  14521  isunitd  14522  crngunit  14527  unitpropdg  14564  elrhmunit  14593  subrngintm  14629  subrguss  14653  subrgunit  14656  subrgugrp  14657  subrgintm  14660  drngunz  14727  lmodfopnelem1  14770  rmodislmodlem  14796  rmodislmod  14797  lssuni  14809  islss3  14825  lss0v  14876  sraval  14883  rnglidlmmgm  14942  2idllidld  14952  2idlridld  14953  rng2idl0  14965  rng2idlsubg0  14968  zrh0  15069  znle  15081  zndvds0  15094  znf1o  15095  znleval  15097  znfi  15099  znhash  15100  znunit  15103  issubassa  15122  asclfval  15130  ascl0  15136  ascl1  15137  rnasclsubrg  15145  psrbaglecl  15169  psrass1filem  15177  psrbasg  15178  psradd  15183  psr0cl  15191  mpladd  15220  cldval  15325  ntrfval  15326  clsfval  15327  neifval  15366  neif  15367  neival  15369  cnclima  15449  cncnpi  15454  cnrest2  15462  cnrest2r  15463  cnptoprest  15465  cnpdis  15468  txvalex  15480  txval  15481  txcnmpt  15499  txdis  15503  cnmpt1t  15511  cnmpt2t  15519  hmeocnv  15533  hmeontr  15539  txhmeo  15545  xmetunirn  15584  xmettpos  15596  metn0  15604  xmetres  15608  metres  15609  blrnps  15637  blrn  15638  blin2  15658  blbas  15659  xmeterval  15661  xmettxlem  15735  xmettx  15736  metcnpi  15741  reldvg  15905  dvaddxx  15929  dvmulxx  15930  dviaddf  15931  dvimulf  15932  dvfre  15936  dvmptid  15942  dveflem  15952  elply2  15961  plyreres  15990  sinq12gt0  16057  logfac  16126  rprelogbdiv  16193  logbgcd1irr  16203  birthdaylem3  16227  ppinprm  16260  chtnprm  16262  ppiqp1le  16267  fsumdvdsmul  16285  bcmono  16304  bposlem1  16311  bposlem3  16313  bposlem5  16315  lgslem4  16327  lgsdirprm  16358  gausslemma2dlem0a  16373  gausslemma2dlem0f  16378  gausslemma2dlem0i  16381  gausslemma2dlem1a  16382  gausslemma2dlem1cl  16383  gausslemma2dlem5  16390  gausslemma2dlem6  16391  gausslemma2d  16393  lgseisenlem1  16394  lgseisenlem2  16395  lgseisenlem3  16396  lgseisen  16398  lgsquadlem1  16401  m1lgs  16409  2lgslem1a  16412  2lgslem1c  16414  2lgsoddprmlem2  16430  edgval  16506  edgstruct  16510  umgrnloopv  16560  umgredgprv  16561  upgr1edc  16567  umgredgne  16596  usgredgssen  16608  umgr2edg1  16655  uspgredg2vlem  16666  uspgr1edc  16686  uhgrspansubgrlem  16722  wlkm  16785  wlkvtxiedg  16791  wlkvtxiedgg  16792  wlk1walkdom  16805  g0wlk0  16816  wlkres  16825  trlf1  16834  trlreslem  16835  trlres  16836  clwwlkg  16839  clwwlkccatlem  16846  clwwlknon  16875  eupthfi  16897  eupthseg  16898  eupthres  16903  trlsegvdeglem1  16906  trlsegvdeglem7  16912  trlsegvdegfi  16913  eupth2lem3lem2fi  16915  eupth2lem3lem3fi  16916  eupth2lem3lem6fi  16917  eupth2lem3lem4fi  16919  eupth2lem3lem7fi  16920  eupth2lem3fi  16922  eupth2lemsfi  16924  eupth2fi  16925  konigsbergssiedgwen  16932  bj-inex  17138  bj-sucexg  17153  bj-peano4  17186  setindis  17198  bdsetindis  17200  bj-inf2vnlem1  17201  wexmiddiffilem  17248  wexmiddifxy  17251  nnsf  17254  nninfall  17258  nninfsellemeq  17263  sbthom  17277