Theorem 3syl 17

Description: Inference chaining two syllogisms. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
3syl.1	⊢ (𝜑 → 𝜓)
3syl.2	⊢ (𝜓 → 𝜒)
3syl.3	⊢ (𝜒 → 𝜃)

Assertion

Ref	Expression
3syl	⊢ (𝜑 → 𝜃)

Proof of Theorem 3syl

Step	Hyp	Ref	Expression
1		3syl.1	. . 3 ⊢ (𝜑 → 𝜓)
2		3syl.2	. . 3 ⊢ (𝜓 → 𝜒)
3	1, 2	syl 14	. 2 ⊢ (𝜑 → 𝜒)
4		3syl.3	. 2 ⊢ (𝜒 → 𝜃)
5	3, 4	syl 14	1 ⊢ (𝜑 → 𝜃)

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  7300  fsuppfiss  7301  fczfsuppd  7305  fi0  7315  fiss  7317  supubti  7346  suplubti  7347  isotilem  7353  supisolem  7355  supisoex  7356  supisoti  7357  ordiso2  7382  eldju1st  7418  eldju2ndl  7419  updjud  7429  djudom  7440  ctmlemr  7455  enumctlemm  7461  nnnninfeq  7475  ctssexmid  7497  nninfwlpoimlemginf  7523  exmidonfinlem  7552  en2other2  7555  exmidaclem  7571  cc2lem  7639  cc3  7641  addclnq  7749  mulclnq  7750  1qec  7762  prarloclemarch2  7793  enq0tr  7808  addclnq0  7825  mulclnq0  7826  nq0m0r  7830  prarloclemlo  7868  prarloc  7877  genpml  7891  genpmu  7892  addnqprl  7903  addnqpru  7904  recnnpr  7922  prmuloc2  7941  1idpru  7965  ltexprlemm  7974  ltexprlemloc  7981  recexprlemm  7998  recexprlem1ssl  8007  caucvgprlemnkj  8040  caucvgprlemnbj  8041  caucvgprlemm  8042  caucvgprlemopl  8043  caucvgprlemlol  8044  caucvgprlemladdfu  8051  caucvgprlemladdrl  8052  caucvgprprlemk  8057  caucvgprprlemloccalc  8058  caucvgprprlemnkltj  8063  caucvgprprlemnjltk  8065  caucvgprprlemml  8068  caucvgprprlemmu  8069  caucvgprprlemlol  8072  caucvgprprlemexb  8081  caucvgprprlem1  8083  suplocexprlemml  8090  suplocexprlemlub  8098  addclsr  8127  mulclsr  8128  prsrcl  8158  caucvgsrlemoffcau  8172  peano5nnnn  8266  mulap0r  8952  indv  9305  nn1suc  9333  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  15173  psrass1filem  15196  psrbasg  15197  psradd  15202  psr0cl  15211  mpladd  15253  cldval  15358  ntrfval  15359  clsfval  15360  neifval  15399  neif  15400  neival  15402  cnclima  15482  cncnpi  15487  cnrest2  15495  cnrest2r  15496  cnptoprest  15498  cnpdis  15501  txvalex  15513  txval  15514  txcnmpt  15532  txdis  15536  cnmpt1t  15544  cnmpt2t  15552  hmeocnv  15566  hmeontr  15572  txhmeo  15578  xmetunirn  15617  xmettpos  15629  metn0  15637  xmetres  15641  metres  15642  blrnps  15670  blrn  15671  blin2  15691  blbas  15692  xmeterval  15694  xmettxlem  15768  xmettx  15769  metcnpi  15774  reldvg  15938  dvaddxx  15962  dvmulxx  15963  dviaddf  15964  dvimulf  15965  dvfre  15969  dvmptid  15975  dveflem  15985  elply2  15994  plyreres  16023  sinq12gt0  16090  logfac  16159  rprelogbdiv  16226  logbgcd1irr  16236  birthdaylem3  16260  ppinprm  16293  chtnprm  16295  ppiqp1le  16300  fsumdvdsmul  16318  bcmono  16337  bposlem1  16344  bposlem3  16346  bposlem5  16348  lgslem4  16360  lgsdirprm  16391  gausslemma2dlem0a  16406  gausslemma2dlem0f  16411  gausslemma2dlem0i  16414  gausslemma2dlem1a  16415  gausslemma2dlem1cl  16416  gausslemma2dlem5  16423  gausslemma2dlem6  16424  gausslemma2d  16426  lgseisenlem1  16427  lgseisenlem2  16428  lgseisenlem3  16429  lgseisen  16431  lgsquadlem1  16434  m1lgs  16442  2lgslem1a  16445  2lgslem1c  16447  2lgsoddprmlem2  16463  edgval  16539  edgstruct  16543  umgrnloopv  16593  umgredgprv  16594  upgr1edc  16600  umgredgne  16629  usgredgssen  16641  umgr2edg1  16688  uspgredg2vlem  16699  uspgr1edc  16719  uhgrspansubgrlem  16755  wlkm  16818  wlkvtxiedg  16824  wlkvtxiedgg  16825  wlk1walkdom  16838  g0wlk0  16849  wlkres  16858  trlf1  16867  trlreslem  16868  trlres  16869  clwwlkg  16872  clwwlkccatlem  16879  clwwlknon  16908  eupthfi  16930  eupthseg  16931  eupthres  16936  trlsegvdeglem1  16939  trlsegvdeglem7  16945  trlsegvdegfi  16946  eupth2lem3lem2fi  16948  eupth2lem3lem3fi  16949  eupth2lem3lem6fi  16950  eupth2lem3lem4fi  16952  eupth2lem3lem7fi  16953  eupth2lem3fi  16955  eupth2lemsfi  16957  eupth2fi  16958  konigsbergssiedgwen  16965  bj-inex  17171  bj-sucexg  17186  bj-peano4  17219  setindis  17231  bdsetindis  17233  bj-inf2vnlem1  17234  wexmiddiffilem  17281  wexmiddifxy  17284  nnsf  17287  nninfall  17291  nninfsellemeq  17296  sbthom  17310