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 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  4syl  18  simpl2im  386  hbim  1594  nfal  1625  19.9hd  1710  equsexd  1777  sbcof2  1858  aev  1860  sbequi  1887  nfsbd  2030  mo2n  2107  eupickb  2161  r19.29af2  2674  spc2gv  2898  spc3gv  2900  eqvincg  2931  sbcco3g  3186  ssrmof  3291  exmidsssnc  4299  exmid1stab  4304  snelpwi  4309  opth1  4334  frind  4455  onin  4489  abnexg  4549  reusv1  4561  xpexg  4846  reldmm  4956  dmexg  5002  rnexg  5003  elrelimasn  5109  relfld  5272  funimaexglem  5420  funimaexg  5421  fabexg  5532  fsnd  5637  elfvm  5681  nfvres  5684  funimass4  5705  elfvmptrab1  5750  funconstss  5774  f1oresrab  5820  resfunexg  5883  f1eqcocnv  5942  isores1  5965  isoini  5969  isose  5972  isopolem  5973  isosolem  5975  eusvobj2  6014  acexmidlemcase  6023  oprabid  6060  offval  6252  resfunexgALT  6279  offval3  6305  1stvalg  6314  2ndvalg  6315  1stcof  6335  2ndcof  6336  cnvf1o  6399  tposf12  6478  smores3  6502  smoiso  6511  tfr0dm  6531  tfrlemibxssdm  6536  tfrlemi14d  6542  tfrexlem  6543  tfr1onlemssrecs  6548  tfr1onlemsucfn  6549  tfr1onlemsucaccv  6550  tfr1onlembxssdm  6552  tfr1onlemres  6558  tfri1dALT  6560  tfrcllemssrecs  6561  tfrcllemsucfn  6562  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllemres  6571  rdgss  6592  nnsucsssuc  6703  nntr2  6714  swoord1  6774  swoord2  6775  iinerm  6819  eroveu  6838  pmresg  6888  en1uniel  7021  dom1o  7045  pw2f1odclem  7063  fopwdom  7065  xpen  7074  ssenen  7080  isinfinf  7129  ac6sfi  7130  preimaf1ofi  7193  sbthlem1  7199  fi0  7217  fiss  7219  supubti  7241  suplubti  7242  isotilem  7248  supisolem  7250  supisoex  7251  supisoti  7252  ordiso2  7277  eldju1st  7313  eldju2ndl  7314  updjud  7324  djudom  7335  ctmlemr  7350  enumctlemm  7356  nnnninfeq  7370  ctssexmid  7392  nninfwlpoimlemginf  7418  exmidonfinlem  7447  en2other2  7450  exmidaclem  7466  cc2lem  7528  cc3  7530  addclnq  7638  mulclnq  7639  1qec  7651  prarloclemarch2  7682  enq0tr  7697  addclnq0  7714  mulclnq0  7715  nq0m0r  7719  prarloclemlo  7757  prarloc  7766  genpml  7780  genpmu  7781  addnqprl  7792  addnqpru  7793  recnnpr  7811  prmuloc2  7830  1idpru  7854  ltexprlemm  7863  ltexprlemloc  7870  recexprlemm  7887  recexprlem1ssl  7896  caucvgprlemnkj  7929  caucvgprlemnbj  7930  caucvgprlemm  7931  caucvgprlemopl  7932  caucvgprlemlol  7933  caucvgprlemladdfu  7940  caucvgprlemladdrl  7941  caucvgprprlemk  7946  caucvgprprlemloccalc  7947  caucvgprprlemnkltj  7952  caucvgprprlemnjltk  7954  caucvgprprlemml  7957  caucvgprprlemmu  7958  caucvgprprlemlol  7961  caucvgprprlemexb  7970  caucvgprprlem1  7972  suplocexprlemml  7979  suplocexprlemlub  7987  addclsr  8016  mulclsr  8017  prsrcl  8047  caucvgsrlemoffcau  8061  peano5nnnn  8155  mulap0r  8838  nn1suc  9205  prime  9622  zindd  9641  xrlttri3  10075  xnn0xadd0  10145  fzopth  10339  fzsuc  10347  fzpred  10348  fzp1ss  10351  fztp  10356  fseq1p1m1  10372  1fv  10417  elfzom1elp1fzo  10491  ssfzo12  10513  fzosplitsn  10522  zsupcllemstep  10533  zsupcllemex  10534  infssuzledc  10538  divfl0  10600  fldiv4lem1div2uz2  10610  modqid  10655  modqmuladdim  10673  frecuzrdgtcl  10718  frecuzrdgfunlem  10725  frecfzennn  10732  frecfzen2  10733  seq3val  10766  seqvalcd  10767  seqsplitg  10795  iseqf1olemqcl  10805  iseqf1olemnab  10807  iseqf1olemmo  10811  iseqf1olemqk  10813  seq3f1olemstep  10820  seqf1oglem2  10826  seq3id3  10830  seqhomog  10836  faclbnd  11047  faclbnd3  11049  bcm1k  11066  hashfz1  11089  hashfz  11129  hashfzp1  11132  fiubm  11136  hashfacen  11144  leisorel  11145  wrdexb  11172  wrdsymb  11188  wrdred1hash  11204  lsw0  11208  lswex  11212  ccat0  11220  ccatval2  11222  ccatw2s1leng  11262  ccats1val2  11264  swrds1  11296  swrdlsw  11297  ccats1pfxeqrex  11343  pfxccatin12lem1  11356  swrdccatin2  11357  swrdccat  11363  cats1fvd  11394  s1s2d  11422  s1s3d  11423  cjcj  11504  caucvgre  11602  r19.2uz  11614  resqrexlemgt0  11641  ltabs  11708  xrmaxiflemab  11868  xrmaxiflemlub  11869  nnf1o  11998  summodclem2a  12003  fsumf1o  12012  fisum0diag2  12069  modfsummodlemstep  12079  fsumparts  12092  clim2prod  12161  prodfap0  12167  prodmodclem2a  12198  fprodssdc  12212  fprodcllem  12228  ef0lem  12282  resinval  12337  recosval  12338  demoivreALT  12396  nn0o  12529  gcdmultiplez  12653  dvdssq  12663  nninfct  12673  eucalg  12692  lcmgcdnn  12715  dvdsnprmd  12758  prm2orodd  12759  isprm5lem  12774  qnumdenbi  12825  nn0gcdsq  12833  phibnd  12850  hashdvds  12854  phimullem  12858  prmdiveq  12869  hashgcdlem  12871  modprm0  12888  nnnn0modprm0  12889  modprmn0modprm0  12890  oddprm  12893  prm23lt5  12897  pcprendvds  12924  pcidlem  12957  pcmpt  12977  pcfac  12984  infpnlem2  12994  prmunb  12996  1arith  13001  4sqlem19  13043  unennn  13079  ennnfonelemk  13082  ennnfonelemjn  13084  ennnfonelemhf1o  13095  ennnfonelemex  13096  ennnfonelemf1  13100  ennnfonelemrn  13101  qnnen  13113  unbendc  13136  setsfun0  13179  srngbased  13291  srngplusgd  13292  srngmulrd  13293  srnginvld  13294  lmodbased  13309  lmodplusgd  13310  lmodscad  13311  lmodvscad  13312  ipsbased  13321  ipsaddgd  13322  ipsmulrd  13323  ipsscad  13324  ipsvscad  13325  ipsipd  13326  tgval  13406  prdsbas3  13431  isnsgrp  13550  ismnd  13563  dfgrp2e  13672  subgintm  13846  eqg0el  13877  ecqusaddcl  13887  kerf1ghm  13922  gsumfzconst  13989  imasrng  14031  srgisid  14061  srg1zr  14062  qusring2  14141  oppr1g  14157  dvdsr02  14181  isunitd  14182  crngunit  14187  unitpropdg  14224  elrhmunit  14253  subrngintm  14288  subrguss  14312  subrgunit  14315  subrgugrp  14316  subrgintm  14319  lmodfopnelem1  14400  rmodislmodlem  14426  rmodislmod  14427  lssuni  14439  islss3  14455  lss0v  14506  sraval  14513  rnglidlmmgm  14572  2idllidld  14582  2idlridld  14583  rng2idl0  14595  rng2idlsubg0  14598  zrh0  14701  znle  14713  zndvds0  14726  znf1o  14727  znleval  14729  znfi  14731  znhash  14732  znunit  14735  psrbaglecl  14751  psrbasg  14755  psradd  14760  psr0cl  14762  mpladd  14785  cldval  14890  ntrfval  14891  clsfval  14892  neifval  14931  neif  14932  neival  14934  cnclima  15014  cncnpi  15019  cnrest2  15027  cnrest2r  15028  cnptoprest  15030  cnpdis  15033  txvalex  15045  txval  15046  txcnmpt  15064  txdis  15068  cnmpt1t  15076  cnmpt2t  15084  hmeocnv  15098  hmeontr  15104  txhmeo  15110  xmetunirn  15149  xmettpos  15161  metn0  15169  xmetres  15173  metres  15174  blrnps  15202  blrn  15203  blin2  15223  blbas  15224  xmeterval  15226  xmettxlem  15300  xmettx  15301  metcnpi  15306  reldvg  15470  dvaddxx  15494  dvmulxx  15495  dviaddf  15496  dvimulf  15497  dvfre  15501  dvmptid  15507  dveflem  15517  elply2  15526  plyreres  15555  sinq12gt0  15621  rprelogbdiv  15748  logbgcd1irr  15758  fsumdvdsmul  15785  lgslem4  15802  lgsdirprm  15833  gausslemma2dlem0a  15848  gausslemma2dlem0f  15853  gausslemma2dlem0i  15856  gausslemma2dlem1a  15857  gausslemma2dlem1cl  15858  gausslemma2dlem5  15865  gausslemma2dlem6  15866  gausslemma2d  15868  lgseisenlem1  15869  lgseisenlem2  15870  lgseisenlem3  15871  lgseisen  15873  lgsquadlem1  15876  m1lgs  15884  2lgslem1a  15887  2lgslem1c  15889  2lgsoddprmlem2  15905  edgval  15981  edgstruct  15985  umgrnloopv  16035  umgredgprv  16036  upgr1edc  16042  umgredgne  16071  usgredgssen  16083  umgr2edg1  16130  uspgredg2vlem  16141  uspgr1edc  16161  uhgrspansubgrlem  16197  wlkm  16260  wlkvtxiedg  16266  wlkvtxiedgg  16267  wlk1walkdom  16280  g0wlk0  16291  wlkres  16300  trlf1  16309  trlreslem  16310  trlres  16311  clwwlkg  16314  clwwlkccatlem  16321  clwwlknon  16350  eupthfi  16372  eupthseg  16373  eupthres  16378  trlsegvdeglem1  16381  trlsegvdeglem7  16387  trlsegvdegfi  16388  eupth2lem3lem2fi  16390  eupth2lem3lem3fi  16391  eupth2lem3lem6fi  16392  eupth2lem3lem4fi  16394  eupth2lem3lem7fi  16395  eupth2lem3fi  16397  eupth2lemsfi  16399  eupth2fi  16400  konigsbergssiedgwen  16407  bj-inex  16603  bj-sucexg  16618  bj-peano4  16651  setindis  16663  bdsetindis  16665  bj-inf2vnlem1  16666  nnsf  16711  nninfall  16715  nninfsellemeq  16720  sbthom  16734  gfsumval  16789