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  1805  sseqtrid  3274  ssdifin0  3573  uneqdifeqim  3577  unimax  3922  opth  4323  djussxp  4867  iss  5051  relresfld  5258  eldmrexrn  5778  f1oresrab  5802  fmptco  5803  fsn  5809  fnressn  5829  foima2  5881  foeqcnvco  5920  isoini2  5949  relmptopab  6213  ofres  6239  ofco  6243  tposexg  6410  tfrlemisucaccv  6477  tfrlemibex  6481  tfri1dALT  6503  tfrcl  6516  rdgivallem  6533  frecabex  6550  frectfr  6552  frecrdg  6560  pmresg  6831  mapsn  6845  mapsncnv  6850  ixpsnf1o  6891  en1  6959  2dom  6966  enpr2d  6980  en2  6981  mapxpen  7017  phplem4  7024  exmidpw2en  7085  fiintim  7104  sbthlem2  7136  elfir  7151  infglbti  7203  caseinl  7269  caseinr  7270  difinfsnlem  7277  difinfsn  7278  nninfisollemne  7309  exmidfodomrlemim  7390  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  2omotaplemap  7454  archnqq  7615  prarloclemlt  7691  prarloclemlo  7692  prarloclemcalc  7700  recexprlemm  7822  recexprlemex  7835  caucvgprlemm  7866  caucvgprprlemmu  7893  suplocexprlem2b  7912  suplocexprlemmu  7916  suplocexprlemlub  7922  1idsr  7966  recexgt0sr  7971  archsr  7980  caucvgsrlemoffval  7994  caucvgsrlemofff  7995  caucvgsrlemoffres  7998  caucvgsr  8000  ltpsrprg  8001  suplocsrlem  8006  pitonnlem2  8045  pitonn  8046  pitoregt0  8047  pitore  8048  recnnre  8049  axrnegex  8077  nntopi  8092  msqge0  8774  mulge0  8777  recexaplem2  8810  recexap  8811  recgt0  9008  recreclt  9058  nn1m1nn  9139  nn1suc  9140  nnle1eq1  9145  nn1gt1  9155  nnsub  9160  addltmul  9359  nn0le0eq0  9408  elnn0nn  9422  elnnz  9467  elznn0  9472  zlem1lt  9514  zltlem1  9515  elz2  9529  nn0n0n1ge2b  9537  nn0lt2  9539  nn0le2is012  9540  eluzaddi  9761  eluzsubi  9762  uzp1  9768  peano2uzr  9792  nn01to3  9824  qreccl  9849  irrmulap  9855  ltpnf  9988  xaddass2  10078  iccen  10214  fz01en  10261  fzpreddisj  10279  fzsuc2  10287  fseq1p1m1  10302  fseq1m1p1  10303  elfzp1b  10305  fzoss2  10382  fzval3  10422  fzosplitsnm1  10427  fzosplitprm1  10452  flhalf  10534  fldiv4lem1div2uz2  10538  modqmulnn  10576  modqmuladdnn0  10602  frec2uzrand  10639  frecuzrdg0  10647  frecuzrdg0t  10656  frecfzennn  10660  frecfzen2  10661  uzennn  10670  seqeq1  10684  seqp1g  10700  seqclg  10706  seq3m1  10707  monoord2  10720  ser3mono  10721  seqf1oglem1  10753  seqf1oglem2  10754  seqfeq4g  10765  ser0f  10768  exp3vallem  10774  expm1t  10801  expeq0  10804  expubnd  10830  binom3  10891  facndiv  10973  facavg  10980  bcn0  10989  bcnp1n  10993  bcm1k  10994  bcp1nk  10996  bcval5  10997  bcn2  10998  bcp1m1  10999  bcpasc  11000  bcn2m1  11003  hashsng  11032  hashun  11039  hashfz  11056  hashfzo  11057  seq3coll  11077  hash2en  11078  iswrdiz  11091  snopiswrd  11094  ccat1st1st  11188  swrds1  11216  cats1un  11269  wrdind  11270  wrd2ind  11271  swrdccatin1  11273  swrdccat3blem  11287  shftfval  11348  2shfti  11358  resqrexlemf1  11535  abs00ap  11589  sqabs  11609  ltabs  11614  caubnd2  11644  max0addsup  11746  rexico  11748  mulcn2  11839  climaddc1  11856  climmulc2  11858  climsubc1  11859  climsubc2  11860  iserex  11866  climlec2  11868  iser3shft  11873  climcvg1nlem  11876  serf0  11879  sumrbdc  11906  fsumm1  11943  fsump1  11947  fsum00  11989  telfsumo  11993  fsumparts  11997  hashiun  12005  binomlem  12010  binom1dif  12014  bcxmas  12016  isumsplit  12018  isum1p  12019  arisum  12025  arisum2  12026  trireciplem  12027  explecnv  12032  geolim  12038  georeclim  12040  mertenslem2  12063  mertensabs  12064  prodf1f  12070  prodrbdclem2  12100  efcllemp  12185  ef0lem  12187  efgt0  12211  eftlub  12217  efsep  12218  effsumlt  12219  tanval3ap  12241  efi4p  12244  resin4p  12245  recos4p  12246  ef01bndlem  12283  sin01bnd  12284  cos01bnd  12285  sinltxirr  12288  sin01gt0  12289  cos01gt0  12290  absefib  12298  efieq1re  12299  eirraplem  12304  dvdsdc  12325  dvdscmulr  12347  fsumdvds  12369  dvdslelemd  12370  3dvds  12391  odd2np1lem  12399  odd2np1  12400  flodddiv4  12463  bitsfzo  12482  bitsmod  12483  gcdsupex  12494  gcdsupcl  12495  gcd1  12524  nninfctlemfo  12577  nn0seqcvgd  12579  algcvg  12586  algcvgblem  12587  eucalg  12597  prmind2  12658  qden1elz  12743  dfphi2  12758  phiprm  12761  phimullem  12763  prmdiv  12773  prmdiveq  12774  prm23lt5  12802  pcpre1  12831  pczpre  12836  pcdiv  12841  pc1  12844  pcqdiv  12846  pcexp  12848  pcxnn0cl  12849  pcxcl  12850  pcdvdstr  12866  pc2dvds  12869  sumhashdc  12886  fldivp1  12887  pcfaclem  12888  qexpz  12891  expnprm  12892  prmpwdvds  12894  pockthlem  12895  4sqlem5  12921  4sqlem6  12922  4sqlem11  12940  4sqlem13m  12942  4sqlem19  12948  oddennn  12979  xpct  12983  ennnfonelemj0  12988  ennnfonelemen  13008  ctinfomlemom  13014  omctfn  13030  restid  13299  prdsex  13318  prdsval  13322  prdsbaslemss  13323  prdsbas  13325  imasbas  13356  imasplusg  13357  imasmulr  13358  imasaddfnlemg  13363  xpscf  13396  igsumvalx  13438  gsumsplit1r  13447  gsumprval  13448  gsumfzz  13544  gsumfzcl  13548  prdsgrpd  13658  prdsinvgd  13659  mulgnngsum  13680  mulgnndir  13704  mulgneg2  13709  dvdsrmuld  14076  zsssubrg  14565  znval  14616  znle  14617  znbaslemnn  14619  znf1o  14631  znleval  14633  psrval  14646  restuni2  14867  cnrest2r  14927  lmfss  14934  lmres  14938  lmtopcnp  14940  ispsmet  15013  isxmet2d  15038  ismet2  15044  blfvalps  15075  blex  15077  xblss2  15095  reopnap  15236  divcnap  15255  climcncf  15274  cncfmpt2fcntop  15289  hovera  15337  limcdifap  15352  cnplimcim  15357  cnlimcim  15361  cnlimc  15362  cnlimci  15363  dvbss  15375  dvcnp2cntop  15389  dvcn  15390  dvaddxxbr  15391  dvmulxxbr  15392  dvexp  15401  dveflem  15416  plyval  15422  elply2  15425  plyf  15427  plyss  15428  plyssc  15429  elplyr  15430  plyaddlem1  15437  plymullem1  15438  plyaddlem  15439  plymullem  15440  plyco  15449  plycj  15451  dvply1  15455  reeff1olem  15461  sinperlem  15498  sin2kpi  15501  cos2kpi  15502  sin2pim  15503  cos2pim  15504  cosq14gt0  15522  coseq0q4123  15524  tangtx  15528  abssinper  15536  sinkpi  15537  coskpi  15538  cosq34lt1  15540  logrpap0b  15566  logdivlti  15571  rpcxpsqrtth  15620  rpabscxpbnd  15630  binom4  15669  wilthlem1  15670  0sgm  15675  1sgmprm  15684  1sgm2ppw  15685  mersenne  15687  perfect1  15688  perfectlem1  15689  perfectlem2  15690  perfect  15691  lgslem1  15695  lgsval  15699  lgsfvalg  15700  lgsfcl2  15701  lgsfcl  15703  lgsval2lem  15705  lgsvalmod  15714  lgsneg  15719  lgsdilem  15722  lgsdir2lem3  15725  lgsdir  15730  lgsdilem2  15731  lgsdi  15732  lgsne0  15733  lgsabs1  15734  lgsprme0  15737  lgsdirnn0  15742  lgsdinn0  15743  gausslemma2dlem0d  15747  gausslemma2dlem1a  15753  gausslemma2dlem1f1o  15755  gausslemma2dlem3  15758  gausslemma2dlem4  15759  gausslemma2dlem5a  15760  gausslemma2dlem5  15761  gausslemma2dlem6  15762  lgseisenlem2  15766  lgseisen  15769  lgsquadlem1  15772  lgsquadlem2  15773  lgsquad2lem1  15776  lgsquad2lem2  15777  lgsquad2  15778  m1lgs  15780  2lgslem1  15786  2lgslem2  15787  2lgs  15799  2sqlem9  15819  2sqlem10  15820  ushgredgedg  16040  ushgredgedgloop  16042  wlkvtxiedg  16091  wlkvtxiedgg  16092  wlk1walkdom  16105  upgr2wlkdc  16121  clwwlkccatlem  16143  umgrclwwlkge2  16145  2omap  16446  pwle2  16451  pw1nct  16456  nninfsellemdc  16464  nnnninfen  16475  nnnninfex  16476  nninfnfiinf  16477  sbthom  16482  trirec0  16500  apdifflemr  16503  reap0  16514  nconstwlpolem  16521