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  1773  sseqtrid  3233  ssdifin0  3532  uneqdifeqim  3536  unimax  3873  opth  4270  djussxp  4811  iss  4992  relresfld  5199  eldmrexrn  5703  f1oresrab  5727  fmptco  5728  fsn  5734  fnressn  5748  foima2  5798  foeqcnvco  5837  isoini2  5866  ofres  6150  ofco  6154  tposexg  6316  tfrlemisucaccv  6383  tfrlemibex  6387  tfri1dALT  6409  tfrcl  6422  rdgivallem  6439  frecabex  6456  frectfr  6458  frecrdg  6466  pmresg  6735  mapsn  6749  mapsncnv  6754  ixpsnf1o  6795  en1  6858  2dom  6864  enpr2d  6876  mapxpen  6909  phplem4  6916  exmidpw2en  6973  fiintim  6992  sbthlem2  7024  elfir  7039  infglbti  7091  caseinl  7157  caseinr  7158  difinfsnlem  7165  difinfsn  7166  nninfisollemne  7197  exmidfodomrlemim  7268  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  2omotaplemap  7324  archnqq  7484  prarloclemlt  7560  prarloclemlo  7561  prarloclemcalc  7569  recexprlemm  7691  recexprlemex  7704  caucvgprlemm  7735  caucvgprprlemmu  7762  suplocexprlem2b  7781  suplocexprlemmu  7785  suplocexprlemlub  7791  1idsr  7835  recexgt0sr  7840  archsr  7849  caucvgsrlemoffval  7863  caucvgsrlemofff  7864  caucvgsrlemoffres  7867  caucvgsr  7869  ltpsrprg  7870  suplocsrlem  7875  pitonnlem2  7914  pitonn  7915  pitoregt0  7916  pitore  7917  recnnre  7918  axrnegex  7946  nntopi  7961  msqge0  8643  mulge0  8646  recexaplem2  8679  recexap  8680  recgt0  8877  recreclt  8927  nn1m1nn  9008  nn1suc  9009  nnle1eq1  9014  nn1gt1  9024  nnsub  9029  addltmul  9228  nn0le0eq0  9277  elnn0nn  9291  elnnz  9336  elznn0  9341  zlem1lt  9382  zltlem1  9383  elz2  9397  nn0n0n1ge2b  9405  nn0lt2  9407  nn0le2is012  9408  eluzaddi  9628  eluzsubi  9629  uzp1  9635  peano2uzr  9659  nn01to3  9691  qreccl  9716  irrmulap  9722  ltpnf  9855  xaddass2  9945  iccen  10081  fz01en  10128  fzpreddisj  10146  fzsuc2  10154  fseq1p1m1  10169  fseq1m1p1  10170  elfzp1b  10172  fzoss2  10248  fzval3  10280  fzosplitsnm1  10285  fzosplitprm1  10310  flhalf  10392  fldiv4lem1div2uz2  10396  modqmulnn  10434  modqmuladdnn0  10460  frec2uzrand  10497  frecuzrdg0  10505  frecuzrdg0t  10514  frecfzennn  10518  frecfzen2  10519  uzennn  10528  seqeq1  10542  seqp1g  10558  seqclg  10564  seq3m1  10565  monoord2  10578  ser3mono  10579  seqf1oglem1  10611  seqf1oglem2  10612  seqfeq4g  10623  ser0f  10626  exp3vallem  10632  expm1t  10659  expeq0  10662  expubnd  10688  binom3  10749  facndiv  10831  facavg  10838  bcn0  10847  bcnp1n  10851  bcm1k  10852  bcp1nk  10854  bcval5  10855  bcn2  10856  bcp1m1  10857  bcpasc  10858  bcn2m1  10861  hashsng  10890  hashun  10897  hashfz  10913  hashfzo  10914  seq3coll  10934  iswrdiz  10942  snopiswrd  10945  shftfval  10986  2shfti  10996  resqrexlemf1  11173  abs00ap  11227  sqabs  11247  ltabs  11252  caubnd2  11282  max0addsup  11384  rexico  11386  mulcn2  11477  climaddc1  11494  climmulc2  11496  climsubc1  11497  climsubc2  11498  iserex  11504  climlec2  11506  iser3shft  11511  climcvg1nlem  11514  serf0  11517  sumrbdc  11544  fsumm1  11581  fsump1  11585  fsum00  11627  telfsumo  11631  fsumparts  11635  hashiun  11643  binomlem  11648  binom1dif  11652  bcxmas  11654  isumsplit  11656  isum1p  11657  arisum  11663  arisum2  11664  trireciplem  11665  explecnv  11670  geolim  11676  georeclim  11678  mertenslem2  11701  mertensabs  11702  prodf1f  11708  prodrbdclem2  11738  efcllemp  11823  ef0lem  11825  efgt0  11849  eftlub  11855  efsep  11856  effsumlt  11857  tanval3ap  11879  efi4p  11882  resin4p  11883  recos4p  11884  ef01bndlem  11921  sin01bnd  11922  cos01bnd  11923  sinltxirr  11926  sin01gt0  11927  cos01gt0  11928  absefib  11936  efieq1re  11937  eirraplem  11942  dvdsdc  11963  dvdscmulr  11985  fsumdvds  12007  dvdslelemd  12008  3dvds  12029  odd2np1lem  12037  odd2np1  12038  flodddiv4  12101  bitsfzo  12119  gcdsupex  12124  gcdsupcl  12125  gcd1  12154  nninfctlemfo  12207  nn0seqcvgd  12209  algcvg  12216  algcvgblem  12217  eucalg  12227  prmind2  12288  qden1elz  12373  dfphi2  12388  phiprm  12391  phimullem  12393  prmdiv  12403  prmdiveq  12404  prm23lt5  12432  pcpre1  12461  pczpre  12466  pcdiv  12471  pc1  12474  pcqdiv  12476  pcexp  12478  pcxnn0cl  12479  pcxcl  12480  pcdvdstr  12496  pc2dvds  12499  sumhashdc  12516  fldivp1  12517  pcfaclem  12518  qexpz  12521  expnprm  12522  prmpwdvds  12524  pockthlem  12525  4sqlem5  12551  4sqlem6  12552  4sqlem11  12570  4sqlem13m  12572  4sqlem19  12578  oddennn  12609  xpct  12613  ennnfonelemj0  12618  ennnfonelemen  12638  ctinfomlemom  12644  omctfn  12660  restid  12921  prdsex  12940  imasbas  12950  imasplusg  12951  imasmulr  12952  imasaddfnlemg  12957  xpscf  12990  igsumvalx  13032  gsumsplit1r  13041  gsumprval  13042  gsumfzz  13127  gsumfzcl  13131  mulgnngsum  13257  mulgnndir  13281  mulgneg2  13286  dvdsrmuld  13652  zsssubrg  14141  znval  14192  znle  14193  znbaslemnn  14195  znf1o  14207  znleval  14209  psrval  14220  restuni2  14413  cnrest2r  14473  lmfss  14480  lmres  14484  lmtopcnp  14486  ispsmet  14559  isxmet2d  14584  ismet2  14590  blfvalps  14621  blex  14623  xblss2  14641  reopnap  14782  divcnap  14801  climcncf  14820  cncfmpt2fcntop  14835  hovera  14883  limcdifap  14898  cnplimcim  14903  cnlimcim  14907  cnlimc  14908  cnlimci  14909  dvbss  14921  dvcnp2cntop  14935  dvcn  14936  dvaddxxbr  14937  dvmulxxbr  14938  dvexp  14947  dveflem  14962  plyval  14968  elply2  14971  plyf  14973  plyss  14974  plyssc  14975  elplyr  14976  plyaddlem1  14983  plymullem1  14984  plyaddlem  14985  plymullem  14986  plyco  14995  plycj  14997  dvply1  15001  reeff1olem  15007  sinperlem  15044  sin2kpi  15047  cos2kpi  15048  sin2pim  15049  cos2pim  15050  cosq14gt0  15068  coseq0q4123  15070  tangtx  15074  abssinper  15082  sinkpi  15083  coskpi  15084  cosq34lt1  15086  logrpap0b  15112  logdivlti  15117  rpcxpsqrtth  15166  rpabscxpbnd  15176  binom4  15215  wilthlem1  15216  0sgm  15221  1sgmprm  15230  1sgm2ppw  15231  mersenne  15233  perfect1  15234  perfectlem1  15235  perfectlem2  15236  perfect  15237  lgslem1  15241  lgsval  15245  lgsfvalg  15246  lgsfcl2  15247  lgsfcl  15249  lgsval2lem  15251  lgsvalmod  15260  lgsneg  15265  lgsdilem  15268  lgsdir2lem3  15271  lgsdir  15276  lgsdilem2  15277  lgsdi  15278  lgsne0  15279  lgsabs1  15280  lgsprme0  15283  lgsdirnn0  15288  lgsdinn0  15289  gausslemma2dlem0d  15293  gausslemma2dlem1a  15299  gausslemma2dlem1f1o  15301  gausslemma2dlem3  15304  gausslemma2dlem4  15305  gausslemma2dlem5a  15306  gausslemma2dlem5  15307  gausslemma2dlem6  15308  lgseisenlem2  15312  lgseisen  15315  lgsquadlem1  15318  lgsquadlem2  15319  lgsquad2lem1  15322  lgsquad2lem2  15323  lgsquad2  15324  m1lgs  15326  2lgslem1  15332  2lgslem2  15333  2lgs  15345  2sqlem9  15365  2sqlem10  15366  pwle2  15643  pw1nct  15647  nninfsellemdc  15654  nnnninfen  15665  sbthom  15670  trirec0  15688  apdifflemr  15691  reap0  15702  nconstwlpolem  15709