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  1807  sseqtrid  3277  ssdifin0  3576  uneqdifeqim  3580  unimax  3927  opth  4329  djussxp  4875  iss  5059  relresfld  5266  eldmrexrn  5788  f1oresrab  5812  fmptco  5813  fsn  5819  fnressn  5839  foima2  5891  foeqcnvco  5930  isoini2  5959  relmptopab  6223  ofres  6249  ofco  6253  tposexg  6423  tfrlemisucaccv  6490  tfrlemibex  6494  tfri1dALT  6516  tfrcl  6529  rdgivallem  6546  frecabex  6563  frectfr  6565  frecrdg  6573  pmresg  6844  mapsn  6858  mapsncnv  6863  ixpsnf1o  6904  en1  6972  2dom  6979  enpr2d  6996  en2  6997  mapxpen  7033  phplem4  7040  exmidpw2en  7103  fiintim  7122  sbthlem2  7156  elfir  7171  infglbti  7223  caseinl  7289  caseinr  7290  difinfsnlem  7297  difinfsn  7298  nninfisollemne  7329  exmidfodomrlemim  7411  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  2omotaplemap  7475  archnqq  7636  prarloclemlt  7712  prarloclemlo  7713  prarloclemcalc  7721  recexprlemm  7843  recexprlemex  7856  caucvgprlemm  7887  caucvgprprlemmu  7914  suplocexprlem2b  7933  suplocexprlemmu  7937  suplocexprlemlub  7943  1idsr  7987  recexgt0sr  7992  archsr  8001  caucvgsrlemoffval  8015  caucvgsrlemofff  8016  caucvgsrlemoffres  8019  caucvgsr  8021  ltpsrprg  8022  suplocsrlem  8027  pitonnlem2  8066  pitonn  8067  pitoregt0  8068  pitore  8069  recnnre  8070  axrnegex  8098  nntopi  8113  msqge0  8795  mulge0  8798  recexaplem2  8831  recexap  8832  recgt0  9029  recreclt  9079  nn1m1nn  9160  nn1suc  9161  nnle1eq1  9166  nn1gt1  9176  nnsub  9181  addltmul  9380  nn0le0eq0  9429  elnn0nn  9443  elnnz  9488  elznn0  9493  zlem1lt  9535  zltlem1  9536  elz2  9550  nn0n0n1ge2b  9558  nn0lt2  9560  nn0le2is012  9561  eluzaddi  9782  eluzsubi  9783  uzp1  9789  peano2uzr  9818  nn01to3  9850  qreccl  9875  irrmulap  9881  ltpnf  10014  xaddass2  10104  iccen  10240  fz01en  10287  fzpreddisj  10305  fzsuc2  10313  fseq1p1m1  10328  fseq1m1p1  10329  elfzp1b  10331  fzoss2  10408  fzval3  10448  fzosplitsnm1  10453  fzosplitprm1  10479  flhalf  10561  fldiv4lem1div2uz2  10565  modqmulnn  10603  modqmuladdnn0  10629  frec2uzrand  10666  frecuzrdg0  10674  frecuzrdg0t  10683  frecfzennn  10687  frecfzen2  10688  uzennn  10697  seqeq1  10711  seqp1g  10727  seqclg  10733  seq3m1  10734  monoord2  10747  ser3mono  10748  seqf1oglem1  10780  seqf1oglem2  10781  seqfeq4g  10792  ser0f  10795  exp3vallem  10801  expm1t  10828  expeq0  10831  expubnd  10857  binom3  10918  facndiv  11000  facavg  11007  bcn0  11016  bcnp1n  11020  bcm1k  11021  bcp1nk  11023  bcval5  11024  bcn2  11025  bcp1m1  11026  bcpasc  11027  bcn2m1  11030  hashsng  11059  hashun  11067  hashfz  11084  hashfzo  11085  seq3coll  11105  hash2en  11106  iswrdiz  11119  snopiswrd  11122  ccat1st1st  11217  swrds1  11248  cats1un  11301  wrdind  11302  wrd2ind  11303  swrdccatin1  11305  swrdccat3blem  11319  shftfval  11381  2shfti  11391  resqrexlemf1  11568  abs00ap  11622  sqabs  11642  ltabs  11647  caubnd2  11677  max0addsup  11779  rexico  11781  mulcn2  11872  climaddc1  11889  climmulc2  11891  climsubc1  11892  climsubc2  11893  iserex  11899  climlec2  11901  iser3shft  11906  climcvg1nlem  11909  serf0  11912  sumrbdc  11939  fsumm1  11976  fsump1  11980  fsum00  12022  telfsumo  12026  fsumparts  12030  hashiun  12038  binomlem  12043  binom1dif  12047  bcxmas  12049  isumsplit  12051  isum1p  12052  arisum  12058  arisum2  12059  trireciplem  12060  explecnv  12065  geolim  12071  georeclim  12073  mertenslem2  12096  mertensabs  12097  prodf1f  12103  prodrbdclem2  12133  efcllemp  12218  ef0lem  12220  efgt0  12244  eftlub  12250  efsep  12251  effsumlt  12252  tanval3ap  12274  efi4p  12277  resin4p  12278  recos4p  12279  ef01bndlem  12316  sin01bnd  12317  cos01bnd  12318  sinltxirr  12321  sin01gt0  12322  cos01gt0  12323  absefib  12331  efieq1re  12332  eirraplem  12337  dvdsdc  12358  dvdscmulr  12380  fsumdvds  12402  dvdslelemd  12403  3dvds  12424  odd2np1lem  12432  odd2np1  12433  flodddiv4  12496  bitsfzo  12515  bitsmod  12516  gcdsupex  12527  gcdsupcl  12528  gcd1  12557  nninfctlemfo  12610  nn0seqcvgd  12612  algcvg  12619  algcvgblem  12620  eucalg  12630  prmind2  12691  qden1elz  12776  dfphi2  12791  phiprm  12794  phimullem  12796  prmdiv  12806  prmdiveq  12807  prm23lt5  12835  pcpre1  12864  pczpre  12869  pcdiv  12874  pc1  12877  pcqdiv  12879  pcexp  12881  pcxnn0cl  12882  pcxcl  12883  pcdvdstr  12899  pc2dvds  12902  sumhashdc  12919  fldivp1  12920  pcfaclem  12921  qexpz  12924  expnprm  12925  prmpwdvds  12927  pockthlem  12928  4sqlem5  12954  4sqlem6  12955  4sqlem11  12973  4sqlem13m  12975  4sqlem19  12981  oddennn  13012  xpct  13016  ennnfonelemj0  13021  ennnfonelemen  13041  ctinfomlemom  13047  omctfn  13063  restid  13332  prdsex  13351  prdsval  13355  prdsbaslemss  13356  prdsbas  13358  imasbas  13389  imasplusg  13390  imasmulr  13391  imasaddfnlemg  13396  xpscf  13429  igsumvalx  13471  gsumsplit1r  13480  gsumprval  13481  gsumfzz  13577  gsumfzcl  13581  prdsgrpd  13691  prdsinvgd  13692  mulgnngsum  13713  mulgnndir  13737  mulgneg2  13742  dvdsrmuld  14109  zsssubrg  14598  znval  14649  znle  14650  znbaslemnn  14652  znf1o  14664  znleval  14666  psrval  14679  restuni2  14900  cnrest2r  14960  lmfss  14967  lmres  14971  lmtopcnp  14973  ispsmet  15046  isxmet2d  15071  ismet2  15077  blfvalps  15108  blex  15110  xblss2  15128  reopnap  15269  divcnap  15288  climcncf  15307  cncfmpt2fcntop  15322  hovera  15370  limcdifap  15385  cnplimcim  15390  cnlimcim  15394  cnlimc  15395  cnlimci  15396  dvbss  15408  dvcnp2cntop  15422  dvcn  15423  dvaddxxbr  15424  dvmulxxbr  15425  dvexp  15434  dveflem  15449  plyval  15455  elply2  15458  plyf  15460  plyss  15461  plyssc  15462  elplyr  15463  plyaddlem1  15470  plymullem1  15471  plyaddlem  15472  plymullem  15473  plyco  15482  plycj  15484  dvply1  15488  reeff1olem  15494  sinperlem  15531  sin2kpi  15534  cos2kpi  15535  sin2pim  15536  cos2pim  15537  cosq14gt0  15555  coseq0q4123  15557  tangtx  15561  abssinper  15569  sinkpi  15570  coskpi  15571  cosq34lt1  15573  logrpap0b  15599  logdivlti  15604  rpcxpsqrtth  15653  rpabscxpbnd  15663  binom4  15702  wilthlem1  15703  0sgm  15708  1sgmprm  15717  1sgm2ppw  15718  mersenne  15720  perfect1  15721  perfectlem1  15722  perfectlem2  15723  perfect  15724  lgslem1  15728  lgsval  15732  lgsfvalg  15733  lgsfcl2  15734  lgsfcl  15736  lgsval2lem  15738  lgsvalmod  15747  lgsneg  15752  lgsdilem  15755  lgsdir2lem3  15758  lgsdir  15763  lgsdilem2  15764  lgsdi  15765  lgsne0  15766  lgsabs1  15767  lgsprme0  15770  lgsdirnn0  15775  lgsdinn0  15776  gausslemma2dlem0d  15780  gausslemma2dlem1a  15786  gausslemma2dlem1f1o  15788  gausslemma2dlem3  15791  gausslemma2dlem4  15792  gausslemma2dlem5a  15793  gausslemma2dlem5  15794  gausslemma2dlem6  15795  lgseisenlem2  15799  lgseisen  15802  lgsquadlem1  15805  lgsquadlem2  15806  lgsquad2lem1  15809  lgsquad2lem2  15810  lgsquad2  15811  m1lgs  15813  2lgslem1  15819  2lgslem2  15820  2lgs  15832  2sqlem9  15852  2sqlem10  15853  ushgredgedg  16076  ushgredgedgloop  16078  uhgrspansubgrlem  16126  wlkvtxiedg  16195  wlkvtxiedgg  16196  wlk1walkdom  16209  upgr2wlkdc  16227  clwwlkccatlem  16250  umgrclwwlkge2  16252  clwwlknonmpo  16278  clwwlknonex2lem2  16288  clwwlknonex2  16289  2omap  16594  pwle2  16599  pw1nct  16604  nninfsellemdc  16612  nnnninfen  16623  nnnninfex  16624  nninfnfiinf  16625  sbthom  16630  trirec0  16648  apdifflemr  16651  reap0  16662  nconstwlpolem  16669  gfsumval  16680