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  suppinisegdc  6513  tposexg  6534  tfrlemisucaccv  6601  tfrlemibex  6605  tfri1dALT  6627  tfrcl  6640  rdgivallem  6657  frecabex  6674  frectfr  6676  frecrdg  6684  pmresg  6962  mapsnd  6976  mapsn  6978  mapsncnv  6983  ixpsnf1o  7024  en1  7092  2dom  7099  mapsnend  7105  enpr2d  7117  en2  7118  mapxpen  7154  mapunen  7157  phplem4  7162  exmidpw2en  7225  fiintim  7244  sbthlem2  7282  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  9663  elznn0  9668  zlem1lt  9710  zltlem1  9711  elz2  9725  nn0n0n1ge2b  9734  nn0lt2  9736  nn0le2is012  9737  eluzaddi  9964  eluzsubi  9965  uzp1  9971  peano2uzr  10000  nn01to3  10032  qreccl  10057  irrmulap  10064  ltpnf  10198  xaddass2  10288  iccen  10425  fz01en  10475  fzpreddisj  10494  fzsuc2  10502  fseq1p1m1  10517  fseq1m1p1  10518  elfzp1b  10520  fzoss2  10597  fzval3  10638  fzosplitsnm1  10643  fzosplitprm1  10669  flhalf  10757  fldiv4lem1div2uz2  10761  modqmulnn  10799  modqmuladdnn0  10825  frec2uzrand  10862  frecuzrdg0  10870  frecuzrdg0t  10879  frecfzennn  10883  frecfzen2  10884  uzennn  10893  seqeq1  10907  seqp1g  10923  seqclg  10929  seq3m1  10930  monoord2  10943  ser3mono  10944  seqf1oglem1  10976  seqf1oglem2  10977  seqfeq4g  10988  ser0f  10991  exp3vallem  10997  expm1t  11024  expeq0  11027  expubnd  11053  binom3  11114  facndiv  11198  facavg  11205  bcn0  11214  bcnp1n  11218  bcm1k  11219  bcp1nk  11221  bcval5  11222  bcn2  11223  bcp1m1  11224  bcpasc  11225  bcn2m1  11229  hashsng  11258  hashun  11266  hashfz  11283  hashfzo  11284  hashmap  11289  hashfibclem  11303  hashf1lem1  11306  hashf1  11308  seq3coll  11315  hash2en  11316  iswrdiz  11332  snopiswrd  11335  ccat1st1st  11430  swrds1  11461  cats1un  11514  wrdind  11515  wrd2ind  11516  swrdccatin1  11518  swrdccat3blem  11532  shftfval  11607  2shfti  11617  resqrexlemf1  11795  abs00ap  11849  sqabs  11870  ltabs  11875  caubnd2  11905  max0addsup  12007  rexico  12009  mulcn2  12102  climaddc1  12119  climmulc2  12121  climsubc1  12122  climsubc2  12123  iserex  12129  climlec2  12131  iser3shft  12136  climcvg1nlem  12139  serf0  12142  sumrbdc  12170  fsumm1  12207  fsump1  12211  fsum00  12253  telfsumo  12257  fsumparts  12261  hashiun  12269  binomlem  12274  binom1dif  12278  bcxmas  12280  isumsplit  12282  isum1p  12283  arisum  12289  arisum2  12290  trireciplem  12291  explecnv  12296  geolim  12302  georeclim  12304  mertenslem2  12327  mertensabs  12328  prodf1f  12334  prodrbdclem2  12364  efcllemp  12449  ef0lem  12451  efgt0  12475  eftlub  12481  efsep  12482  effsumlt  12483  tanval3ap  12505  efi4p  12508  resin4p  12509  recos4p  12510  ef01bndlem  12547  sin01bnd  12548  cos01bnd  12549  sinltxirr  12552  sin01gt0  12553  cos01gt0  12554  absefib  12562  efieq1re  12563  eirraplem  12568  dvdsdc  12589  dvdscmulr  12611  fsumdvds  12633  dvdslelemd  12634  3dvds  12655  odd2np1lem  12663  odd2np1  12664  flodddiv4  12727  bitsfzo  12746  bitsmod  12747  gcdsupex  12758  gcdsupcl  12759  gcd1  12788  nninfctlemfo  12841  nn0seqcvgd  12843  algcvg  12850  algcvgblem  12851  eucalg  12861  prmind2  12922  qden1elz  13009  dfphi2  13026  phiprm  13029  phimullem  13031  prmdiv  13041  prmdiveq  13042  prm23lt5  13070  pcpre1  13099  pczpre  13104  pcdiv  13109  pc1  13112  pcqdiv  13114  pcexp  13116  pcxnn0cl  13117  pcxcl  13118  pcdvdstr  13134  pc2dvds  13137  sumhashdc  13154  fldivp1  13155  pcfaclem  13156  qexpz  13159  expnprm  13160  prmpwdvds  13162  pockthlem  13163  4sqlem5  13189  4sqlem6  13190  4sqlem11  13208  4sqlem13m  13210  4sqlem19  13216  prmlem1a  13249  ballotfilemofi  13276  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilemodife  13297  ballotfilemscl  13304  ballotfilemsle  13305  oddennn  13340  xpct  13344  ennnfonelemj0  13349  ennnfonelemen  13369  ctinfomlemom  13375  omctfn  13391  restid  13662  imasbas  13686  imasplusg  13687  imasmulr  13688  imasaddfnlemg  13693  xpscf  13726  gzsumvalx  13767  gzsumsplit1r  13773  gzsumcl  13862  mulgnngzsum  13988  mulgnndir  14012  mulgneg2  14017  cntrnsg  14175  gsumvalfi  14241  gsum2dfilem2  14271  prdsex  14278  prdsval  14279  prdsbaslemss  14280  prdsbas  14282  prdsgrpd  14303  prdsinvgd  14304  dvdsrmuld  14511  zsssubrg  15030  znval  15079  znle  15080  znbaslemnn  15082  znf1o  15094  znleval  15096  psrval  15160  psrlidmfi  15208  psrridmfi  15209  mplsubgfileminv  15233  restuni2  15420  cnrest2r  15480  lmfss  15487  lmres  15491  lmtopcnp  15493  ispsmet  15566  isxmet2d  15591  ismet2  15597  blfvalps  15628  blex  15630  xblss2  15648  reopnap  15789  divcnap  15808  climcncf  15827  cncfmpt2fcntop  15842  hovera  15890  limcdifap  15905  cnplimcim  15910  cnlimcim  15914  cnlimc  15915  cnlimci  15916  dvbss  15928  dvcnp2cntop  15942  dvcn  15943  dvaddxxbr  15944  dvmulxxbr  15945  dvexp  15954  dveflem  15969  plyval  15975  elply2  15978  plyf  15980  plyss  15981  plyssc  15982  elplyr  15983  plyaddlem1  15990  plymullem1  15991  plyaddlem  15992  plymullem  15993  plyco  16002  plycj  16004  dvply1  16008  reeff1olem  16014  sinperlem  16052  sin2kpi  16055  cos2kpi  16056  sin2pim  16057  cos2pim  16058  cosq14gt0  16076  coseq0q4123  16078  tangtx  16082  abssinper  16090  sinkpi  16091  coskpi  16092  cosq34lt1  16095  logrpap0b  16123  logdivlti  16128  rpcxpsqrtth  16182  rpabscxpbnd  16192  binom4  16236  birthdaylem2  16243  birthdaylem3  16244  wilthlem1  16249  0sgm  16271  ppiprm  16276  ppinprm  16277  chtprm  16278  chtnprm  16279  chtdif  16281  ppiqp1le  16284  ppidif  16286  ppiqeq0  16297  ppiqltx  16298  prmorcht  16299  1sgmprm  16305  1sgm2ppw  16306  ppiublem2  16309  ppiqub  16310  chtublem  16312  chtqub  16313  mersenne  16314  perfect1  16315  perfectlem1  16316  perfectlem2  16317  perfect  16318  bcp1ctr  16323  bclbnd  16324  bposlem1  16328  bposlem2  16329  bposlem3  16330  bposlem4  16331  bposlem5  16332  bposlem6  16333  bposlem9  16336  bpos  16337  lgslem1  16341  lgsval  16345  lgsfvalg  16346  lgsfcl2  16347  lgsfcl  16349  lgsval2lem  16351  lgsvalmod  16360  lgsneg  16365  lgsdilem  16368  lgsdir2lem3  16371  lgsdir  16376  lgsdilem2  16377  lgsdi  16378  lgsne0  16379  lgsabs1  16380  lgsprme0  16383  lgsdirnn0  16388  lgsdinn0  16389  gausslemma2dlem0d  16393  gausslemma2dlem1a  16399  gausslemma2dlem1f1o  16401  gausslemma2dlem3  16404  gausslemma2dlem4  16405  gausslemma2dlem5a  16406  gausslemma2dlem5  16407  gausslemma2dlem6  16408  lgseisenlem2  16412  lgseisen  16415  lgsquadlem1  16418  lgsquadlem2  16419  lgsquad2lem1  16422  lgsquad2lem2  16423  lgsquad2  16424  m1lgs  16426  2lgslem1  16432  2lgslem2  16433  2lgs  16445  2sqlem9  16465  2sqlem10  16466  ushgredgedg  16689  ushgredgedgloop  16691  uhgrspansubgrlem  16739  wlkvtxiedg  16808  wlkvtxiedgg  16809  wlk1walkdom  16822  upgr2wlkdc  16840  clwwlkccatlem  16863  umgrclwwlkge2  16865  clwwlknonmpo  16891  clwwlknonex2lem2  16901  clwwlknonex2  16902  konigsberglem1  16951  pwle2  17250  pw1nct  17255  nninfsellemdc  17276  nnnninfen  17287  nnnninfex  17288  nninfnfiinf  17289  sbthom  17294  repiecelem  17297  repiecele0  17298  trirec0  17317  apdifflemr  17320  reap0  17332  nconstwlpolem  17339