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  1808  sseqtrid  3290  ssdifin0  3593  uneqdifeqim  3597  unimax  3950  opth  4355  djussxp  4902  iss  5086  relresfld  5294  eldmrexrn  5820  f1oresrab  5844  fmptco  5845  fsn  5851  fnressn  5872  foima2  5926  foeqcnvco  5965  isoini2  5994  relmptopab  6258  ofres  6283  ofco  6287  suppval1  6441  suppimacnvfn  6448  tposexg  6491  tfrlemisucaccv  6558  tfrlemibex  6562  tfri1dALT  6584  tfrcl  6597  rdgivallem  6614  frecabex  6631  frectfr  6633  frecrdg  6641  pmresg  6912  mapsnd  6925  mapsn  6927  mapsncnv  6932  ixpsnf1o  6973  en1  7041  2dom  7048  mapsnend  7054  enpr2d  7066  en2  7067  mapxpen  7103  mapunen  7106  phplem4  7111  exmidpw2en  7174  fiintim  7193  sbthlem2  7230  elfir  7262  2omap  7271  infglbti  7318  caseinl  7384  caseinr  7385  difinfsnlem  7392  difinfsn  7393  nninfisollemne  7424  exmidfodomrlemim  7506  exmidfodomrlemr  7507  exmidfodomrlemrALT  7508  2omotaplemap  7573  archnqq  7734  prarloclemlt  7810  prarloclemlo  7811  prarloclemcalc  7819  recexprlemm  7941  recexprlemex  7954  caucvgprlemm  7985  caucvgprprlemmu  8012  suplocexprlem2b  8031  suplocexprlemmu  8035  suplocexprlemlub  8041  1idsr  8085  recexgt0sr  8090  archsr  8099  caucvgsrlemoffval  8113  caucvgsrlemofff  8114  caucvgsrlemoffres  8117  caucvgsr  8119  ltpsrprg  8120  suplocsrlem  8125  pitonnlem2  8164  pitonn  8165  pitoregt0  8166  pitore  8167  recnnre  8168  axrnegex  8196  nntopi  8211  msqge0  8892  mulge0  8895  recexaplem2  8928  recexap  8929  recgt0  9126  recreclt  9176  nn1m1nn  9257  nn1suc  9258  nnle1eq1  9263  nn1gt1  9273  nnsub  9278  addltmul  9477  nn0le0eq0  9526  elnn0nn  9540  elnnz  9589  elznn0  9594  zlem1lt  9636  zltlem1  9637  elz2  9651  nn0n0n1ge2b  9660  nn0lt2  9662  nn0le2is012  9663  eluzaddi  9884  eluzsubi  9885  uzp1  9891  peano2uzr  9920  nn01to3  9952  qreccl  9977  irrmulap  9983  ltpnf  10116  xaddass2  10206  iccen  10343  fz01en  10390  fzpreddisj  10409  fzsuc2  10417  fseq1p1m1  10432  fseq1m1p1  10433  elfzp1b  10435  fzoss2  10512  fzval3  10553  fzosplitsnm1  10558  fzosplitprm1  10584  flhalf  10666  fldiv4lem1div2uz2  10670  modqmulnn  10708  modqmuladdnn0  10734  frec2uzrand  10771  frecuzrdg0  10779  frecuzrdg0t  10788  frecfzennn  10792  frecfzen2  10793  uzennn  10802  seqeq1  10816  seqp1g  10832  seqclg  10838  seq3m1  10839  monoord2  10852  ser3mono  10853  seqf1oglem1  10885  seqf1oglem2  10886  seqfeq4g  10897  ser0f  10900  exp3vallem  10906  expm1t  10933  expeq0  10936  expubnd  10962  binom3  11023  facndiv  11105  facavg  11112  bcn0  11121  bcnp1n  11125  bcm1k  11126  bcp1nk  11128  bcval5  11129  bcn2  11130  bcp1m1  11131  bcpasc  11132  bcn2m1  11136  hashsng  11165  hashun  11173  hashfz  11190  hashfzo  11191  hashmap  11196  hashfibclem  11210  seq3coll  11218  hash2en  11219  iswrdiz  11235  snopiswrd  11238  ccat1st1st  11333  swrds1  11364  cats1un  11417  wrdind  11418  wrd2ind  11419  swrdccatin1  11421  swrdccat3blem  11435  shftfval  11510  2shfti  11520  resqrexlemf1  11697  abs00ap  11751  sqabs  11771  ltabs  11776  caubnd2  11806  max0addsup  11908  rexico  11910  mulcn2  12001  climaddc1  12018  climmulc2  12020  climsubc1  12021  climsubc2  12022  iserex  12028  climlec2  12030  iser3shft  12035  climcvg1nlem  12038  serf0  12041  sumrbdc  12069  fsumm1  12106  fsump1  12110  fsum00  12152  telfsumo  12156  fsumparts  12160  hashiun  12168  binomlem  12173  binom1dif  12177  bcxmas  12179  isumsplit  12181  isum1p  12182  arisum  12188  arisum2  12189  trireciplem  12190  explecnv  12195  geolim  12201  georeclim  12203  mertenslem2  12226  mertensabs  12227  prodf1f  12233  prodrbdclem2  12263  efcllemp  12348  ef0lem  12350  efgt0  12374  eftlub  12380  efsep  12381  effsumlt  12382  tanval3ap  12404  efi4p  12407  resin4p  12408  recos4p  12409  ef01bndlem  12446  sin01bnd  12447  cos01bnd  12448  sinltxirr  12451  sin01gt0  12452  cos01gt0  12453  absefib  12461  efieq1re  12462  eirraplem  12467  dvdsdc  12488  dvdscmulr  12510  fsumdvds  12532  dvdslelemd  12533  3dvds  12554  odd2np1lem  12562  odd2np1  12563  flodddiv4  12626  bitsfzo  12645  bitsmod  12646  gcdsupex  12657  gcdsupcl  12658  gcd1  12687  nninfctlemfo  12740  nn0seqcvgd  12742  algcvg  12749  algcvgblem  12750  eucalg  12760  prmind2  12821  qden1elz  12906  dfphi2  12921  phiprm  12924  phimullem  12926  prmdiv  12936  prmdiveq  12937  prm23lt5  12965  pcpre1  12994  pczpre  12999  pcdiv  13004  pc1  13007  pcqdiv  13009  pcexp  13011  pcxnn0cl  13012  pcxcl  13013  pcdvdstr  13029  pc2dvds  13032  sumhashdc  13049  fldivp1  13050  pcfaclem  13051  qexpz  13054  expnprm  13055  prmpwdvds  13057  pockthlem  13058  4sqlem5  13084  4sqlem6  13085  4sqlem11  13103  4sqlem13m  13105  4sqlem19  13111  ballotfilemofi  13142  ballotfilemfc0  13153  ballotfilemfcc  13154  ballotfilemodife  13158  oddennn  13160  xpct  13164  ennnfonelemj0  13169  ennnfonelemen  13189  ctinfomlemom  13195  omctfn  13211  restid  13480  prdsex  13499  prdsval  13503  prdsbaslemss  13504  prdsbas  13506  imasbas  13537  imasplusg  13538  imasmulr  13539  imasaddfnlemg  13544  xpscf  13577  igsumvalx  13619  gsumsplit1r  13628  gsumprval  13629  gsumfzz  13725  gsumfzcl  13729  prdsgrpd  13839  prdsinvgd  13840  mulgnngsum  13861  mulgnndir  13885  mulgneg2  13890  dvdsrmuld  14258  zsssubrg  14750  znval  14801  znle  14802  znbaslemnn  14804  znf1o  14816  znleval  14818  psrval  14831  restuni2  15059  cnrest2r  15119  lmfss  15126  lmres  15130  lmtopcnp  15132  ispsmet  15205  isxmet2d  15230  ismet2  15236  blfvalps  15267  blex  15269  xblss2  15287  reopnap  15428  divcnap  15447  climcncf  15466  cncfmpt2fcntop  15481  hovera  15529  limcdifap  15544  cnplimcim  15549  cnlimcim  15553  cnlimc  15554  cnlimci  15555  dvbss  15567  dvcnp2cntop  15581  dvcn  15582  dvaddxxbr  15583  dvmulxxbr  15584  dvexp  15593  dveflem  15608  plyval  15614  elply2  15617  plyf  15619  plyss  15620  plyssc  15621  elplyr  15622  plyaddlem1  15629  plymullem1  15630  plyaddlem  15631  plymullem  15632  plyco  15641  plycj  15643  dvply1  15647  reeff1olem  15653  sinperlem  15690  sin2kpi  15693  cos2kpi  15694  sin2pim  15695  cos2pim  15696  cosq14gt0  15714  coseq0q4123  15716  tangtx  15720  abssinper  15728  sinkpi  15729  coskpi  15730  cosq34lt1  15732  logrpap0b  15758  logdivlti  15763  rpcxpsqrtth  15812  rpabscxpbnd  15822  binom4  15861  wilthlem1  15865  0sgm  15870  1sgmprm  15879  1sgm2ppw  15880  mersenne  15882  perfect1  15883  perfectlem1  15884  perfectlem2  15885  perfect  15886  lgslem1  15890  lgsval  15894  lgsfvalg  15895  lgsfcl2  15896  lgsfcl  15898  lgsval2lem  15900  lgsvalmod  15909  lgsneg  15914  lgsdilem  15917  lgsdir2lem3  15920  lgsdir  15925  lgsdilem2  15926  lgsdi  15927  lgsne0  15928  lgsabs1  15929  lgsprme0  15932  lgsdirnn0  15937  lgsdinn0  15938  gausslemma2dlem0d  15942  gausslemma2dlem1a  15948  gausslemma2dlem1f1o  15950  gausslemma2dlem3  15953  gausslemma2dlem4  15954  gausslemma2dlem5a  15955  gausslemma2dlem5  15956  gausslemma2dlem6  15957  lgseisenlem2  15961  lgseisen  15964  lgsquadlem1  15967  lgsquadlem2  15968  lgsquad2lem1  15971  lgsquad2lem2  15972  lgsquad2  15973  m1lgs  15975  2lgslem1  15981  2lgslem2  15982  2lgs  15994  2sqlem9  16014  2sqlem10  16015  ushgredgedg  16238  ushgredgedgloop  16240  uhgrspansubgrlem  16288  wlkvtxiedg  16357  wlkvtxiedgg  16358  wlk1walkdom  16371  upgr2wlkdc  16389  clwwlkccatlem  16412  umgrclwwlkge2  16414  clwwlknonmpo  16440  clwwlknonex2lem2  16450  clwwlknonex2  16451  konigsberglem1  16500  pwle2  16789  pw1nct  16794  nninfsellemdc  16805  nnnninfen  16816  nnnninfex  16817  nninfnfiinf  16818  sbthom  16823  repiecelem  16826  repiecele0  16827  trirec0  16845  apdifflemr  16848  reap0  16860  trimul0or  16862  nconstwlpolem  16868  gfsumval  16879