Theorem sylancl 417

Description: Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)

Hypotheses

Ref	Expression
sylancl.1	|- ( ph -> ps )
sylancl.2	|- ch
sylancl.3	|- ( ( ps /\ ch ) -> th )

Assertion

Ref	Expression
sylancl	|- ( ph -> th )

Proof of Theorem sylancl

Step	Hyp	Ref	Expression
1		sylancl.1	. 2 |- ( ph -> ps )
2		sylancl.2	. . 3 |- ch
3	2	a1i 9	. 2 |- ( ph -> ch )
4		sylancl.3	. 2 |- ( ( ps /\ ch ) -> th )
5	1, 3, 4	syl2anc 415	1 |- ( ph -> th )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used by:  sylanblc  419  sylanblrc  420  equveli  1812  sseqtrid  3298  ssdifin0  3609  uneqdifeqim  3613  unimax  3969  opth  4379  djussxp  4927  iss  5112  relresfld  5320  eldmrexrn  5852  f1oresrab  5876  fmptco  5877  fsn  5883  fnressn  5904  foima2  5960  foeqcnvco  5999  isoini2  6028  relmptopab  6294  ofres  6321  ofco  6325  suppval1  6483  suppimacnvfn  6490  tposexg  6533  tfrlemisucaccv  6600  tfrlemibex  6604  tfri1dALT  6626  tfrcl  6639  rdgivallem  6656  frecabex  6673  frectfr  6675  frecrdg  6683  pmresg  6961  mapsnd  6974  mapsn  6976  mapsncnv  6981  ixpsnf1o  7022  en1  7090  2dom  7097  mapsnend  7103  enpr2d  7115  en2  7116  mapxpen  7152  mapunen  7155  phplem4  7160  exmidpw2en  7223  fiintim  7242  sbthlem2  7280  elfir  7312  2omap  7324  infglbti  7371  caseinl  7437  caseinr  7438  difinfsnlem  7445  difinfsn  7446  nninfisollemne  7477  exmidfodomrlemim  7559  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  2omotaplemap  7629  archnqq  7790  prarloclemlt  7866  prarloclemlo  7867  prarloclemcalc  7875  recexprlemm  7997  recexprlemex  8010  caucvgprlemm  8041  caucvgprprlemmu  8068  suplocexprlem2b  8087  suplocexprlemmu  8091  suplocexprlemlub  8097  1idsr  8141  recexgt0sr  8146  archsr  8155  caucvgsrlemoffval  8169  caucvgsrlemofff  8170  caucvgsrlemoffres  8173  caucvgsr  8175  ltpsrprg  8176  suplocsrlem  8181  pitonnlem2  8220  pitonn  8221  pitoregt0  8222  pitore  8223  recnnre  8224  axrnegex  8252  nntopi  8267  msqge0  8952  mulge0  8955  recexaplem2  8988  recexap  8989  recgt0  9188  recreclt  9238  ofsubeq0  9300  nn1m1nn  9331  nn1suc  9332  nnle1eq1  9337  nn1gt1  9347  nnsub  9352  addltmul  9553  nn0le0eq0  9602  elnn0nn  9616  elnnz  9665  elznn0  9670  zlem1lt  9712  zltlem1  9713  elz2  9727  nn0n0n1ge2b  9736  nn0lt2  9738  nn0le2is012  9739  eluzaddi  9965  eluzsubi  9966  uzp1  9972  peano2uzr  10001  nn01to3  10033  qreccl  10058  irrmulap  10065  ltpnf  10199  xaddass2  10289  iccen  10426  fz01en  10476  fzpreddisj  10495  fzsuc2  10503  fseq1p1m1  10518  fseq1m1p1  10519  elfzp1b  10521  fzoss2  10598  fzval3  10639  fzosplitsnm1  10644  fzosplitprm1  10670  flhalf  10758  fldiv4lem1div2uz2  10762  modqmulnn  10800  modqmuladdnn0  10826  frec2uzrand  10863  frecuzrdg0  10871  frecuzrdg0t  10880  frecfzennn  10884  frecfzen2  10885  uzennn  10894  seqeq1  10908  seqp1g  10924  seqclg  10930  seq3m1  10931  monoord2  10944  ser3mono  10945  seqf1oglem1  10977  seqf1oglem2  10978  seqfeq4g  10989  ser0f  10992  exp3vallem  10998  expm1t  11025  expeq0  11028  expubnd  11054  binom3  11115  facndiv  11199  facavg  11206  bcn0  11215  bcnp1n  11219  bcm1k  11220  bcp1nk  11222  bcval5  11223  bcn2  11224  bcp1m1  11225  bcpasc  11226  bcn2m1  11230  hashsng  11259  hashun  11267  hashfz  11284  hashfzo  11285  hashmap  11290  hashfibclem  11304  hashf1lem1  11307  hashf1  11309  seq3coll  11316  hash2en  11317  iswrdiz  11333  snopiswrd  11336  ccat1st1st  11431  swrds1  11462  cats1un  11515  wrdind  11516  wrd2ind  11517  swrdccatin1  11519  swrdccat3blem  11533  shftfval  11608  2shfti  11618  resqrexlemf1  11796  abs00ap  11850  sqabs  11871  ltabs  11876  caubnd2  11906  max0addsup  12008  rexico  12010  mulcn2  12103  climaddc1  12120  climmulc2  12122  climsubc1  12123  climsubc2  12124  iserex  12130  climlec2  12132  iser3shft  12137  climcvg1nlem  12140  serf0  12143  sumrbdc  12171  fsumm1  12208  fsump1  12212  fsum00  12254  telfsumo  12258  fsumparts  12262  hashiun  12270  binomlem  12275  binom1dif  12279  bcxmas  12281  isumsplit  12283  isum1p  12284  arisum  12290  arisum2  12291  trireciplem  12292  explecnv  12297  geolim  12303  georeclim  12305  mertenslem2  12328  mertensabs  12329  prodf1f  12335  prodrbdclem2  12365  efcllemp  12450  ef0lem  12452  efgt0  12476  eftlub  12482  efsep  12483  effsumlt  12484  tanval3ap  12506  efi4p  12509  resin4p  12510  recos4p  12511  ef01bndlem  12548  sin01bnd  12549  cos01bnd  12550  sinltxirr  12553  sin01gt0  12554  cos01gt0  12555  absefib  12563  efieq1re  12564  eirraplem  12569  dvdsdc  12590  dvdscmulr  12612  fsumdvds  12634  dvdslelemd  12635  3dvds  12656  odd2np1lem  12664  odd2np1  12665  flodddiv4  12728  bitsfzo  12747  bitsmod  12748  gcdsupex  12759  gcdsupcl  12760  gcd1  12789  nninfctlemfo  12842  nn0seqcvgd  12844  algcvg  12851  algcvgblem  12852  eucalg  12862  prmind2  12923  qden1elz  13010  dfphi2  13027  phiprm  13030  phimullem  13032  prmdiv  13042  prmdiveq  13043  prm23lt5  13071  pcpre1  13100  pczpre  13105  pcdiv  13110  pc1  13113  pcqdiv  13115  pcexp  13117  pcxnn0cl  13118  pcxcl  13119  pcdvdstr  13135  pc2dvds  13138  sumhashdc  13155  fldivp1  13156  pcfaclem  13157  qexpz  13160  expnprm  13161  prmpwdvds  13163  pockthlem  13164  4sqlem5  13190  4sqlem6  13191  4sqlem11  13209  4sqlem13m  13211  4sqlem19  13217  prmlem1a  13250  ballotfilemofi  13277  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilemodife  13298  ballotfilemscl  13305  ballotfilemsle  13306  oddennn  13341  xpct  13345  ennnfonelemj0  13350  ennnfonelemen  13370  ctinfomlemom  13376  omctfn  13392  restid  13663  imasbas  13687  imasplusg  13688  imasmulr  13689  imasaddfnlemg  13694  xpscf  13727  gzsumvalx  13768  gzsumsplit1r  13774  gzsumcl  13863  mulgnngzsum  13989  mulgnndir  14013  mulgneg2  14018  cntrnsg  14176  gsumvalfi  14242  gsum2dfilem2  14272  prdsex  14279  prdsval  14280  prdsbaslemss  14281  prdsbas  14283  prdsgrpd  14304  prdsinvgd  14305  dvdsrmuld  14512  zsssubrg  15031  znval  15080  znle  15081  znbaslemnn  15083  znf1o  15095  znleval  15097  psrval  15159  psrlidmfi  15199  psrridmfi  15200  restuni2  15403  cnrest2r  15463  lmfss  15470  lmres  15474  lmtopcnp  15476  ispsmet  15549  isxmet2d  15574  ismet2  15580  blfvalps  15611  blex  15613  xblss2  15631  reopnap  15772  divcnap  15791  climcncf  15810  cncfmpt2fcntop  15825  hovera  15873  limcdifap  15888  cnplimcim  15893  cnlimcim  15897  cnlimc  15898  cnlimci  15899  dvbss  15911  dvcnp2cntop  15925  dvcn  15926  dvaddxxbr  15927  dvmulxxbr  15928  dvexp  15937  dveflem  15952  plyval  15958  elply2  15961  plyf  15963  plyss  15964  plyssc  15965  elplyr  15966  plyaddlem1  15973  plymullem1  15974  plyaddlem  15975  plymullem  15976  plyco  15985  plycj  15987  dvply1  15991  reeff1olem  15997  sinperlem  16035  sin2kpi  16038  cos2kpi  16039  sin2pim  16040  cos2pim  16041  cosq14gt0  16059  coseq0q4123  16061  tangtx  16065  abssinper  16073  sinkpi  16074  coskpi  16075  cosq34lt1  16078  logrpap0b  16106  logdivlti  16111  rpcxpsqrtth  16165  rpabscxpbnd  16175  binom4  16219  birthdaylem2  16226  birthdaylem3  16227  wilthlem1  16232  0sgm  16254  ppiprm  16259  ppinprm  16260  chtprm  16261  chtnprm  16262  chtdif  16264  ppiqp1le  16267  ppidif  16269  ppiqeq0  16280  ppiqltx  16281  prmorcht  16282  1sgmprm  16288  1sgm2ppw  16289  ppiublem2  16292  ppiqub  16293  chtublem  16295  chtqub  16296  mersenne  16297  perfect1  16298  perfectlem1  16299  perfectlem2  16300  perfect  16301  bcp1ctr  16306  bclbnd  16307  bposlem1  16311  bposlem2  16312  bposlem3  16313  bposlem4  16314  bposlem5  16315  bposlem6  16316  bposlem9  16319  bpos  16320  lgslem1  16324  lgsval  16328  lgsfvalg  16329  lgsfcl2  16330  lgsfcl  16332  lgsval2lem  16334  lgsvalmod  16343  lgsneg  16348  lgsdilem  16351  lgsdir2lem3  16354  lgsdir  16359  lgsdilem2  16360  lgsdi  16361  lgsne0  16362  lgsabs1  16363  lgsprme0  16366  lgsdirnn0  16371  lgsdinn0  16372  gausslemma2dlem0d  16376  gausslemma2dlem1a  16382  gausslemma2dlem1f1o  16384  gausslemma2dlem3  16387  gausslemma2dlem4  16388  gausslemma2dlem5a  16389  gausslemma2dlem5  16390  gausslemma2dlem6  16391  lgseisenlem2  16395  lgseisen  16398  lgsquadlem1  16401  lgsquadlem2  16402  lgsquad2lem1  16405  lgsquad2lem2  16406  lgsquad2  16407  m1lgs  16409  2lgslem1  16415  2lgslem2  16416  2lgs  16428  2sqlem9  16448  2sqlem10  16449  ushgredgedg  16672  ushgredgedgloop  16674  uhgrspansubgrlem  16722  wlkvtxiedg  16791  wlkvtxiedgg  16792  wlk1walkdom  16805  upgr2wlkdc  16823  clwwlkccatlem  16846  umgrclwwlkge2  16848  clwwlknonmpo  16874  clwwlknonex2lem2  16884  clwwlknonex2  16885  konigsberglem1  16934  pwle2  17233  pw1nct  17238  nninfsellemdc  17259  nnnninfen  17270  nnnninfex  17271  nninfnfiinf  17272  sbthom  17277  repiecelem  17280  repiecele0  17281  trirec0  17300  apdifflemr  17303  reap0  17315  nconstwlpolem  17322