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  1807  sseqtrid  3278  ssdifin0  3578  uneqdifeqim  3582  unimax  3932  opth  4335  djussxp  4881  iss  5065  relresfld  5273  eldmrexrn  5796  f1oresrab  5820  fmptco  5821  fsn  5827  fnressn  5848  foima2  5902  foeqcnvco  5941  isoini2  5970  relmptopab  6234  ofres  6259  ofco  6263  suppval1  6417  suppimacnvfn  6424  tposexg  6467  tfrlemisucaccv  6534  tfrlemibex  6538  tfri1dALT  6560  tfrcl  6573  rdgivallem  6590  frecabex  6607  frectfr  6609  frecrdg  6617  pmresg  6888  mapsn  6902  mapsncnv  6907  ixpsnf1o  6948  en1  7016  2dom  7023  enpr2d  7040  en2  7041  mapxpen  7077  phplem4  7084  exmidpw2en  7147  fiintim  7166  sbthlem2  7200  elfir  7232  infglbti  7284  caseinl  7350  caseinr  7351  difinfsnlem  7358  difinfsn  7359  nninfisollemne  7390  exmidfodomrlemim  7472  exmidfodomrlemr  7473  exmidfodomrlemrALT  7474  2omotaplemap  7536  archnqq  7697  prarloclemlt  7773  prarloclemlo  7774  prarloclemcalc  7782  recexprlemm  7904  recexprlemex  7917  caucvgprlemm  7948  caucvgprprlemmu  7975  suplocexprlem2b  7994  suplocexprlemmu  7998  suplocexprlemlub  8004  1idsr  8048  recexgt0sr  8053  archsr  8062  caucvgsrlemoffval  8076  caucvgsrlemofff  8077  caucvgsrlemoffres  8080  caucvgsr  8082  ltpsrprg  8083  suplocsrlem  8088  pitonnlem2  8127  pitonn  8128  pitoregt0  8129  pitore  8130  recnnre  8131  axrnegex  8159  nntopi  8174  msqge0  8855  mulge0  8858  recexaplem2  8891  recexap  8892  recgt0  9089  recreclt  9139  nn1m1nn  9220  nn1suc  9221  nnle1eq1  9226  nn1gt1  9236  nnsub  9241  addltmul  9440  nn0le0eq0  9489  elnn0nn  9503  elnnz  9550  elznn0  9555  zlem1lt  9597  zltlem1  9598  elz2  9612  nn0n0n1ge2b  9620  nn0lt2  9622  nn0le2is012  9623  eluzaddi  9844  eluzsubi  9845  uzp1  9851  peano2uzr  9880  nn01to3  9912  qreccl  9937  irrmulap  9943  ltpnf  10076  xaddass2  10166  iccen  10303  fz01en  10350  fzpreddisj  10368  fzsuc2  10376  fseq1p1m1  10391  fseq1m1p1  10392  elfzp1b  10394  fzoss2  10471  fzval3  10512  fzosplitsnm1  10517  fzosplitprm1  10543  flhalf  10625  fldiv4lem1div2uz2  10629  modqmulnn  10667  modqmuladdnn0  10693  frec2uzrand  10730  frecuzrdg0  10738  frecuzrdg0t  10747  frecfzennn  10751  frecfzen2  10752  uzennn  10761  seqeq1  10775  seqp1g  10791  seqclg  10797  seq3m1  10798  monoord2  10811  ser3mono  10812  seqf1oglem1  10844  seqf1oglem2  10845  seqfeq4g  10856  ser0f  10859  exp3vallem  10865  expm1t  10892  expeq0  10895  expubnd  10921  binom3  10982  facndiv  11064  facavg  11071  bcn0  11080  bcnp1n  11084  bcm1k  11085  bcp1nk  11087  bcval5  11088  bcn2  11089  bcp1m1  11090  bcpasc  11091  bcn2m1  11094  hashsng  11123  hashun  11131  hashfz  11148  hashfzo  11149  seq3coll  11169  hash2en  11170  iswrdiz  11186  snopiswrd  11189  ccat1st1st  11284  swrds1  11315  cats1un  11368  wrdind  11369  wrd2ind  11370  swrdccatin1  11372  swrdccat3blem  11386  shftfval  11461  2shfti  11471  resqrexlemf1  11648  abs00ap  11702  sqabs  11722  ltabs  11727  caubnd2  11757  max0addsup  11859  rexico  11861  mulcn2  11952  climaddc1  11969  climmulc2  11971  climsubc1  11972  climsubc2  11973  iserex  11979  climlec2  11981  iser3shft  11986  climcvg1nlem  11989  serf0  11992  sumrbdc  12020  fsumm1  12057  fsump1  12061  fsum00  12103  telfsumo  12107  fsumparts  12111  hashiun  12119  binomlem  12124  binom1dif  12128  bcxmas  12130  isumsplit  12132  isum1p  12133  arisum  12139  arisum2  12140  trireciplem  12141  explecnv  12146  geolim  12152  georeclim  12154  mertenslem2  12177  mertensabs  12178  prodf1f  12184  prodrbdclem2  12214  efcllemp  12299  ef0lem  12301  efgt0  12325  eftlub  12331  efsep  12332  effsumlt  12333  tanval3ap  12355  efi4p  12358  resin4p  12359  recos4p  12360  ef01bndlem  12397  sin01bnd  12398  cos01bnd  12399  sinltxirr  12402  sin01gt0  12403  cos01gt0  12404  absefib  12412  efieq1re  12413  eirraplem  12418  dvdsdc  12439  dvdscmulr  12461  fsumdvds  12483  dvdslelemd  12484  3dvds  12505  odd2np1lem  12513  odd2np1  12514  flodddiv4  12577  bitsfzo  12596  bitsmod  12597  gcdsupex  12608  gcdsupcl  12609  gcd1  12638  nninfctlemfo  12691  nn0seqcvgd  12693  algcvg  12700  algcvgblem  12701  eucalg  12711  prmind2  12772  qden1elz  12857  dfphi2  12872  phiprm  12875  phimullem  12877  prmdiv  12887  prmdiveq  12888  prm23lt5  12916  pcpre1  12945  pczpre  12950  pcdiv  12955  pc1  12958  pcqdiv  12960  pcexp  12962  pcxnn0cl  12963  pcxcl  12964  pcdvdstr  12980  pc2dvds  12983  sumhashdc  13000  fldivp1  13001  pcfaclem  13002  qexpz  13005  expnprm  13006  prmpwdvds  13008  pockthlem  13009  4sqlem5  13035  4sqlem6  13036  4sqlem11  13054  4sqlem13m  13056  4sqlem19  13062  oddennn  13093  xpct  13097  ennnfonelemj0  13102  ennnfonelemen  13122  ctinfomlemom  13128  omctfn  13144  restid  13413  prdsex  13432  prdsval  13436  prdsbaslemss  13437  prdsbas  13439  imasbas  13470  imasplusg  13471  imasmulr  13472  imasaddfnlemg  13477  xpscf  13510  igsumvalx  13552  gsumsplit1r  13561  gsumprval  13562  gsumfzz  13658  gsumfzcl  13662  prdsgrpd  13772  prdsinvgd  13773  mulgnngsum  13794  mulgnndir  13818  mulgneg2  13823  dvdsrmuld  14191  zsssubrg  14681  znval  14732  znle  14733  znbaslemnn  14735  znf1o  14747  znleval  14749  psrval  14762  restuni2  14988  cnrest2r  15048  lmfss  15055  lmres  15059  lmtopcnp  15061  ispsmet  15134  isxmet2d  15159  ismet2  15165  blfvalps  15196  blex  15198  xblss2  15216  reopnap  15357  divcnap  15376  climcncf  15395  cncfmpt2fcntop  15410  hovera  15458  limcdifap  15473  cnplimcim  15478  cnlimcim  15482  cnlimc  15483  cnlimci  15484  dvbss  15496  dvcnp2cntop  15510  dvcn  15511  dvaddxxbr  15512  dvmulxxbr  15513  dvexp  15522  dveflem  15537  plyval  15543  elply2  15546  plyf  15548  plyss  15549  plyssc  15550  elplyr  15551  plyaddlem1  15558  plymullem1  15559  plyaddlem  15560  plymullem  15561  plyco  15570  plycj  15572  dvply1  15576  reeff1olem  15582  sinperlem  15619  sin2kpi  15622  cos2kpi  15623  sin2pim  15624  cos2pim  15625  cosq14gt0  15643  coseq0q4123  15645  tangtx  15649  abssinper  15657  sinkpi  15658  coskpi  15659  cosq34lt1  15661  logrpap0b  15687  logdivlti  15692  rpcxpsqrtth  15741  rpabscxpbnd  15751  binom4  15790  wilthlem1  15794  0sgm  15799  1sgmprm  15808  1sgm2ppw  15809  mersenne  15811  perfect1  15812  perfectlem1  15813  perfectlem2  15814  perfect  15815  lgslem1  15819  lgsval  15823  lgsfvalg  15824  lgsfcl2  15825  lgsfcl  15827  lgsval2lem  15829  lgsvalmod  15838  lgsneg  15843  lgsdilem  15846  lgsdir2lem3  15849  lgsdir  15854  lgsdilem2  15855  lgsdi  15856  lgsne0  15857  lgsabs1  15858  lgsprme0  15861  lgsdirnn0  15866  lgsdinn0  15867  gausslemma2dlem0d  15871  gausslemma2dlem1a  15877  gausslemma2dlem1f1o  15879  gausslemma2dlem3  15882  gausslemma2dlem4  15883  gausslemma2dlem5a  15884  gausslemma2dlem5  15885  gausslemma2dlem6  15886  lgseisenlem2  15890  lgseisen  15893  lgsquadlem1  15896  lgsquadlem2  15897  lgsquad2lem1  15900  lgsquad2lem2  15901  lgsquad2  15902  m1lgs  15904  2lgslem1  15910  2lgslem2  15911  2lgs  15923  2sqlem9  15943  2sqlem10  15944  ushgredgedg  16167  ushgredgedgloop  16169  uhgrspansubgrlem  16217  wlkvtxiedg  16286  wlkvtxiedgg  16287  wlk1walkdom  16300  upgr2wlkdc  16318  clwwlkccatlem  16341  umgrclwwlkge2  16343  clwwlknonmpo  16369  clwwlknonex2lem2  16379  clwwlknonex2  16380  konigsberglem1  16429  2omap  16715  pwle2  16720  pw1nct  16725  nninfsellemdc  16736  nnnninfen  16747  nnnninfex  16748  nninfnfiinf  16749  sbthom  16754  repiecelem  16757  repiecele0  16758  trirec0  16776  apdifflemr  16779  reap0  16791  nconstwlpolem  16798  gfsumval  16809