Theorem sylancl 413

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 411	1 |- ( ph -> th )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  sylanblc  415  sylanblrc  416  equveli  1808  sseqtrid  3288  ssdifin0  3591  uneqdifeqim  3595  unimax  3948  opth  4353  djussxp  4900  iss  5084  relresfld  5292  eldmrexrn  5818  f1oresrab  5842  fmptco  5843  fsn  5849  fnressn  5870  foima2  5924  foeqcnvco  5963  isoini2  5992  relmptopab  6256  ofres  6281  ofco  6285  suppval1  6439  suppimacnvfn  6446  tposexg  6489  tfrlemisucaccv  6556  tfrlemibex  6560  tfri1dALT  6582  tfrcl  6595  rdgivallem  6612  frecabex  6629  frectfr  6631  frecrdg  6639  pmresg  6910  mapsnd  6923  mapsn  6925  mapsncnv  6930  ixpsnf1o  6971  en1  7039  2dom  7046  mapsnend  7052  enpr2d  7064  en2  7065  mapxpen  7101  mapunen  7104  phplem4  7109  exmidpw2en  7172  fiintim  7191  sbthlem2  7228  elfir  7260  2omap  7269  infglbti  7316  caseinl  7382  caseinr  7383  difinfsnlem  7390  difinfsn  7391  nninfisollemne  7422  exmidfodomrlemim  7504  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  2omotaplemap  7571  archnqq  7732  prarloclemlt  7808  prarloclemlo  7809  prarloclemcalc  7817  recexprlemm  7939  recexprlemex  7952  caucvgprlemm  7983  caucvgprprlemmu  8010  suplocexprlem2b  8029  suplocexprlemmu  8033  suplocexprlemlub  8039  1idsr  8083  recexgt0sr  8088  archsr  8097  caucvgsrlemoffval  8111  caucvgsrlemofff  8112  caucvgsrlemoffres  8115  caucvgsr  8117  ltpsrprg  8118  suplocsrlem  8123  pitonnlem2  8162  pitonn  8163  pitoregt0  8164  pitore  8165  recnnre  8166  axrnegex  8194  nntopi  8209  msqge0  8890  mulge0  8893  recexaplem2  8926  recexap  8927  recgt0  9124  recreclt  9174  nn1m1nn  9255  nn1suc  9256  nnle1eq1  9261  nn1gt1  9271  nnsub  9276  addltmul  9475  nn0le0eq0  9524  elnn0nn  9538  elnnz  9587  elznn0  9592  zlem1lt  9634  zltlem1  9635  elz2  9649  nn0n0n1ge2b  9657  nn0lt2  9659  nn0le2is012  9660  eluzaddi  9881  eluzsubi  9882  uzp1  9888  peano2uzr  9917  nn01to3  9949  qreccl  9974  irrmulap  9980  ltpnf  10113  xaddass2  10203  iccen  10340  fz01en  10387  fzpreddisj  10405  fzsuc2  10413  fseq1p1m1  10428  fseq1m1p1  10429  elfzp1b  10431  fzoss2  10508  fzval3  10549  fzosplitsnm1  10554  fzosplitprm1  10580  flhalf  10662  fldiv4lem1div2uz2  10666  modqmulnn  10704  modqmuladdnn0  10730  frec2uzrand  10767  frecuzrdg0  10775  frecuzrdg0t  10784  frecfzennn  10788  frecfzen2  10789  uzennn  10798  seqeq1  10812  seqp1g  10828  seqclg  10834  seq3m1  10835  monoord2  10848  ser3mono  10849  seqf1oglem1  10881  seqf1oglem2  10882  seqfeq4g  10893  ser0f  10896  exp3vallem  10902  expm1t  10929  expeq0  10932  expubnd  10958  binom3  11019  facndiv  11101  facavg  11108  bcn0  11117  bcnp1n  11121  bcm1k  11122  bcp1nk  11124  bcval5  11125  bcn2  11126  bcp1m1  11127  bcpasc  11128  bcn2m1  11132  hashsng  11161  hashun  11169  hashfz  11186  hashfzo  11187  hashmap  11192  hashfibclem  11206  seq3coll  11214  hash2en  11215  iswrdiz  11231  snopiswrd  11234  ccat1st1st  11329  swrds1  11360  cats1un  11413  wrdind  11414  wrd2ind  11415  swrdccatin1  11417  swrdccat3blem  11431  shftfval  11506  2shfti  11516  resqrexlemf1  11693  abs00ap  11747  sqabs  11767  ltabs  11772  caubnd2  11802  max0addsup  11904  rexico  11906  mulcn2  11997  climaddc1  12014  climmulc2  12016  climsubc1  12017  climsubc2  12018  iserex  12024  climlec2  12026  iser3shft  12031  climcvg1nlem  12034  serf0  12037  sumrbdc  12065  fsumm1  12102  fsump1  12106  fsum00  12148  telfsumo  12152  fsumparts  12156  hashiun  12164  binomlem  12169  binom1dif  12173  bcxmas  12175  isumsplit  12177  isum1p  12178  arisum  12184  arisum2  12185  trireciplem  12186  explecnv  12191  geolim  12197  georeclim  12199  mertenslem2  12222  mertensabs  12223  prodf1f  12229  prodrbdclem2  12259  efcllemp  12344  ef0lem  12346  efgt0  12370  eftlub  12376  efsep  12377  effsumlt  12378  tanval3ap  12400  efi4p  12403  resin4p  12404  recos4p  12405  ef01bndlem  12442  sin01bnd  12443  cos01bnd  12444  sinltxirr  12447  sin01gt0  12448  cos01gt0  12449  absefib  12457  efieq1re  12458  eirraplem  12463  dvdsdc  12484  dvdscmulr  12506  fsumdvds  12528  dvdslelemd  12529  3dvds  12550  odd2np1lem  12558  odd2np1  12559  flodddiv4  12622  bitsfzo  12641  bitsmod  12642  gcdsupex  12653  gcdsupcl  12654  gcd1  12683  nninfctlemfo  12736  nn0seqcvgd  12738  algcvg  12745  algcvgblem  12746  eucalg  12756  prmind2  12817  qden1elz  12902  dfphi2  12917  phiprm  12920  phimullem  12922  prmdiv  12932  prmdiveq  12933  prm23lt5  12961  pcpre1  12990  pczpre  12995  pcdiv  13000  pc1  13003  pcqdiv  13005  pcexp  13007  pcxnn0cl  13008  pcxcl  13009  pcdvdstr  13025  pc2dvds  13028  sumhashdc  13045  fldivp1  13046  pcfaclem  13047  qexpz  13050  expnprm  13051  prmpwdvds  13053  pockthlem  13054  4sqlem5  13080  4sqlem6  13081  4sqlem11  13099  4sqlem13m  13101  4sqlem19  13107  ballotfilemofi  13138  oddennn  13143  xpct  13147  ennnfonelemj0  13152  ennnfonelemen  13172  ctinfomlemom  13178  omctfn  13194  restid  13463  prdsex  13482  prdsval  13486  prdsbaslemss  13487  prdsbas  13489  imasbas  13520  imasplusg  13521  imasmulr  13522  imasaddfnlemg  13527  xpscf  13560  igsumvalx  13602  gsumsplit1r  13611  gsumprval  13612  gsumfzz  13708  gsumfzcl  13712  prdsgrpd  13822  prdsinvgd  13823  mulgnngsum  13844  mulgnndir  13868  mulgneg2  13873  dvdsrmuld  14241  zsssubrg  14733  znval  14784  znle  14785  znbaslemnn  14787  znf1o  14799  znleval  14801  psrval  14814  restuni2  15042  cnrest2r  15102  lmfss  15109  lmres  15113  lmtopcnp  15115  ispsmet  15188  isxmet2d  15213  ismet2  15219  blfvalps  15250  blex  15252  xblss2  15270  reopnap  15411  divcnap  15430  climcncf  15449  cncfmpt2fcntop  15464  hovera  15512  limcdifap  15527  cnplimcim  15532  cnlimcim  15536  cnlimc  15537  cnlimci  15538  dvbss  15550  dvcnp2cntop  15564  dvcn  15565  dvaddxxbr  15566  dvmulxxbr  15567  dvexp  15576  dveflem  15591  plyval  15597  elply2  15600  plyf  15602  plyss  15603  plyssc  15604  elplyr  15605  plyaddlem1  15612  plymullem1  15613  plyaddlem  15614  plymullem  15615  plyco  15624  plycj  15626  dvply1  15630  reeff1olem  15636  sinperlem  15673  sin2kpi  15676  cos2kpi  15677  sin2pim  15678  cos2pim  15679  cosq14gt0  15697  coseq0q4123  15699  tangtx  15703  abssinper  15711  sinkpi  15712  coskpi  15713  cosq34lt1  15715  logrpap0b  15741  logdivlti  15746  rpcxpsqrtth  15795  rpabscxpbnd  15805  binom4  15844  wilthlem1  15848  0sgm  15853  1sgmprm  15862  1sgm2ppw  15863  mersenne  15865  perfect1  15866  perfectlem1  15867  perfectlem2  15868  perfect  15869  lgslem1  15873  lgsval  15877  lgsfvalg  15878  lgsfcl2  15879  lgsfcl  15881  lgsval2lem  15883  lgsvalmod  15892  lgsneg  15897  lgsdilem  15900  lgsdir2lem3  15903  lgsdir  15908  lgsdilem2  15909  lgsdi  15910  lgsne0  15911  lgsabs1  15912  lgsprme0  15915  lgsdirnn0  15920  lgsdinn0  15921  gausslemma2dlem0d  15925  gausslemma2dlem1a  15931  gausslemma2dlem1f1o  15933  gausslemma2dlem3  15936  gausslemma2dlem4  15937  gausslemma2dlem5a  15938  gausslemma2dlem5  15939  gausslemma2dlem6  15940  lgseisenlem2  15944  lgseisen  15947  lgsquadlem1  15950  lgsquadlem2  15951  lgsquad2lem1  15954  lgsquad2lem2  15955  lgsquad2  15956  m1lgs  15958  2lgslem1  15964  2lgslem2  15965  2lgs  15977  2sqlem9  15997  2sqlem10  15998  ushgredgedg  16221  ushgredgedgloop  16223  uhgrspansubgrlem  16271  wlkvtxiedg  16340  wlkvtxiedgg  16341  wlk1walkdom  16354  upgr2wlkdc  16372  clwwlkccatlem  16395  umgrclwwlkge2  16397  clwwlknonmpo  16423  clwwlknonex2lem2  16433  clwwlknonex2  16434  konigsberglem1  16483  pwle2  16772  pw1nct  16777  nninfsellemdc  16788  nnnninfen  16799  nnnninfex  16800  nninfnfiinf  16801  sbthom  16806  repiecelem  16809  repiecele0  16810  trirec0  16828  apdifflemr  16831  reap0  16843  trimul0or  16845  nconstwlpolem  16851  gfsumval  16862