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  8944  mulge0  8947  recexaplem2  8980  recexap  8981  recgt0  9180  recreclt  9230  nn1m1nn  9322  nn1suc  9323  nnle1eq1  9328  nn1gt1  9338  nnsub  9343  addltmul  9542  nn0le0eq0  9591  elnn0nn  9605  elnnz  9654  elznn0  9659  zlem1lt  9701  zltlem1  9702  elz2  9716  nn0n0n1ge2b  9725  nn0lt2  9727  nn0le2is012  9728  eluzaddi  9949  eluzsubi  9950  uzp1  9956  peano2uzr  9985  nn01to3  10017  qreccl  10042  irrmulap  10048  ltpnf  10182  xaddass2  10272  iccen  10409  fz01en  10459  fzpreddisj  10478  fzsuc2  10486  fseq1p1m1  10501  fseq1m1p1  10502  elfzp1b  10504  fzoss2  10581  fzval3  10622  fzosplitsnm1  10627  fzosplitprm1  10653  flhalf  10737  fldiv4lem1div2uz2  10741  modqmulnn  10779  modqmuladdnn0  10805  frec2uzrand  10842  frecuzrdg0  10850  frecuzrdg0t  10859  frecfzennn  10863  frecfzen2  10864  uzennn  10873  seqeq1  10887  seqp1g  10903  seqclg  10909  seq3m1  10910  monoord2  10923  ser3mono  10924  seqf1oglem1  10956  seqf1oglem2  10957  seqfeq4g  10968  ser0f  10971  exp3vallem  10977  expm1t  11004  expeq0  11007  expubnd  11033  binom3  11094  facndiv  11177  facavg  11184  bcn0  11193  bcnp1n  11197  bcm1k  11198  bcp1nk  11200  bcval5  11201  bcn2  11202  bcp1m1  11203  bcpasc  11204  bcn2m1  11208  hashsng  11237  hashun  11245  hashfz  11262  hashfzo  11263  hashmap  11268  hashfibclem  11282  hashf1lem1  11285  hashf1  11287  seq3coll  11294  hash2en  11295  iswrdiz  11311  snopiswrd  11314  ccat1st1st  11409  swrds1  11440  cats1un  11493  wrdind  11494  wrd2ind  11495  swrdccatin1  11497  swrdccat3blem  11511  shftfval  11586  2shfti  11596  resqrexlemf1  11774  abs00ap  11828  sqabs  11848  ltabs  11853  caubnd2  11883  max0addsup  11985  rexico  11987  mulcn2  12078  climaddc1  12095  climmulc2  12097  climsubc1  12098  climsubc2  12099  iserex  12105  climlec2  12107  iser3shft  12112  climcvg1nlem  12115  serf0  12118  sumrbdc  12146  fsumm1  12183  fsump1  12187  fsum00  12229  telfsumo  12233  fsumparts  12237  hashiun  12245  binomlem  12250  binom1dif  12254  bcxmas  12256  isumsplit  12258  isum1p  12259  arisum  12265  arisum2  12266  trireciplem  12267  explecnv  12272  geolim  12278  georeclim  12280  mertenslem2  12303  mertensabs  12304  prodf1f  12310  prodrbdclem2  12340  efcllemp  12425  ef0lem  12427  efgt0  12451  eftlub  12457  efsep  12458  effsumlt  12459  tanval3ap  12481  efi4p  12484  resin4p  12485  recos4p  12486  ef01bndlem  12523  sin01bnd  12524  cos01bnd  12525  sinltxirr  12528  sin01gt0  12529  cos01gt0  12530  absefib  12538  efieq1re  12539  eirraplem  12544  dvdsdc  12565  dvdscmulr  12587  fsumdvds  12609  dvdslelemd  12610  3dvds  12631  odd2np1lem  12639  odd2np1  12640  flodddiv4  12703  bitsfzo  12722  bitsmod  12723  gcdsupex  12734  gcdsupcl  12735  gcd1  12764  nninfctlemfo  12817  nn0seqcvgd  12819  algcvg  12826  algcvgblem  12827  eucalg  12837  prmind2  12898  qden1elz  12983  dfphi2  12998  phiprm  13001  phimullem  13003  prmdiv  13013  prmdiveq  13014  prm23lt5  13042  pcpre1  13071  pczpre  13076  pcdiv  13081  pc1  13084  pcqdiv  13086  pcexp  13088  pcxnn0cl  13089  pcxcl  13090  pcdvdstr  13106  pc2dvds  13109  sumhashdc  13126  fldivp1  13127  pcfaclem  13128  qexpz  13131  expnprm  13132  prmpwdvds  13134  pockthlem  13135  4sqlem5  13161  4sqlem6  13162  4sqlem11  13180  4sqlem13m  13182  4sqlem19  13188  ballotfilemofi  13219  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilemodife  13240  ballotfilemscl  13247  ballotfilemsle  13248  oddennn  13283  xpct  13287  ennnfonelemj0  13292  ennnfonelemen  13312  ctinfomlemom  13318  omctfn  13334  restid  13604  imasbas  13628  imasplusg  13629  imasmulr  13630  imasaddfnlemg  13635  xpscf  13668  gzsumvalx  13709  gzsumsplit1r  13715  gzsumcl  13804  mulgnngzsum  13930  mulgnndir  13954  mulgneg2  13959  gsumvalfi  14152  prdsex  14172  prdsval  14173  prdsbaslemss  14174  prdsbas  14176  prdsgrpd  14197  prdsinvgd  14198  dvdsrmuld  14403  zsssubrg  14922  znval  14971  znle  14972  znbaslemnn  14974  znf1o  14986  znleval  14988  psrval  15050  restuni2  15278  cnrest2r  15338  lmfss  15345  lmres  15349  lmtopcnp  15351  ispsmet  15424  isxmet2d  15449  ismet2  15455  blfvalps  15486  blex  15488  xblss2  15506  reopnap  15647  divcnap  15666  climcncf  15685  cncfmpt2fcntop  15700  hovera  15748  limcdifap  15763  cnplimcim  15768  cnlimcim  15772  cnlimc  15773  cnlimci  15774  dvbss  15786  dvcnp2cntop  15800  dvcn  15801  dvaddxxbr  15802  dvmulxxbr  15803  dvexp  15812  dveflem  15827  plyval  15833  elply2  15836  plyf  15838  plyss  15839  plyssc  15840  elplyr  15841  plyaddlem1  15848  plymullem1  15849  plyaddlem  15850  plymullem  15851  plyco  15860  plycj  15862  dvply1  15866  reeff1olem  15872  sinperlem  15909  sin2kpi  15912  cos2kpi  15913  sin2pim  15914  cos2pim  15915  cosq14gt0  15933  coseq0q4123  15935  tangtx  15939  abssinper  15947  sinkpi  15948  coskpi  15949  cosq34lt1  15951  logrpap0b  15977  logdivlti  15982  rpcxpsqrtth  16032  rpabscxpbnd  16042  binom4  16081  birthdaylem2  16088  birthdaylem3  16089  wilthlem1  16094  0sgm  16099  1sgmprm  16108  1sgm2ppw  16109  mersenne  16111  perfect1  16112  perfectlem1  16113  perfectlem2  16114  perfect  16115  lgslem1  16119  lgsval  16123  lgsfvalg  16124  lgsfcl2  16125  lgsfcl  16127  lgsval2lem  16129  lgsvalmod  16138  lgsneg  16143  lgsdilem  16146  lgsdir2lem3  16149  lgsdir  16154  lgsdilem2  16155  lgsdi  16156  lgsne0  16157  lgsabs1  16158  lgsprme0  16161  lgsdirnn0  16166  lgsdinn0  16167  gausslemma2dlem0d  16171  gausslemma2dlem1a  16177  gausslemma2dlem1f1o  16179  gausslemma2dlem3  16182  gausslemma2dlem4  16183  gausslemma2dlem5a  16184  gausslemma2dlem5  16185  gausslemma2dlem6  16186  lgseisenlem2  16190  lgseisen  16193  lgsquadlem1  16196  lgsquadlem2  16197  lgsquad2lem1  16200  lgsquad2lem2  16201  lgsquad2  16202  m1lgs  16204  2lgslem1  16210  2lgslem2  16211  2lgs  16223  2sqlem9  16243  2sqlem10  16244  ushgredgedg  16467  ushgredgedgloop  16469  uhgrspansubgrlem  16517  wlkvtxiedg  16586  wlkvtxiedgg  16587  wlk1walkdom  16600  upgr2wlkdc  16618  clwwlkccatlem  16641  umgrclwwlkge2  16643  clwwlknonmpo  16669  clwwlknonex2lem2  16679  clwwlknonex2  16680  konigsberglem1  16729  pwle2  17028  pw1nct  17033  nninfsellemdc  17053  nnnninfen  17064  nnnninfex  17065  nninfnfiinf  17066  sbthom  17071  repiecelem  17074  repiecele0  17075  trirec0  17093  apdifflemr  17096  reap0  17108  nconstwlpolem  17115