Theorem 3syl 17

Description: Inference chaining two syllogisms. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
3syl.1	|- ( ph -> ps )
3syl.2	|- ( ps -> ch )
3syl.3	|- ( ch -> th )

Assertion

Ref	Expression
3syl	|- ( ph -> th )

Proof of Theorem 3syl

Step	Hyp	Ref	Expression
1		3syl.1	. . 3 |- ( ph -> ps )
2		3syl.2	. . 3 |- ( ps -> ch )
3	1, 2	syl 14	. 2 |- ( ph -> ch )
4		3syl.3	. 2 |- ( ch -> th )
5	3, 4	syl 14	1 |- ( ph -> th )

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  1559  nfal  1590  19.9hd  1676  equsexd  1743  sbcof2  1824  aev  1826  sbequi  1853  nfsbd  1996  mo2n  2073  eupickb  2126  r19.29af2  2637  spc2gv  2855  spc3gv  2857  eqvincg  2888  sbcco3g  3142  ssrmof  3246  exmidsssnc  4236  exmid1stab  4241  snelpwi  4245  opth1  4269  frind  4387  onin  4421  abnexg  4481  reusv1  4493  xpexg  4777  dmexg  4930  rnexg  4931  elrelimasn  5035  relfld  5198  funimaexglem  5341  funimaexg  5342  fabexg  5445  fsnd  5547  elfvm  5591  nfvres  5592  funimass4  5611  elfvmptrab1  5656  funconstss  5680  f1oresrab  5727  resfunexg  5783  f1eqcocnv  5838  isores1  5861  isoini  5865  isose  5868  isopolem  5869  isosolem  5871  eusvobj2  5908  acexmidlemcase  5917  oprabid  5954  offval  6143  resfunexgALT  6165  offval3  6191  1stvalg  6200  2ndvalg  6201  1stcof  6221  2ndcof  6222  cnvf1o  6283  tposf12  6327  smores3  6351  smoiso  6360  tfr0dm  6380  tfrlemibxssdm  6385  tfrlemi14d  6391  tfrexlem  6392  tfr1onlemssrecs  6397  tfr1onlemsucfn  6398  tfr1onlemsucaccv  6399  tfr1onlembxssdm  6401  tfr1onlemres  6407  tfri1dALT  6409  tfrcllemssrecs  6410  tfrcllemsucfn  6411  tfrcllemsucaccv  6412  tfrcllembxssdm  6414  tfrcllemres  6420  rdgss  6441  nnsucsssuc  6550  nntr2  6561  swoord1  6621  swoord2  6622  iinerm  6666  eroveu  6685  pmresg  6735  en1uniel  6863  pw2f1odclem  6895  fopwdom  6897  xpen  6906  ssenen  6912  isinfinf  6958  ac6sfi  6959  preimaf1ofi  7017  sbthlem1  7023  fi0  7041  fiss  7043  supubti  7065  suplubti  7066  isotilem  7072  supisolem  7074  supisoex  7075  supisoti  7076  ordiso2  7101  eldju1st  7137  eldju2ndl  7138  updjud  7148  djudom  7159  ctmlemr  7174  enumctlemm  7180  nnnninfeq  7194  ctssexmid  7216  nninfwlpoimlemginf  7242  exmidonfinlem  7260  en2other2  7263  exmidaclem  7275  cc2lem  7333  cc3  7335  addclnq  7442  mulclnq  7443  1qec  7455  prarloclemarch2  7486  enq0tr  7501  addclnq0  7518  mulclnq0  7519  nq0m0r  7523  prarloclemlo  7561  prarloc  7570  genpml  7584  genpmu  7585  addnqprl  7596  addnqpru  7597  recnnpr  7615  prmuloc2  7634  1idpru  7658  ltexprlemm  7667  ltexprlemloc  7674  recexprlemm  7691  recexprlem1ssl  7700  caucvgprlemnkj  7733  caucvgprlemnbj  7734  caucvgprlemm  7735  caucvgprlemopl  7736  caucvgprlemlol  7737  caucvgprlemladdfu  7744  caucvgprlemladdrl  7745  caucvgprprlemk  7750  caucvgprprlemloccalc  7751  caucvgprprlemnkltj  7756  caucvgprprlemnjltk  7758  caucvgprprlemml  7761  caucvgprprlemmu  7762  caucvgprprlemlol  7765  caucvgprprlemexb  7774  caucvgprprlem1  7776  suplocexprlemml  7783  suplocexprlemlub  7791  addclsr  7820  mulclsr  7821  prsrcl  7851  caucvgsrlemoffcau  7865  peano5nnnn  7959  mulap0r  8642  nn1suc  9009  prime  9425  zindd  9444  xrlttri3  9872  xnn0xadd0  9942  fzopth  10136  fzsuc  10144  fzpred  10145  fzp1ss  10148  fztp  10153  fseq1p1m1  10169  1fv  10214  elfzom1elp1fzo  10278  ssfzo12  10300  fzosplitsn  10309  zsupcllemstep  10319  zsupcllemex  10320  infssuzledc  10324  divfl0  10386  fldiv4lem1div2uz2  10396  modqid  10441  modqmuladdim  10459  frecuzrdgtcl  10504  frecuzrdgfunlem  10511  frecfzennn  10518  frecfzen2  10519  seq3val  10552  seqvalcd  10553  seqsplitg  10581  iseqf1olemqcl  10591  iseqf1olemnab  10593  iseqf1olemmo  10597  iseqf1olemqk  10599  seq3f1olemstep  10606  seqf1oglem2  10612  seq3id3  10616  seqhomog  10622  faclbnd  10833  faclbnd3  10835  bcm1k  10852  hashfz1  10875  hashfz  10913  hashfzp1  10916  fiubm  10920  hashfacen  10928  leisorel  10929  wrdexb  10947  wrdsymb  10962  wrdred1hash  10978  cjcj  11048  caucvgre  11146  r19.2uz  11158  resqrexlemgt0  11185  ltabs  11252  xrmaxiflemab  11412  xrmaxiflemlub  11413  nnf1o  11541  summodclem2a  11546  fsumf1o  11555  fisum0diag2  11612  modfsummodlemstep  11622  fsumparts  11635  clim2prod  11704  prodfap0  11710  prodmodclem2a  11741  fprodssdc  11755  fprodcllem  11771  ef0lem  11825  resinval  11880  recosval  11881  demoivreALT  11939  nn0o  12072  gcdmultiplez  12188  dvdssq  12198  nninfct  12208  eucalg  12227  lcmgcdnn  12250  dvdsnprmd  12293  prm2orodd  12294  isprm5lem  12309  qnumdenbi  12360  nn0gcdsq  12368  phibnd  12385  hashdvds  12389  phimullem  12393  prmdiveq  12404  hashgcdlem  12406  modprm0  12423  nnnn0modprm0  12424  modprmn0modprm0  12425  oddprm  12428  prm23lt5  12432  pcprendvds  12459  pcidlem  12492  pcmpt  12512  pcfac  12519  infpnlem2  12529  prmunb  12531  1arith  12536  4sqlem19  12578  unennn  12614  ennnfonelemk  12617  ennnfonelemjn  12619  ennnfonelemhf1o  12630  ennnfonelemex  12631  ennnfonelemf1  12635  ennnfonelemrn  12636  qnnen  12648  unbendc  12671  setsfun0  12714  srngbased  12824  srngplusgd  12825  srngmulrd  12826  srnginvld  12827  lmodbased  12842  lmodplusgd  12843  lmodscad  12844  lmodvscad  12845  ipsbased  12854  ipsaddgd  12855  ipsmulrd  12856  ipsscad  12857  ipsvscad  12858  ipsipd  12859  tgval  12933  isnsgrp  13049  ismnd  13060  dfgrp2e  13160  subgintm  13328  eqg0el  13359  ecqusaddcl  13369  kerf1ghm  13404  gsumfzconst  13471  imasrng  13512  srgisid  13542  srg1zr  13543  qusring2  13622  oppr1g  13638  dvdsr02  13661  isunitd  13662  crngunit  13667  unitpropdg  13704  elrhmunit  13733  subrngintm  13768  subrguss  13792  subrgunit  13795  subrgugrp  13796  subrgintm  13799  lmodfopnelem1  13880  rmodislmodlem  13906  rmodislmod  13907  lssuni  13919  islss3  13935  lss0v  13986  sraval  13993  rnglidlmmgm  14052  2idllidld  14062  2idlridld  14063  rng2idl0  14075  rng2idlsubg0  14078  zrh0  14181  znle  14193  zndvds0  14206  znf1o  14207  znleval  14209  znfi  14211  znhash  14212  znunit  14215  psrbasg  14227  psradd  14231  cldval  14335  ntrfval  14336  clsfval  14337  neifval  14376  neif  14377  neival  14379  cnclima  14459  cncnpi  14464  cnrest2  14472  cnrest2r  14473  cnptoprest  14475  cnpdis  14478  txvalex  14490  txval  14491  txcnmpt  14509  txdis  14513  cnmpt1t  14521  cnmpt2t  14529  hmeocnv  14543  hmeontr  14549  txhmeo  14555  xmetunirn  14594  xmettpos  14606  metn0  14614  xmetres  14618  metres  14619  blrnps  14647  blrn  14648  blin2  14668  blbas  14669  xmeterval  14671  xmettxlem  14745  xmettx  14746  metcnpi  14751  reldvg  14915  dvaddxx  14939  dvmulxx  14940  dviaddf  14941  dvimulf  14942  dvfre  14946  dvmptid  14952  dveflem  14962  elply2  14971  plyreres  15000  sinq12gt0  15066  rprelogbdiv  15193  logbgcd1irr  15203  fsumdvdsmul  15227  lgslem4  15244  lgsdirprm  15275  gausslemma2dlem0a  15290  gausslemma2dlem0f  15295  gausslemma2dlem0i  15298  gausslemma2dlem1a  15299  gausslemma2dlem1cl  15300  gausslemma2dlem5  15307  gausslemma2dlem6  15308  gausslemma2d  15310  lgseisenlem1  15311  lgseisenlem2  15312  lgseisenlem3  15313  lgseisen  15315  lgsquadlem1  15318  m1lgs  15326  2lgslem1a  15329  2lgslem1c  15331  2lgsoddprmlem2  15347  bj-inex  15553  bj-sucexg  15568  bj-peano4  15601  setindis  15613  bdsetindis  15615  bj-inf2vnlem1  15616  nnsf  15649  nninfall  15653  nninfsellemeq  15658  sbthom  15670