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  4340  exmid1stab  4345  snelpwi  4351  opth1  4376  frind  4497  onin  4531  abnexg  4592  reusv1  4604  xpexg  4889  reldmm  5000  dmexg  5046  rnexg  5047  elrelimasn  5153  relfld  5316  funimaexglem  5464  funimaexg  5465  fabexg  5579  fsnd  5684  elfvm  5729  nfvres  5732  funimass4  5753  elfvmptrab1  5801  funconstss  5827  f1oresrab  5873  resfunexg  5936  f1eqcocnv  5997  isores1  6020  isoini  6024  isose  6027  isopolem  6028  isosolem  6030  eusvobj2  6071  acexmidlemcase  6080  oprabid  6117  offval  6310  resfunexgALT  6337  offval3  6367  1stvalg  6376  2ndvalg  6377  1stcof  6397  2ndcof  6398  cnvf1o  6461  tposf12  6540  smores3  6564  smoiso  6573  tfr0dm  6593  tfrlemibxssdm  6598  tfrlemi14d  6604  tfrexlem  6605  tfr1onlemssrecs  6610  tfr1onlemsucfn  6611  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlemres  6620  tfri1dALT  6622  tfrcllemssrecs  6623  tfrcllemsucfn  6624  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllemres  6633  rdgss  6654  nnsucsssuc  6765  nntr2  6776  swoord1  6836  swoord2  6837  iinerm  6881  eroveu  6900  pmresg  6957  en1uniel  7091  dom1o  7116  pw2f1odclem  7134  fopwdom  7136  xpen  7145  mapunen  7151  ssenen  7152  isinfinf  7201  ac6sfi  7202  preimaf1ofi  7268  sbthlem1  7274  fczfsuppd  7297  fi0  7309  fiss  7311  supubti  7339  suplubti  7340  isotilem  7346  supisolem  7348  supisoex  7349  supisoti  7350  ordiso2  7375  eldju1st  7411  eldju2ndl  7412  updjud  7422  djudom  7433  ctmlemr  7448  enumctlemm  7454  nnnninfeq  7468  ctssexmid  7490  nninfwlpoimlemginf  7516  exmidonfinlem  7545  en2other2  7548  exmidaclem  7564  cc2lem  7632  cc3  7634  addclnq  7742  mulclnq  7743  1qec  7755  prarloclemarch2  7786  enq0tr  7801  addclnq0  7818  mulclnq0  7819  nq0m0r  7823  prarloclemlo  7861  prarloc  7870  genpml  7884  genpmu  7885  addnqprl  7896  addnqpru  7897  recnnpr  7915  prmuloc2  7934  1idpru  7958  ltexprlemm  7967  ltexprlemloc  7974  recexprlemm  7991  recexprlem1ssl  8000  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemm  8035  caucvgprlemopl  8036  caucvgprlemlol  8037  caucvgprlemladdfu  8044  caucvgprlemladdrl  8045  caucvgprprlemk  8050  caucvgprprlemloccalc  8051  caucvgprprlemnkltj  8056  caucvgprprlemnjltk  8058  caucvgprprlemml  8061  caucvgprprlemmu  8062  caucvgprprlemlol  8065  caucvgprprlemexb  8074  caucvgprprlem1  8076  suplocexprlemml  8083  suplocexprlemlub  8091  addclsr  8120  mulclsr  8121  prsrcl  8151  caucvgsrlemoffcau  8165  peano5nnnn  8259  mulap0r  8944  indv  9296  nn1suc  9324  prime  9747  zindd  9766  xrlttri3  10201  xnn0xadd0  10271  fzopth  10469  fzsuc  10477  fzpred  10479  fzp1ss  10482  fztp  10487  fseq1p1m1  10503  1fv  10548  elfzom1elp1fzo  10622  ssfzo12  10644  fzosplitsn  10653  zsupcllemstep  10664  zsupcllemex  10665  infssuzledc  10669  divfl0  10733  fldiv4lem1div2uz2  10743  modqid  10788  modqmuladdim  10806  frecuzrdgtcl  10851  frecuzrdgfunlem  10858  frecfzennn  10865  frecfzen2  10866  seq3val  10899  seqvalcd  10900  seqsplitg  10928  iseqf1olemqcl  10938  iseqf1olemnab  10940  iseqf1olemmo  10944  iseqf1olemqk  10946  seq3f1olemstep  10953  seqf1oglem2  10959  seq3id3  10963  seqhomog  10969  faclbnd  11181  faclbnd3  11183  bcm1k  11200  hashfz1  11224  hashfz  11264  hashfzp1  11267  fiubm  11273  hashfacen  11286  leisorel  11291  wrdexb  11318  wrdsymb  11334  wrdred1hash  11350  lsw0  11354  lswex  11358  ccat0  11366  ccatval2  11368  ccatw2s1leng  11408  ccats1val2  11410  swrds1  11442  swrdlsw  11443  ccats1pfxeqrex  11489  pfxccatin12lem1  11502  swrdccatin2  11503  swrdccat  11509  cats1fvd  11540  s1s2d  11568  s1s3d  11569  cjcj  11650  caucvgre  11749  r19.2uz  11761  resqrexlemgt0  11788  ltabs  11855  xrmaxiflemab  12015  xrmaxiflemlub  12016  nnf1o  12145  summodclem2a  12150  fsumf1o  12159  fisum0diag2  12216  modfsummodlemstep  12226  fsumparts  12239  clim2prod  12308  prodfap0  12314  prodmodclem2a  12345  fprodssdc  12359  fprodcllem  12375  ef0lem  12429  resinval  12484  recosval  12485  demoivreALT  12543  nn0o  12676  gcdmultiplez  12800  dvdssq  12810  nninfct  12820  eucalg  12839  lcmgcdnn  12862  dvdsnprmd  12905  prm2orodd  12906  isprm5lem  12921  qnumdenbi  12972  nn0gcdsq  12980  phibnd  12997  hashdvds  13001  phimullem  13005  prmdiveq  13016  hashgcdlem  13018  modprm0  13035  nnnn0modprm0  13036  modprmn0modprm0  13037  oddprm  13040  prm23lt5  13044  pcprendvds  13071  pcidlem  13104  pcmpt  13124  pcfac  13131  infpnlem2  13141  prmunb  13143  1arith  13148  4sqlem19  13190  ballotfilemfp1  13233  ballotfilemic  13252  ballotfilem1c  13253  ballotfilemsima  13261  ballotfilemrv  13265  ballotfilemro  13268  ballotfilemfrc  13272  ballotfilemfrci  13273  ballotfilemfrceq  13274  ballotfilemfrcn0  13275  ballotfilemrinv0  13278  unennn  13290  ennnfonelemk  13293  ennnfonelemjn  13295  ennnfonelemhf1o  13306  ennnfonelemex  13307  ennnfonelemf1  13311  ennnfonelemrn  13312  qnnen  13324  unbendc  13347  setsfun0  13390  srngbased  13503  srngplusgd  13504  srngmulrd  13505  srnginvld  13506  lmodbased  13521  lmodplusgd  13522  lmodscad  13523  lmodvscad  13524  ipsbased  13533  ipsaddgd  13534  ipsmulrd  13535  ipsscad  13536  ipsvscad  13537  ipsipd  13538  tgval  13618  gzsumval2  13716  isnsgrp  13723  ismnd  13734  dfgrp2e  13835  subgintm  14003  eqg0el  14034  ecqusaddcl  14044  kerf1ghm  14079  gzsumconst  14145  gsumvalfi  14154  gsumf1ofi  14162  prdsbas3  14189  imasrng  14257  srgisid  14292  qusring2  14373  oppr1g  14390  dvdsr02  14414  isunitd  14415  crngunit  14420  unitpropdg  14457  elrhmunit  14486  subrngintm  14522  subrguss  14546  subrgunit  14549  subrgugrp  14550  subrgintm  14553  drngunz  14620  lmodfopnelem1  14663  rmodislmodlem  14689  rmodislmod  14690  lssuni  14702  islss3  14718  lss0v  14769  sraval  14776  rnglidlmmgm  14835  2idllidld  14845  2idlridld  14846  rng2idl0  14858  rng2idlsubg0  14861  zrh0  14962  znle  14974  zndvds0  14987  znf1o  14988  znleval  14990  znfi  14992  znhash  14993  znunit  14996  issubassa  15015  asclfval  15023  ascl0  15029  ascl1  15030  rnasclsubrg  15038  psrbaglecl  15062  psrbasg  15067  psradd  15072  psr0cl  15074  mpladd  15097  cldval  15202  ntrfval  15203  clsfval  15204  neifval  15243  neif  15244  neival  15246  cnclima  15326  cncnpi  15331  cnrest2  15339  cnrest2r  15340  cnptoprest  15342  cnpdis  15345  txvalex  15357  txval  15358  txcnmpt  15376  txdis  15380  cnmpt1t  15388  cnmpt2t  15396  hmeocnv  15410  hmeontr  15416  txhmeo  15422  xmetunirn  15461  xmettpos  15473  metn0  15481  xmetres  15485  metres  15486  blrnps  15514  blrn  15515  blin2  15535  blbas  15536  xmeterval  15538  xmettxlem  15612  xmettx  15613  metcnpi  15618  reldvg  15782  dvaddxx  15806  dvmulxx  15807  dviaddf  15808  dvimulf  15809  dvfre  15813  dvmptid  15819  dveflem  15829  elply2  15838  plyreres  15867  sinq12gt0  15934  logfac  16001  rprelogbdiv  16065  logbgcd1irr  16075  birthdaylem3  16095  fsumdvdsmul  16111  bcmono  16124  lgslem4  16134  lgsdirprm  16165  gausslemma2dlem0a  16180  gausslemma2dlem0f  16185  gausslemma2dlem0i  16188  gausslemma2dlem1a  16189  gausslemma2dlem1cl  16190  gausslemma2dlem5  16197  gausslemma2dlem6  16198  gausslemma2d  16200  lgseisenlem1  16201  lgseisenlem2  16202  lgseisenlem3  16203  lgseisen  16205  lgsquadlem1  16208  m1lgs  16216  2lgslem1a  16219  2lgslem1c  16221  2lgsoddprmlem2  16237  edgval  16313  edgstruct  16317  umgrnloopv  16367  umgredgprv  16368  upgr1edc  16374  umgredgne  16403  usgredgssen  16415  umgr2edg1  16462  uspgredg2vlem  16473  uspgr1edc  16493  uhgrspansubgrlem  16529  wlkm  16592  wlkvtxiedg  16598  wlkvtxiedgg  16599  wlk1walkdom  16612  g0wlk0  16623  wlkres  16632  trlf1  16641  trlreslem  16642  trlres  16643  clwwlkg  16646  clwwlkccatlem  16653  clwwlknon  16682  eupthfi  16704  eupthseg  16705  eupthres  16710  trlsegvdeglem1  16713  trlsegvdeglem7  16719  trlsegvdegfi  16720  eupth2lem3lem2fi  16722  eupth2lem3lem3fi  16723  eupth2lem3lem6fi  16724  eupth2lem3lem4fi  16726  eupth2lem3lem7fi  16727  eupth2lem3fi  16729  eupth2lemsfi  16731  eupth2fi  16732  konigsbergssiedgwen  16739  bj-inex  16945  bj-sucexg  16960  bj-peano4  16993  setindis  17005  bdsetindis  17007  bj-inf2vnlem1  17008  wexmiddiffilem  17055  wexmiddifxy  17058  nnsf  17060  nninfall  17064  nninfsellemeq  17069  sbthom  17083