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  6545  smores3  6569  smoiso  6578  tfr0dm  6598  tfrlemibxssdm  6603  tfrlemi14d  6609  tfrexlem  6610  tfr1onlemssrecs  6615  tfr1onlemsucfn  6616  tfr1onlemsucaccv  6617  tfr1onlembxssdm  6619  tfr1onlemres  6625  tfri1dALT  6627  tfrcllemssrecs  6628  tfrcllemsucfn  6629  tfrcllemsucaccv  6630  tfrcllembxssdm  6632  tfrcllemres  6638  rdgss  6659  nnsucsssuc  6770  nntr2  6781  swoord1  6841  swoord2  6842  iinerm  6886  eroveu  6905  pmresg  6962  en1uniel  7097  dom1o  7122  pw2f1odclem  7140  fopwdom  7142  xpen  7151  mapunen  7157  ssenen  7158  isinfinf  7207  ac6sfi  7208  preimaf1ofi  7275  sbthlem1  7281  fsuppfund  7299  fsuppfiss  7300  fczfsuppd  7304  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  9755  zindd  9774  xrlttri3  10215  xnn0xadd0  10285  fzopth  10483  fzsuc  10491  fzpred  10493  fzp1ss  10496  fztp  10501  fseq1p1m1  10517  1fv  10562  elfzom1elp1fzo  10636  ssfzo12  10658  fzosplitsn  10667  zsupcllemstep  10678  zsupcllemex  10679  infssuzledc  10683  divfl0  10751  fldiv4lem1div2uz2  10761  modqid  10806  modqmuladdim  10824  frecuzrdgtcl  10869  frecuzrdgfunlem  10876  frecfzennn  10883  frecfzen2  10884  seq3val  10917  seqvalcd  10918  seqsplitg  10946  iseqf1olemqcl  10956  iseqf1olemnab  10958  iseqf1olemmo  10962  iseqf1olemqk  10964  seq3f1olemstep  10971  seqf1oglem2  10977  seq3id3  10981  seqhomog  10987  faclbnd  11200  faclbnd3  11202  bcm1k  11219  hashfz1  11243  hashfz  11283  hashfzp1  11286  fiubm  11292  hashfacen  11305  leisorel  11310  wrdexb  11337  wrdsymb  11353  wrdred1hash  11369  lsw0  11373  lswex  11377  ccat0  11385  ccatval2  11387  ccatw2s1leng  11427  ccats1val2  11429  swrds1  11461  swrdlsw  11462  ccats1pfxeqrex  11508  pfxccatin12lem1  11521  swrdccatin2  11522  swrdccat  11528  cats1fvd  11559  s1s2d  11587  s1s3d  11588  cjcj  11669  caucvgre  11768  r19.2uz  11780  resqrexlemgt0  11807  ltabs  11875  xrmaxiflemab  12037  xrmaxiflemlub  12038  nnf1o  12167  summodclem2a  12172  fsumf1o  12181  fisum0diag2  12238  modfsummodlemstep  12248  fsumparts  12261  clim2prod  12330  prodfap0  12336  prodmodclem2a  12367  fprodssdc  12381  fprodcllem  12397  ef0lem  12451  resinval  12506  recosval  12507  demoivreALT  12565  nn0o  12698  gcdmultiplez  12822  dvdssq  12832  nninfct  12842  eucalg  12861  lcmgcdnn  12884  dvdsnprmd  12927  prm2orodd  12928  isprm5lem  12944  qnumdenbi  12996  nn0gcdsq  13004  phibnd  13023  hashdvds  13027  phimullem  13031  prmdiveq  13042  hashgcdlem  13044  modprm0  13061  nnnn0modprm0  13062  modprmn0modprm0  13063  oddprm  13066  prm23lt5  13070  pcprendvds  13097  pcidlem  13130  pcmpt  13150  pcfac  13157  infpnlem2  13167  prmunb  13169  1arith  13174  4sqlem19  13216  ballotfilemfp1  13288  ballotfilemic  13307  ballotfilem1c  13308  ballotfilemsima  13316  ballotfilemrv  13320  ballotfilemro  13323  ballotfilemfrc  13327  ballotfilemfrci  13328  ballotfilemfrceq  13329  ballotfilemfrcn0  13330  ballotfilemrinv0  13333  unennn  13345  ennnfonelemk  13348  ennnfonelemjn  13350  ennnfonelemhf1o  13361  ennnfonelemex  13362  ennnfonelemf1  13366  ennnfonelemrn  13367  qnnen  13379  unbendc  13402  setsfun0  13445  srngbased  13559  srngplusgd  13560  srngmulrd  13561  srnginvld  13562  lmodbased  13577  lmodplusgd  13578  lmodscad  13579  lmodvscad  13580  ipsbased  13589  ipsaddgd  13590  ipsmulrd  13591  ipsscad  13592  ipsvscad  13593  ipsipd  13594  tgval  13674  gzsumval2  13772  isnsgrp  13779  ismnd  13790  dfgrp2e  13891  subgintm  14059  eqg0el  14090  ecqusaddcl  14100  kerf1ghm  14135  gzsumconst  14232  gsumvalfi  14241  gsumf1ofi  14249  gsumresfi  14262  gsum2dfilem2  14271  prdsbas3  14293  imasrng  14361  srgisid  14396  qusring2  14479  oppr1g  14496  dvdsr02  14520  isunitd  14521  crngunit  14526  unitpropdg  14563  elrhmunit  14592  subrngintm  14628  subrguss  14652  subrgunit  14655  subrgugrp  14656  subrgintm  14659  drngunz  14726  lmodfopnelem1  14769  rmodislmodlem  14795  rmodislmod  14796  lssuni  14808  islss3  14824  lss0v  14875  sraval  14882  rnglidlmmgm  14941  2idllidld  14951  2idlridld  14952  rng2idl0  14964  rng2idlsubg0  14967  zrh0  15068  znle  15080  zndvds0  15093  znf1o  15094  znleval  15096  znfi  15098  znhash  15099  znunit  15102  issubassa  15121  asclfval  15129  ascl0  15135  ascl1  15136  rnasclsubrg  15144  psrbaglecl  15172  psrass1filem  15186  psrbasg  15187  psradd  15192  psr0cl  15200  mpladd  15237  cldval  15342  ntrfval  15343  clsfval  15344  neifval  15383  neif  15384  neival  15386  cnclima  15466  cncnpi  15471  cnrest2  15479  cnrest2r  15480  cnptoprest  15482  cnpdis  15485  txvalex  15497  txval  15498  txcnmpt  15516  txdis  15520  cnmpt1t  15528  cnmpt2t  15536  hmeocnv  15550  hmeontr  15556  txhmeo  15562  xmetunirn  15601  xmettpos  15613  metn0  15621  xmetres  15625  metres  15626  blrnps  15654  blrn  15655  blin2  15675  blbas  15676  xmeterval  15678  xmettxlem  15752  xmettx  15753  metcnpi  15758  reldvg  15922  dvaddxx  15946  dvmulxx  15947  dviaddf  15948  dvimulf  15949  dvfre  15953  dvmptid  15959  dveflem  15969  elply2  15978  plyreres  16007  sinq12gt0  16074  logfac  16143  rprelogbdiv  16210  logbgcd1irr  16220  birthdaylem3  16244  ppinprm  16277  chtnprm  16279  ppiqp1le  16284  fsumdvdsmul  16302  bcmono  16321  bposlem1  16328  bposlem3  16330  bposlem5  16332  lgslem4  16344  lgsdirprm  16375  gausslemma2dlem0a  16390  gausslemma2dlem0f  16395  gausslemma2dlem0i  16398  gausslemma2dlem1a  16399  gausslemma2dlem1cl  16400  gausslemma2dlem5  16407  gausslemma2dlem6  16408  gausslemma2d  16410  lgseisenlem1  16411  lgseisenlem2  16412  lgseisenlem3  16413  lgseisen  16415  lgsquadlem1  16418  m1lgs  16426  2lgslem1a  16429  2lgslem1c  16431  2lgsoddprmlem2  16447  edgval  16523  edgstruct  16527  umgrnloopv  16577  umgredgprv  16578  upgr1edc  16584  umgredgne  16613  usgredgssen  16625  umgr2edg1  16672  uspgredg2vlem  16683  uspgr1edc  16703  uhgrspansubgrlem  16739  wlkm  16802  wlkvtxiedg  16808  wlkvtxiedgg  16809  wlk1walkdom  16822  g0wlk0  16833  wlkres  16842  trlf1  16851  trlreslem  16852  trlres  16853  clwwlkg  16856  clwwlkccatlem  16863  clwwlknon  16892  eupthfi  16914  eupthseg  16915  eupthres  16920  trlsegvdeglem1  16923  trlsegvdeglem7  16929  trlsegvdegfi  16930  eupth2lem3lem2fi  16932  eupth2lem3lem3fi  16933  eupth2lem3lem6fi  16934  eupth2lem3lem4fi  16936  eupth2lem3lem7fi  16937  eupth2lem3fi  16939  eupth2lemsfi  16941  eupth2fi  16942  konigsbergssiedgwen  16949  bj-inex  17155  bj-sucexg  17170  bj-peano4  17203  setindis  17215  bdsetindis  17217  bj-inf2vnlem1  17218  wexmiddiffilem  17265  wexmiddifxy  17268  nnsf  17271  nninfall  17275  nninfsellemeq  17280  sbthom  17294