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  383  hbim  1524  19.9hd  1640  equsexd  1707  sbcof2  1782  aev  1784  sbequi  1811  nfsbd  1950  mo2n  2027  eupickb  2080  r19.29af2  2572  spc2gv  2776  spc3gv  2778  eqvincg  2809  sbcco3g  3057  ssrmof  3160  exmidsssnc  4126  snelpwi  4134  opth1  4158  frind  4274  onin  4308  abnexg  4367  reusv1  4379  xpexg  4653  dmexg  4803  rnexg  4804  relfld  5067  funimaexglem  5206  funimaexg  5207  fabexg  5310  fsnd  5410  nfvres  5454  funimass4  5472  elfvmptrab1  5515  funconstss  5538  f1oresrab  5585  resfunexg  5641  f1eqcocnv  5692  isores1  5715  isoini  5719  isose  5722  isopolem  5723  isosolem  5725  eusvobj2  5760  acexmidlemcase  5769  oprabid  5803  offval  5989  resfunexgALT  6008  offval3  6032  1stvalg  6040  2ndvalg  6041  1stcof  6061  2ndcof  6062  cnvf1o  6122  tposf12  6166  smores3  6190  smoiso  6199  tfr0dm  6219  tfrlemibxssdm  6224  tfrlemi14d  6230  tfrexlem  6231  tfr1onlemssrecs  6236  tfr1onlemsucfn  6237  tfr1onlemsucaccv  6238  tfr1onlembxssdm  6240  tfr1onlemres  6246  tfri1dALT  6248  tfrcllemssrecs  6249  tfrcllemsucfn  6250  tfrcllemsucaccv  6251  tfrcllembxssdm  6253  tfrcllemres  6259  rdgss  6280  nnsucsssuc  6388  nntr2  6399  swoord1  6458  swoord2  6459  iinerm  6501  eroveu  6520  pmresg  6570  en1uniel  6698  fopwdom  6730  xpen  6739  ssenen  6745  isinfinf  6791  ac6sfi  6792  preimaf1ofi  6839  sbthlem1  6845  fi0  6863  fiss  6865  supubti  6886  suplubti  6887  isotilem  6893  supisolem  6895  supisoex  6896  supisoti  6897  ordiso2  6920  eldju1st  6956  eldju2ndl  6957  updjud  6967  djudom  6978  ctmlemr  6993  enumctlemm  6999  ctssexmid  7024  exmidonfinlem  7049  en2other2  7052  exmidaclem  7064  addclnq  7183  mulclnq  7184  1qec  7196  prarloclemarch2  7227  enq0tr  7242  addclnq0  7259  mulclnq0  7260  nq0m0r  7264  prarloclemlo  7302  prarloc  7311  genpml  7325  genpmu  7326  addnqprl  7337  addnqpru  7338  recnnpr  7356  prmuloc2  7375  1idpru  7399  ltexprlemm  7408  ltexprlemloc  7415  recexprlemm  7432  recexprlem1ssl  7441  caucvgprlemnkj  7474  caucvgprlemnbj  7475  caucvgprlemm  7476  caucvgprlemopl  7477  caucvgprlemlol  7478  caucvgprlemladdfu  7485  caucvgprlemladdrl  7486  caucvgprprlemk  7491  caucvgprprlemloccalc  7492  caucvgprprlemnkltj  7497  caucvgprprlemnjltk  7499  caucvgprprlemml  7502  caucvgprprlemmu  7503  caucvgprprlemlol  7506  caucvgprprlemexb  7515  caucvgprprlem1  7517  suplocexprlemml  7524  suplocexprlemlub  7532  addclsr  7561  mulclsr  7562  prsrcl  7592  caucvgsrlemoffcau  7606  peano5nnnn  7700  mulap0r  8377  nn1suc  8739  prime  9150  zindd  9169  xrlttri3  9583  xnn0xadd0  9650  fzopth  9841  fzsuc  9849  fzpred  9850  fzp1ss  9853  fztp  9858  fseq1p1m1  9874  1fv  9916  elfzom1elp1fzo  9979  ssfzo12  10001  fzosplitsn  10010  divfl0  10069  modqid  10122  modqmuladdim  10140  frecuzrdgtcl  10185  frecuzrdgfunlem  10192  frecfzennn  10199  frecfzen2  10200  seq3val  10231  seqvalcd  10232  iseqf1olemqcl  10259  iseqf1olemnab  10261  iseqf1olemmo  10265  iseqf1olemqk  10267  seq3f1olemstep  10274  seq3id3  10280  faclbnd  10487  faclbnd3  10489  bcm1k  10506  hashfz1  10529  focdmex  10533  hashfz  10567  hashfzp1  10570  hashfacen  10579  leisorel  10580  cjcj  10655  caucvgre  10753  r19.2uz  10765  resqrexlemgt0  10792  ltabs  10859  xrmaxiflemab  11016  xrmaxiflemlub  11017  nnf1o  11145  summodclem2a  11150  fsumf1o  11159  fisum0diag2  11216  modfsummodlemstep  11226  fsumparts  11239  clim2prod  11308  prodfap0  11314  prodmodclem2a  11345  ef0lem  11366  resinval  11422  recosval  11423  demoivreALT  11480  nn0o  11604  zsupcllemstep  11638  zsupcllemex  11639  infssuzledc  11643  gcdmultiplez  11709  dvdssq  11719  eucalg  11740  lcmgcdnn  11763  dvdsnprmd  11806  prm2orodd  11807  qnumdenbi  11870  nn0gcdsq  11878  phibnd  11893  hashdvds  11897  phimullem  11901  hashgcdlem  11903  unennn  11910  ennnfonelemk  11913  ennnfonelemjn  11915  ennnfonelemhf1o  11926  ennnfonelemex  11927  ennnfonelemf1  11931  ennnfonelemrn  11932  qnnen  11944  setsfun0  11995  srngbased  12082  srngplusgd  12083  srngmulrd  12084  srnginvld  12085  lmodbased  12093  lmodplusgd  12094  lmodscad  12095  lmodvscad  12096  ipsbased  12101  ipsaddgd  12102  ipsmulrd  12103  ipsscad  12104  ipsvscad  12105  ipsipd  12106  tgval  12218  cldval  12268  ntrfval  12269  clsfval  12270  neifval  12309  neif  12310  neival  12312  cnclima  12392  cncnpi  12397  cnrest2  12405  cnrest2r  12406  cnptoprest  12408  cnpdis  12411  txvalex  12423  txval  12424  txcnmpt  12442  txdis  12446  cnmpt1t  12454  cnmpt2t  12462  hmeocnv  12476  hmeontr  12482  txhmeo  12488  xmetunirn  12527  xmettpos  12539  metn0  12547  xmetres  12551  metres  12552  blrnps  12580  blrn  12581  blin2  12601  blbas  12602  xmeterval  12604  xmettxlem  12678  xmettx  12679  metcnpi  12684  reldvg  12817  dvaddxx  12836  dvmulxx  12837  dviaddf  12838  dvimulf  12839  dvfre  12843  dveflem  12855  sinq12gt0  12911  bj-inex  13105  bj-sucexg  13120  bj-peano4  13153  setindis  13165  bdsetindis  13167  bj-inf2vnlem1  13168  exmid1stab  13195  nnsf  13199  nninfalllemn  13202  nninfall  13204  nninfsellemeq  13210  sbthom  13221