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  384  hbim  1532  nfal  1563  19.9hd  1649  equsexd  1716  sbcof2  1797  aev  1799  sbequi  1826  nfsbd  1964  mo2n  2041  eupickb  2094  r19.29af2  2604  spc2gv  2812  spc3gv  2814  eqvincg  2845  sbcco3g  3097  ssrmof  3200  exmidsssnc  4176  snelpwi  4184  opth1  4208  frind  4324  onin  4358  abnexg  4418  reusv1  4430  xpexg  4712  dmexg  4862  rnexg  4863  relfld  5126  funimaexglem  5265  funimaexg  5266  fabexg  5369  fsnd  5469  nfvres  5513  funimass4  5531  elfvmptrab1  5574  funconstss  5597  f1oresrab  5644  resfunexg  5700  f1eqcocnv  5753  isores1  5776  isoini  5780  isose  5783  isopolem  5784  isosolem  5786  eusvobj2  5822  acexmidlemcase  5831  oprabid  5865  offval  6051  resfunexgALT  6070  offval3  6094  1stvalg  6102  2ndvalg  6103  1stcof  6123  2ndcof  6124  cnvf1o  6184  tposf12  6228  smores3  6252  smoiso  6261  tfr0dm  6281  tfrlemibxssdm  6286  tfrlemi14d  6292  tfrexlem  6293  tfr1onlemssrecs  6298  tfr1onlemsucfn  6299  tfr1onlemsucaccv  6300  tfr1onlembxssdm  6302  tfr1onlemres  6308  tfri1dALT  6310  tfrcllemssrecs  6311  tfrcllemsucfn  6312  tfrcllemsucaccv  6313  tfrcllembxssdm  6315  tfrcllemres  6321  rdgss  6342  nnsucsssuc  6451  nntr2  6462  swoord1  6521  swoord2  6522  iinerm  6564  eroveu  6583  pmresg  6633  en1uniel  6761  fopwdom  6793  xpen  6802  ssenen  6808  isinfinf  6854  ac6sfi  6855  preimaf1ofi  6907  sbthlem1  6913  fi0  6931  fiss  6933  supubti  6955  suplubti  6956  isotilem  6962  supisolem  6964  supisoex  6965  supisoti  6966  ordiso2  6991  eldju1st  7027  eldju2ndl  7028  updjud  7038  djudom  7049  ctmlemr  7064  enumctlemm  7070  nnnninfeq  7083  ctssexmid  7105  exmidonfinlem  7140  en2other2  7143  exmidaclem  7155  cc2lem  7198  cc3  7200  addclnq  7307  mulclnq  7308  1qec  7320  prarloclemarch2  7351  enq0tr  7366  addclnq0  7383  mulclnq0  7384  nq0m0r  7388  prarloclemlo  7426  prarloc  7435  genpml  7449  genpmu  7450  addnqprl  7461  addnqpru  7462  recnnpr  7480  prmuloc2  7499  1idpru  7523  ltexprlemm  7532  ltexprlemloc  7539  recexprlemm  7556  recexprlem1ssl  7565  caucvgprlemnkj  7598  caucvgprlemnbj  7599  caucvgprlemm  7600  caucvgprlemopl  7601  caucvgprlemlol  7602  caucvgprlemladdfu  7609  caucvgprlemladdrl  7610  caucvgprprlemk  7615  caucvgprprlemloccalc  7616  caucvgprprlemnkltj  7621  caucvgprprlemnjltk  7623  caucvgprprlemml  7626  caucvgprprlemmu  7627  caucvgprprlemlol  7630  caucvgprprlemexb  7639  caucvgprprlem1  7641  suplocexprlemml  7648  suplocexprlemlub  7656  addclsr  7685  mulclsr  7686  prsrcl  7716  caucvgsrlemoffcau  7730  peano5nnnn  7824  mulap0r  8504  nn1suc  8867  prime  9281  zindd  9300  xrlttri3  9724  xnn0xadd0  9794  fzopth  9986  fzsuc  9994  fzpred  9995  fzp1ss  9998  fztp  10003  fseq1p1m1  10019  1fv  10064  elfzom1elp1fzo  10127  ssfzo12  10149  fzosplitsn  10158  divfl0  10221  modqid  10274  modqmuladdim  10292  frecuzrdgtcl  10337  frecuzrdgfunlem  10344  frecfzennn  10351  frecfzen2  10352  seq3val  10383  seqvalcd  10384  iseqf1olemqcl  10411  iseqf1olemnab  10413  iseqf1olemmo  10417  iseqf1olemqk  10419  seq3f1olemstep  10426  seq3id3  10432  faclbnd  10643  faclbnd3  10645  bcm1k  10662  hashfz1  10685  focdmex  10689  hashfz  10723  hashfzp1  10726  hashfacen  10735  leisorel  10736  cjcj  10811  caucvgre  10909  r19.2uz  10921  resqrexlemgt0  10948  ltabs  11015  xrmaxiflemab  11174  xrmaxiflemlub  11175  nnf1o  11303  summodclem2a  11308  fsumf1o  11317  fisum0diag2  11374  modfsummodlemstep  11384  fsumparts  11397  clim2prod  11466  prodfap0  11472  prodmodclem2a  11503  fprodssdc  11517  fprodcllem  11533  ef0lem  11587  resinval  11642  recosval  11643  demoivreALT  11700  nn0o  11829  zsupcllemstep  11863  zsupcllemex  11864  infssuzledc  11868  gcdmultiplez  11939  dvdssq  11949  eucalg  11970  lcmgcdnn  11993  dvdsnprmd  12036  prm2orodd  12037  qnumdenbi  12101  nn0gcdsq  12109  phibnd  12126  hashdvds  12130  phimullem  12134  prmdiveq  12145  hashgcdlem  12147  modprm0  12163  nnnn0modprm0  12164  modprmn0modprm0  12165  oddprm  12168  prm23lt5  12172  pcprendvds  12199  pcidlem  12231  pcmpt  12250  pcfac  12257  unennn  12267  ennnfonelemk  12270  ennnfonelemjn  12272  ennnfonelemhf1o  12283  ennnfonelemex  12284  ennnfonelemf1  12288  ennnfonelemrn  12289  qnnen  12301  unbendc  12326  setsfun0  12367  srngbased  12454  srngplusgd  12455  srngmulrd  12456  srnginvld  12457  lmodbased  12465  lmodplusgd  12466  lmodscad  12467  lmodvscad  12468  ipsbased  12473  ipsaddgd  12474  ipsmulrd  12475  ipsscad  12476  ipsvscad  12477  ipsipd  12478  tgval  12590  cldval  12640  ntrfval  12641  clsfval  12642  neifval  12681  neif  12682  neival  12684  cnclima  12764  cncnpi  12769  cnrest2  12777  cnrest2r  12778  cnptoprest  12780  cnpdis  12783  txvalex  12795  txval  12796  txcnmpt  12814  txdis  12818  cnmpt1t  12826  cnmpt2t  12834  hmeocnv  12848  hmeontr  12854  txhmeo  12860  xmetunirn  12899  xmettpos  12911  metn0  12919  xmetres  12923  metres  12924  blrnps  12952  blrn  12953  blin2  12973  blbas  12974  xmeterval  12976  xmettxlem  13050  xmettx  13051  metcnpi  13056  reldvg  13189  dvaddxx  13208  dvmulxx  13209  dviaddf  13210  dvimulf  13211  dvfre  13215  dveflem  13228  sinq12gt0  13292  rprelogbdiv  13416  logbgcd1irr  13426  bj-inex  13624  bj-sucexg  13639  bj-peano4  13672  setindis  13684  bdsetindis  13686  bj-inf2vnlem1  13687  exmid1stab  13714  nnsf  13719  nninfall  13723  nninfsellemeq  13728  sbthom  13739