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  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  7096  dom1o  7121  pw2f1odclem  7139  fopwdom  7141  xpen  7150  mapunen  7156  ssenen  7157  isinfinf  7206  ac6sfi  7207  preimaf1ofi  7274  sbthlem1  7280  fczfsuppd  7303  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  9757  zindd  9776  xrlttri3  10217  xnn0xadd0  10287  fzopth  10485  fzsuc  10493  fzpred  10495  fzp1ss  10498  fztp  10503  fseq1p1m1  10519  1fv  10564  elfzom1elp1fzo  10638  ssfzo12  10660  fzosplitsn  10669  zsupcllemstep  10680  zsupcllemex  10681  infssuzledc  10685  divfl0  10753  fldiv4lem1div2uz2  10763  modqid  10808  modqmuladdim  10826  frecuzrdgtcl  10871  frecuzrdgfunlem  10878  frecfzennn  10885  frecfzen2  10886  seq3val  10919  seqvalcd  10920  seqsplitg  10948  iseqf1olemqcl  10958  iseqf1olemnab  10960  iseqf1olemmo  10964  iseqf1olemqk  10966  seq3f1olemstep  10973  seqf1oglem2  10979  seq3id3  10983  seqhomog  10989  faclbnd  11202  faclbnd3  11204  bcm1k  11221  hashfz1  11245  hashfz  11285  hashfzp1  11288  fiubm  11294  hashfacen  11307  leisorel  11312  wrdexb  11339  wrdsymb  11355  wrdred1hash  11371  lsw0  11375  lswex  11379  ccat0  11387  ccatval2  11389  ccatw2s1leng  11429  ccats1val2  11431  swrds1  11463  swrdlsw  11464  ccats1pfxeqrex  11510  pfxccatin12lem1  11523  swrdccatin2  11524  swrdccat  11530  cats1fvd  11561  s1s2d  11589  s1s3d  11590  cjcj  11671  caucvgre  11770  r19.2uz  11782  resqrexlemgt0  11809  ltabs  11877  xrmaxiflemab  12039  xrmaxiflemlub  12040  nnf1o  12169  summodclem2a  12174  fsumf1o  12183  fisum0diag2  12240  modfsummodlemstep  12250  fsumparts  12263  clim2prod  12332  prodfap0  12338  prodmodclem2a  12369  fprodssdc  12383  fprodcllem  12399  ef0lem  12453  resinval  12508  recosval  12509  demoivreALT  12567  nn0o  12700  gcdmultiplez  12824  dvdssq  12834  nninfct  12844  eucalg  12863  lcmgcdnn  12886  dvdsnprmd  12929  prm2orodd  12930  isprm5lem  12946  qnumdenbi  12998  nn0gcdsq  13006  phibnd  13025  hashdvds  13029  phimullem  13033  prmdiveq  13044  hashgcdlem  13046  modprm0  13063  nnnn0modprm0  13064  modprmn0modprm0  13065  oddprm  13068  prm23lt5  13072  pcprendvds  13099  pcidlem  13132  pcmpt  13152  pcfac  13159  infpnlem2  13169  prmunb  13171  1arith  13176  4sqlem19  13218  ballotfilemfp1  13290  ballotfilemic  13309  ballotfilem1c  13310  ballotfilemsima  13318  ballotfilemrv  13322  ballotfilemro  13325  ballotfilemfrc  13329  ballotfilemfrci  13330  ballotfilemfrceq  13331  ballotfilemfrcn0  13332  ballotfilemrinv0  13335  unennn  13347  ennnfonelemk  13350  ennnfonelemjn  13352  ennnfonelemhf1o  13363  ennnfonelemex  13364  ennnfonelemf1  13368  ennnfonelemrn  13369  qnnen  13381  unbendc  13404  setsfun0  13447  srngbased  13561  srngplusgd  13562  srngmulrd  13563  srnginvld  13564  lmodbased  13579  lmodplusgd  13580  lmodscad  13581  lmodvscad  13582  ipsbased  13591  ipsaddgd  13592  ipsmulrd  13593  ipsscad  13594  ipsvscad  13595  ipsipd  13596  tgval  13676  gzsumval2  13774  isnsgrp  13781  ismnd  13792  dfgrp2e  13893  subgintm  14061  eqg0el  14092  ecqusaddcl  14102  kerf1ghm  14137  gzsumconst  14234  gsumvalfi  14243  gsumf1ofi  14251  gsumresfi  14264  gsum2dfilem2  14273  prdsbas3  14295  imasrng  14363  srgisid  14398  qusring2  14481  oppr1g  14498  dvdsr02  14522  isunitd  14523  crngunit  14528  unitpropdg  14565  elrhmunit  14594  subrngintm  14630  subrguss  14654  subrgunit  14657  subrgugrp  14658  subrgintm  14661  drngunz  14728  lmodfopnelem1  14771  rmodislmodlem  14797  rmodislmod  14798  lssuni  14810  islss3  14826  lss0v  14877  sraval  14884  rnglidlmmgm  14943  2idllidld  14953  2idlridld  14954  rng2idl0  14966  rng2idlsubg0  14969  zrh0  15070  znle  15082  zndvds0  15095  znf1o  15096  znleval  15098  znfi  15100  znhash  15101  znunit  15104  issubassa  15123  asclfval  15131  ascl0  15137  ascl1  15138  rnasclsubrg  15146  psrbaglecl  15174  psrass1filem  15182  psrbasg  15183  psradd  15188  psr0cl  15196  mpladd  15232  cldval  15337  ntrfval  15338  clsfval  15339  neifval  15378  neif  15379  neival  15381  cnclima  15461  cncnpi  15466  cnrest2  15474  cnrest2r  15475  cnptoprest  15477  cnpdis  15480  txvalex  15492  txval  15493  txcnmpt  15511  txdis  15515  cnmpt1t  15523  cnmpt2t  15531  hmeocnv  15545  hmeontr  15551  txhmeo  15557  xmetunirn  15596  xmettpos  15608  metn0  15616  xmetres  15620  metres  15621  blrnps  15649  blrn  15650  blin2  15670  blbas  15671  xmeterval  15673  xmettxlem  15747  xmettx  15748  metcnpi  15753  reldvg  15917  dvaddxx  15941  dvmulxx  15942  dviaddf  15943  dvimulf  15944  dvfre  15948  dvmptid  15954  dveflem  15964  elply2  15973  plyreres  16002  sinq12gt0  16069  logfac  16138  rprelogbdiv  16205  logbgcd1irr  16215  birthdaylem3  16239  ppinprm  16272  chtnprm  16274  ppiqp1le  16279  fsumdvdsmul  16297  bcmono  16316  bposlem1  16323  bposlem3  16325  bposlem5  16327  lgslem4  16339  lgsdirprm  16370  gausslemma2dlem0a  16385  gausslemma2dlem0f  16390  gausslemma2dlem0i  16393  gausslemma2dlem1a  16394  gausslemma2dlem1cl  16395  gausslemma2dlem5  16402  gausslemma2dlem6  16403  gausslemma2d  16405  lgseisenlem1  16406  lgseisenlem2  16407  lgseisenlem3  16408  lgseisen  16410  lgsquadlem1  16413  m1lgs  16421  2lgslem1a  16424  2lgslem1c  16426  2lgsoddprmlem2  16442  edgval  16518  edgstruct  16522  umgrnloopv  16572  umgredgprv  16573  upgr1edc  16579  umgredgne  16608  usgredgssen  16620  umgr2edg1  16667  uspgredg2vlem  16678  uspgr1edc  16698  uhgrspansubgrlem  16734  wlkm  16797  wlkvtxiedg  16803  wlkvtxiedgg  16804  wlk1walkdom  16817  g0wlk0  16828  wlkres  16837  trlf1  16846  trlreslem  16847  trlres  16848  clwwlkg  16851  clwwlkccatlem  16858  clwwlknon  16887  eupthfi  16909  eupthseg  16910  eupthres  16915  trlsegvdeglem1  16918  trlsegvdeglem7  16924  trlsegvdegfi  16925  eupth2lem3lem2fi  16927  eupth2lem3lem3fi  16928  eupth2lem3lem6fi  16929  eupth2lem3lem4fi  16931  eupth2lem3lem7fi  16932  eupth2lem3fi  16934  eupth2lemsfi  16936  eupth2fi  16937  konigsbergssiedgwen  16944  bj-inex  17150  bj-sucexg  17165  bj-peano4  17198  setindis  17210  bdsetindis  17212  bj-inf2vnlem1  17213  wexmiddiffilem  17260  wexmiddifxy  17263  nnsf  17266  nninfall  17270  nninfsellemeq  17275  sbthom  17289