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-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  4syl  18  simpl2im  381  hbim  1507  19.9hd  1623  equsexd  1690  sbcof2  1764  aev  1766  sbequi  1793  nfsbd  1926  mo2n  2003  eupickb  2056  r19.29af2  2546  spc2gv  2747  spc3gv  2749  eqvincg  2779  sbcco3g  3023  ssrmof  3126  exmidsssnc  4086  snelpwi  4094  opth1  4118  frind  4234  onin  4268  abnexg  4327  reusv1  4339  xpexg  4613  dmexg  4761  rnexg  4762  relfld  5025  funimaexglem  5164  funimaexg  5165  fabexg  5268  nfvres  5408  funimass4  5426  elfvmptrab1  5469  funconstss  5492  f1oresrab  5539  resfunexg  5595  f1eqcocnv  5646  isores1  5669  isoini  5673  isose  5676  isopolem  5677  isosolem  5679  eusvobj2  5714  acexmidlemcase  5723  oprabid  5757  offval  5943  resfunexgALT  5962  offval3  5986  1stvalg  5994  2ndvalg  5995  1stcof  6015  2ndcof  6016  cnvf1o  6076  tposf12  6120  smores3  6144  smoiso  6153  tfr0dm  6173  tfrlemibxssdm  6178  tfrlemi14d  6184  tfrexlem  6185  tfr1onlemssrecs  6190  tfr1onlemsucfn  6191  tfr1onlemsucaccv  6192  tfr1onlembxssdm  6194  tfr1onlemres  6200  tfri1dALT  6202  tfrcllemssrecs  6203  tfrcllemsucfn  6204  tfrcllemsucaccv  6205  tfrcllembxssdm  6207  tfrcllemres  6213  rdgss  6234  nnsucsssuc  6342  nntr2  6353  swoord1  6412  swoord2  6413  iinerm  6455  eroveu  6474  pmresg  6524  en1uniel  6652  fopwdom  6683  xpen  6692  ssenen  6698  isinfinf  6744  ac6sfi  6745  preimaf1ofi  6791  sbthlem1  6797  fi0  6815  fiss  6817  supubti  6838  suplubti  6839  isotilem  6845  supisolem  6847  supisoex  6848  supisoti  6849  ordiso2  6872  eldju1st  6908  eldju2ndl  6909  updjud  6919  djudom  6930  ctmlemr  6945  enumctlemm  6951  ctssexmid  6974  en2other2  7000  exmidaclem  7012  addclnq  7131  mulclnq  7132  1qec  7144  prarloclemarch2  7175  enq0tr  7190  addclnq0  7207  mulclnq0  7208  nq0m0r  7212  prarloclemlo  7250  prarloc  7259  genpml  7273  genpmu  7274  addnqprl  7285  addnqpru  7286  recnnpr  7304  prmuloc2  7323  1idpru  7347  ltexprlemm  7356  ltexprlemloc  7363  recexprlemm  7380  recexprlem1ssl  7389  caucvgprlemnkj  7422  caucvgprlemnbj  7423  caucvgprlemm  7424  caucvgprlemopl  7425  caucvgprlemlol  7426  caucvgprlemladdfu  7433  caucvgprlemladdrl  7434  caucvgprprlemk  7439  caucvgprprlemloccalc  7440  caucvgprprlemnkltj  7445  caucvgprprlemnjltk  7447  caucvgprprlemml  7450  caucvgprprlemmu  7451  caucvgprprlemlol  7454  caucvgprprlemexb  7463  caucvgprprlem1  7465  addclsr  7496  mulclsr  7497  prsrcl  7526  caucvgsrlemoffcau  7540  peano5nnnn  7627  mulap0r  8295  nn1suc  8649  prime  9054  zindd  9073  xrlttri3  9476  xnn0xadd0  9543  fzopth  9734  fzsuc  9742  fzpred  9743  fzp1ss  9746  fztp  9751  fseq1p1m1  9767  1fv  9809  elfzom1elp1fzo  9872  ssfzo12  9894  fzosplitsn  9903  divfl0  9962  modqid  10015  modqmuladdim  10033  frecuzrdgtcl  10078  frecuzrdgfunlem  10085  frecfzennn  10092  frecfzen2  10093  seq3val  10124  seqvalcd  10125  iseqf1olemqcl  10152  iseqf1olemnab  10154  iseqf1olemmo  10158  iseqf1olemqk  10160  seq3f1olemstep  10167  seq3id3  10173  faclbnd  10380  faclbnd3  10382  bcm1k  10399  hashfz1  10422  focdmex  10426  hashfz  10460  hashfzp1  10463  hashfacen  10472  leisorel  10473  cjcj  10548  caucvgre  10645  r19.2uz  10657  resqrexlemgt0  10684  ltabs  10751  xrmaxiflemab  10908  xrmaxiflemlub  10909  isummolemnm  11040  summodclem2a  11042  fsumf1o  11051  fisum0diag2  11108  modfsummodlemstep  11118  fsumparts  11131  ef0lem  11217  resinval  11273  recosval  11274  demoivreALT  11330  nn0o  11452  zsupcllemstep  11486  zsupcllemex  11487  infssuzledc  11491  gcdmultiplez  11555  dvdssq  11565  eucalg  11586  lcmgcdnn  11609  dvdsnprmd  11652  prm2orodd  11653  qnumdenbi  11715  nn0gcdsq  11723  phibnd  11738  hashdvds  11742  phimullem  11746  hashgcdlem  11748  unennn  11755  ennnfonelemk  11758  ennnfonelemjn  11760  ennnfonelemhf1o  11771  ennnfonelemex  11772  ennnfonelemf1  11776  ennnfonelemrn  11777  qnnen  11789  setsfun0  11838  srngbased  11925  srngplusgd  11926  srngmulrd  11927  srnginvld  11928  lmodbased  11936  lmodplusgd  11937  lmodscad  11938  lmodvscad  11939  ipsbased  11944  ipsaddgd  11945  ipsmulrd  11946  ipsscad  11947  ipsvscad  11948  ipsipd  11949  tgval  12061  cldval  12111  ntrfval  12112  clsfval  12113  neifval  12152  neif  12153  neival  12155  cnclima  12234  cncnpi  12239  cnrest2  12247  cnrest2r  12248  cnptoprest  12250  cnpdis  12253  txvalex  12265  txval  12266  txcnmpt  12284  txdis  12288  cnmpt1t  12296  cnmpt2t  12304  xmetunirn  12347  xmettpos  12359  metn0  12367  xmetres  12371  metres  12372  blrnps  12400  blrn  12401  blin2  12421  blbas  12422  xmeterval  12424  xmettxlem  12498  xmettx  12499  metcnpi  12504  reldvg  12603  dvaddxx  12622  dvmulxx  12623  dviaddf  12624  dvimulf  12625  bj-inex  12795  bj-sucexg  12810  bj-peano4  12843  setindis  12855  bdsetindis  12857  bj-inf2vnlem1  12858  exmid1stab  12885  nnsf  12889  nninfalllemn  12892  nninfall  12894  nninfsellemeq  12900  sbthom  12911