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  4377  djussxp  4925  iss  5109  relresfld  5317  eldmrexrn  5849  f1oresrab  5873  fmptco  5874  fsn  5880  fnressn  5901  foima2  5957  foeqcnvco  5996  isoini2  6025  relmptopab  6291  ofres  6317  ofco  6321  suppval1  6479  suppimacnvfn  6486  tposexg  6529  tfrlemisucaccv  6596  tfrlemibex  6600  tfri1dALT  6622  tfrcl  6635  rdgivallem  6652  frecabex  6669  frectfr  6671  frecrdg  6679  pmresg  6957  mapsnd  6970  mapsn  6972  mapsncnv  6977  ixpsnf1o  7018  en1  7086  2dom  7093  mapsnend  7099  enpr2d  7111  en2  7112  mapxpen  7148  mapunen  7151  phplem4  7156  exmidpw2en  7219  fiintim  7238  sbthlem2  7275  elfir  7307  2omap  7318  infglbti  7365  caseinl  7431  caseinr  7432  difinfsnlem  7439  difinfsn  7440  nninfisollemne  7471  exmidfodomrlemim  7553  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  2omotaplemap  7623  archnqq  7784  prarloclemlt  7860  prarloclemlo  7861  prarloclemcalc  7869  recexprlemm  7991  recexprlemex  8004  caucvgprlemm  8035  caucvgprprlemmu  8062  suplocexprlem2b  8081  suplocexprlemmu  8085  suplocexprlemlub  8091  1idsr  8135  recexgt0sr  8140  archsr  8149  caucvgsrlemoffval  8163  caucvgsrlemofff  8164  caucvgsrlemoffres  8167  caucvgsr  8169  ltpsrprg  8170  suplocsrlem  8175  pitonnlem2  8214  pitonn  8215  pitoregt0  8216  pitore  8217  recnnre  8218  axrnegex  8246  nntopi  8261  msqge0  8946  mulge0  8949  recexaplem2  8982  recexap  8983  recgt0  9182  recreclt  9232  nn1m1nn  9324  nn1suc  9325  nnle1eq1  9330  nn1gt1  9340  nnsub  9345  addltmul  9546  nn0le0eq0  9595  elnn0nn  9609  elnnz  9658  elznn0  9663  zlem1lt  9705  zltlem1  9706  elz2  9720  nn0n0n1ge2b  9729  nn0lt2  9731  nn0le2is012  9732  eluzaddi  9958  eluzsubi  9959  uzp1  9965  peano2uzr  9994  nn01to3  10026  qreccl  10051  irrmulap  10058  ltpnf  10192  xaddass2  10282  iccen  10419  fz01en  10469  fzpreddisj  10488  fzsuc2  10496  fseq1p1m1  10511  fseq1m1p1  10512  elfzp1b  10514  fzoss2  10591  fzval3  10632  fzosplitsnm1  10637  fzosplitprm1  10663  flhalf  10750  fldiv4lem1div2uz2  10754  modqmulnn  10792  modqmuladdnn0  10818  frec2uzrand  10855  frecuzrdg0  10863  frecuzrdg0t  10872  frecfzennn  10876  frecfzen2  10877  uzennn  10886  seqeq1  10900  seqp1g  10916  seqclg  10922  seq3m1  10923  monoord2  10936  ser3mono  10937  seqf1oglem1  10969  seqf1oglem2  10970  seqfeq4g  10981  ser0f  10984  exp3vallem  10990  expm1t  11017  expeq0  11020  expubnd  11046  binom3  11107  facndiv  11191  facavg  11198  bcn0  11207  bcnp1n  11211  bcm1k  11212  bcp1nk  11214  bcval5  11215  bcn2  11216  bcp1m1  11217  bcpasc  11218  bcn2m1  11222  hashsng  11251  hashun  11259  hashfz  11276  hashfzo  11277  hashmap  11282  hashfibclem  11296  hashf1lem1  11299  hashf1  11301  seq3coll  11308  hash2en  11309  iswrdiz  11325  snopiswrd  11328  ccat1st1st  11423  swrds1  11454  cats1un  11507  wrdind  11508  wrd2ind  11509  swrdccatin1  11511  swrdccat3blem  11525  shftfval  11600  2shfti  11610  resqrexlemf1  11788  abs00ap  11842  sqabs  11863  ltabs  11868  caubnd2  11898  max0addsup  12000  rexico  12002  mulcn2  12094  climaddc1  12111  climmulc2  12113  climsubc1  12114  climsubc2  12115  iserex  12121  climlec2  12123  iser3shft  12128  climcvg1nlem  12131  serf0  12134  sumrbdc  12162  fsumm1  12199  fsump1  12203  fsum00  12245  telfsumo  12249  fsumparts  12253  hashiun  12261  binomlem  12266  binom1dif  12270  bcxmas  12272  isumsplit  12274  isum1p  12275  arisum  12281  arisum2  12282  trireciplem  12283  explecnv  12288  geolim  12294  georeclim  12296  mertenslem2  12319  mertensabs  12320  prodf1f  12326  prodrbdclem2  12356  efcllemp  12441  ef0lem  12443  efgt0  12467  eftlub  12473  efsep  12474  effsumlt  12475  tanval3ap  12497  efi4p  12500  resin4p  12501  recos4p  12502  ef01bndlem  12539  sin01bnd  12540  cos01bnd  12541  sinltxirr  12544  sin01gt0  12545  cos01gt0  12546  absefib  12554  efieq1re  12555  eirraplem  12560  dvdsdc  12581  dvdscmulr  12603  fsumdvds  12625  dvdslelemd  12626  3dvds  12647  odd2np1lem  12655  odd2np1  12656  flodddiv4  12719  bitsfzo  12738  bitsmod  12739  gcdsupex  12750  gcdsupcl  12751  gcd1  12780  nninfctlemfo  12833  nn0seqcvgd  12835  algcvg  12842  algcvgblem  12843  eucalg  12853  prmind2  12914  qden1elz  13001  dfphi2  13018  phiprm  13021  phimullem  13023  prmdiv  13033  prmdiveq  13034  prm23lt5  13062  pcpre1  13091  pczpre  13096  pcdiv  13101  pc1  13104  pcqdiv  13106  pcexp  13108  pcxnn0cl  13109  pcxcl  13110  pcdvdstr  13126  pc2dvds  13129  sumhashdc  13146  fldivp1  13147  pcfaclem  13148  qexpz  13151  expnprm  13152  prmpwdvds  13154  pockthlem  13155  4sqlem5  13181  4sqlem6  13182  4sqlem11  13200  4sqlem13m  13202  4sqlem19  13208  prmlem1a  13241  ballotfilemofi  13268  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilemodife  13289  ballotfilemscl  13296  ballotfilemsle  13297  oddennn  13332  xpct  13336  ennnfonelemj0  13341  ennnfonelemen  13361  ctinfomlemom  13367  omctfn  13383  restid  13653  imasbas  13677  imasplusg  13678  imasmulr  13679  imasaddfnlemg  13684  xpscf  13717  gzsumvalx  13758  gzsumsplit1r  13764  gzsumcl  13853  mulgnngzsum  13979  mulgnndir  14003  mulgneg2  14008  gsumvalfi  14201  prdsex  14221  prdsval  14222  prdsbaslemss  14223  prdsbas  14225  prdsgrpd  14246  prdsinvgd  14247  dvdsrmuld  14452  zsssubrg  14971  znval  15020  znle  15021  znbaslemnn  15023  znf1o  15035  znleval  15037  psrval  15099  restuni2  15327  cnrest2r  15387  lmfss  15394  lmres  15398  lmtopcnp  15400  ispsmet  15473  isxmet2d  15498  ismet2  15504  blfvalps  15535  blex  15537  xblss2  15555  reopnap  15696  divcnap  15715  climcncf  15734  cncfmpt2fcntop  15749  hovera  15797  limcdifap  15812  cnplimcim  15817  cnlimcim  15821  cnlimc  15822  cnlimci  15823  dvbss  15835  dvcnp2cntop  15849  dvcn  15850  dvaddxxbr  15851  dvmulxxbr  15852  dvexp  15861  dveflem  15876  plyval  15882  elply2  15885  plyf  15887  plyss  15888  plyssc  15889  elplyr  15890  plyaddlem1  15897  plymullem1  15898  plyaddlem  15899  plymullem  15900  plyco  15909  plycj  15911  dvply1  15915  reeff1olem  15921  sinperlem  15959  sin2kpi  15962  cos2kpi  15963  sin2pim  15964  cos2pim  15965  cosq14gt0  15983  coseq0q4123  15985  tangtx  15989  abssinper  15997  sinkpi  15998  coskpi  15999  cosq34lt1  16001  logrpap0b  16028  logdivlti  16033  rpcxpsqrtth  16085  rpabscxpbnd  16095  binom4  16138  birthdaylem2  16145  birthdaylem3  16146  wilthlem1  16151  0sgm  16166  ppiprm  16170  ppinprm  16171  ppiqp1le  16173  ppidif  16175  ppiqeq0  16182  ppiqltx  16183  1sgmprm  16189  1sgm2ppw  16190  ppiublem2  16193  ppiqub  16194  mersenne  16195  perfect1  16196  perfectlem1  16197  perfectlem2  16198  perfect  16199  bcp1ctr  16204  bclbnd  16205  bposlem1  16209  bposlem2  16210  bposlem3  16211  bposlem4  16212  bposlem5  16213  lgslem1  16217  lgsval  16221  lgsfvalg  16222  lgsfcl2  16223  lgsfcl  16225  lgsval2lem  16227  lgsvalmod  16236  lgsneg  16241  lgsdilem  16244  lgsdir2lem3  16247  lgsdir  16252  lgsdilem2  16253  lgsdi  16254  lgsne0  16255  lgsabs1  16256  lgsprme0  16259  lgsdirnn0  16264  lgsdinn0  16265  gausslemma2dlem0d  16269  gausslemma2dlem1a  16275  gausslemma2dlem1f1o  16277  gausslemma2dlem3  16280  gausslemma2dlem4  16281  gausslemma2dlem5a  16282  gausslemma2dlem5  16283  gausslemma2dlem6  16284  lgseisenlem2  16288  lgseisen  16291  lgsquadlem1  16294  lgsquadlem2  16295  lgsquad2lem1  16298  lgsquad2lem2  16299  lgsquad2  16300  m1lgs  16302  2lgslem1  16308  2lgslem2  16309  2lgs  16321  2sqlem9  16341  2sqlem10  16342  ushgredgedg  16565  ushgredgedgloop  16567  uhgrspansubgrlem  16615  wlkvtxiedg  16684  wlkvtxiedgg  16685  wlk1walkdom  16698  upgr2wlkdc  16716  clwwlkccatlem  16739  umgrclwwlkge2  16741  clwwlknonmpo  16767  clwwlknonex2lem2  16777  clwwlknonex2  16778  konigsberglem1  16827  pwle2  17126  pw1nct  17131  nninfsellemdc  17151  nnnninfen  17162  nnnninfex  17163  nninfnfiinf  17164  sbthom  17169  repiecelem  17172  repiecele0  17173  trirec0  17191  apdifflemr  17194  reap0  17206  nconstwlpolem  17213