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  1770  sseqtrid  3230  ssdifin0  3529  uneqdifeqim  3533  unimax  3870  opth  4267  djussxp  4808  iss  4989  relresfld  5196  eldmrexrn  5700  f1oresrab  5724  fmptco  5725  fsn  5731  fnressn  5745  foima2  5795  foeqcnvco  5834  isoini2  5863  ofres  6147  ofco  6151  tposexg  6313  tfrlemisucaccv  6380  tfrlemibex  6384  tfri1dALT  6406  tfrcl  6419  rdgivallem  6436  frecabex  6453  frectfr  6455  frecrdg  6463  pmresg  6732  mapsn  6746  mapsncnv  6751  ixpsnf1o  6792  en1  6855  2dom  6861  enpr2d  6873  mapxpen  6906  phplem4  6913  exmidpw2en  6970  fiintim  6987  sbthlem2  7019  elfir  7034  infglbti  7086  caseinl  7152  caseinr  7153  difinfsnlem  7160  difinfsn  7161  nninfisollemne  7192  exmidfodomrlemim  7263  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  2omotaplemap  7319  archnqq  7479  prarloclemlt  7555  prarloclemlo  7556  prarloclemcalc  7564  recexprlemm  7686  recexprlemex  7699  caucvgprlemm  7730  caucvgprprlemmu  7757  suplocexprlem2b  7776  suplocexprlemmu  7780  suplocexprlemlub  7786  1idsr  7830  recexgt0sr  7835  archsr  7844  caucvgsrlemoffval  7858  caucvgsrlemofff  7859  caucvgsrlemoffres  7862  caucvgsr  7864  ltpsrprg  7865  suplocsrlem  7870  pitonnlem2  7909  pitonn  7910  pitoregt0  7911  pitore  7912  recnnre  7913  axrnegex  7941  nntopi  7956  msqge0  8637  mulge0  8640  recexaplem2  8673  recexap  8674  recgt0  8871  recreclt  8921  nn1m1nn  9002  nn1suc  9003  nnle1eq1  9008  nn1gt1  9018  nnsub  9023  addltmul  9222  nn0le0eq0  9271  elnn0nn  9285  elnnz  9330  elznn0  9335  zlem1lt  9376  zltlem1  9377  elz2  9391  nn0n0n1ge2b  9399  nn0lt2  9401  nn0le2is012  9402  eluzaddi  9622  eluzsubi  9623  uzp1  9629  peano2uzr  9653  nn01to3  9685  qreccl  9710  irrmulap  9716  ltpnf  9849  xaddass2  9939  iccen  10075  fz01en  10122  fzpreddisj  10140  fzsuc2  10148  fseq1p1m1  10163  fseq1m1p1  10164  elfzp1b  10166  fzoss2  10242  fzval3  10274  fzosplitsnm1  10279  fzosplitprm1  10304  flhalf  10374  fldiv4lem1div2uz2  10378  modqmulnn  10416  modqmuladdnn0  10442  frec2uzrand  10479  frecuzrdg0  10487  frecuzrdg0t  10496  frecfzennn  10500  frecfzen2  10501  uzennn  10510  seqeq1  10524  seqp1g  10540  seqclg  10546  seq3m1  10547  monoord2  10560  ser3mono  10561  seqf1oglem1  10593  seqf1oglem2  10594  seqfeq4g  10605  ser0f  10608  exp3vallem  10614  expm1t  10641  expeq0  10644  expubnd  10670  binom3  10731  facndiv  10813  facavg  10820  bcn0  10829  bcnp1n  10833  bcm1k  10834  bcp1nk  10836  bcval5  10837  bcn2  10838  bcp1m1  10839  bcpasc  10840  bcn2m1  10843  hashsng  10872  hashun  10879  hashfz  10895  hashfzo  10896  seq3coll  10916  iswrdiz  10924  snopiswrd  10927  shftfval  10968  2shfti  10978  resqrexlemf1  11155  abs00ap  11209  sqabs  11229  ltabs  11234  caubnd2  11264  max0addsup  11366  rexico  11368  mulcn2  11458  climaddc1  11475  climmulc2  11477  climsubc1  11478  climsubc2  11479  iserex  11485  climlec2  11487  iser3shft  11492  climcvg1nlem  11495  serf0  11498  sumrbdc  11525  fsumm1  11562  fsump1  11566  fsum00  11608  telfsumo  11612  fsumparts  11616  hashiun  11624  binomlem  11629  binom1dif  11633  bcxmas  11635  isumsplit  11637  isum1p  11638  arisum  11644  arisum2  11645  trireciplem  11646  explecnv  11651  geolim  11657  georeclim  11659  mertenslem2  11682  mertensabs  11683  prodf1f  11689  prodrbdclem2  11719  efcllemp  11804  ef0lem  11806  efgt0  11830  eftlub  11836  efsep  11837  effsumlt  11838  tanval3ap  11860  efi4p  11863  resin4p  11864  recos4p  11865  ef01bndlem  11902  sin01bnd  11903  cos01bnd  11904  sinltxirr  11907  sin01gt0  11908  cos01gt0  11909  absefib  11917  efieq1re  11918  eirraplem  11923  dvdsdc  11944  dvdscmulr  11966  dvdslelemd  11988  odd2np1lem  12016  odd2np1  12017  flodddiv4  12078  gcdsupex  12097  gcdsupcl  12098  gcd1  12127  nninfctlemfo  12180  nn0seqcvgd  12182  algcvg  12189  algcvgblem  12190  eucalg  12200  prmind2  12261  qden1elz  12346  dfphi2  12361  phiprm  12364  phimullem  12366  prmdiv  12376  prmdiveq  12377  prm23lt5  12404  pcpre1  12433  pczpre  12438  pcdiv  12443  pc1  12446  pcqdiv  12448  pcexp  12450  pcxnn0cl  12451  pcxcl  12452  pcdvdstr  12468  pc2dvds  12471  sumhashdc  12488  fldivp1  12489  pcfaclem  12490  qexpz  12493  expnprm  12494  prmpwdvds  12496  pockthlem  12497  4sqlem5  12523  4sqlem6  12524  4sqlem11  12542  4sqlem13m  12544  4sqlem19  12550  oddennn  12552  xpct  12556  ennnfonelemj0  12561  ennnfonelemen  12581  ctinfomlemom  12587  omctfn  12603  restid  12864  prdsex  12883  imasbas  12893  imasplusg  12894  imasmulr  12895  imasaddfnlemg  12900  xpscf  12933  igsumvalx  12975  gsumsplit1r  12984  gsumprval  12985  gsumfzz  13070  gsumfzcl  13074  mulgnngsum  13200  mulgnndir  13224  mulgneg2  13229  dvdsrmuld  13595  zsssubrg  14084  znval  14135  znle  14136  znbaslemnn  14138  znf1o  14150  znleval  14152  psrval  14163  restuni2  14356  cnrest2r  14416  lmfss  14423  lmres  14427  lmtopcnp  14429  ispsmet  14502  isxmet2d  14527  ismet2  14533  blfvalps  14564  blex  14566  xblss2  14584  reopnap  14725  divcnap  14744  climcncf  14763  cncfmpt2fcntop  14778  hovera  14826  limcdifap  14841  cnplimcim  14846  cnlimcim  14850  cnlimc  14851  cnlimci  14852  dvbss  14864  dvcnp2cntop  14878  dvcn  14879  dvaddxxbr  14880  dvmulxxbr  14881  dvexp  14890  dveflem  14905  plyval  14911  elply2  14914  plyf  14916  plyss  14917  plyssc  14918  elplyr  14919  plyaddlem1  14926  plymullem1  14927  plyaddlem  14928  plymullem  14929  plyco  14937  plycj  14939  dvply1  14943  reeff1olem  14947  sinperlem  14984  sin2kpi  14987  cos2kpi  14988  sin2pim  14989  cos2pim  14990  cosq14gt0  15008  coseq0q4123  15010  tangtx  15014  abssinper  15022  sinkpi  15023  coskpi  15024  cosq34lt1  15026  logrpap0b  15052  logdivlti  15057  rpcxpsqrtth  15105  rpabscxpbnd  15114  binom4  15152  wilthlem1  15153  lgslem1  15157  lgsval  15161  lgsfvalg  15162  lgsfcl2  15163  lgsfcl  15165  lgsval2lem  15167  lgsvalmod  15176  lgsneg  15181  lgsdilem  15184  lgsdir2lem3  15187  lgsdir  15192  lgsdilem2  15193  lgsdi  15194  lgsne0  15195  lgsabs1  15196  lgsprme0  15199  lgsdirnn0  15204  lgsdinn0  15205  gausslemma2dlem0d  15209  gausslemma2dlem1a  15215  gausslemma2dlem1f1o  15217  gausslemma2dlem3  15220  gausslemma2dlem4  15221  gausslemma2dlem5a  15222  gausslemma2dlem5  15223  gausslemma2dlem6  15224  lgseisenlem2  15228  lgseisen  15231  lgsquadlem1  15234  lgsquadlem2  15235  lgsquad2lem1  15238  lgsquad2lem2  15239  lgsquad2  15240  m1lgs  15242  2lgslem1  15248  2lgslem2  15249  2lgs  15261  2sqlem9  15281  2sqlem10  15282  pwle2  15559  pw1nct  15563  nninfsellemdc  15570  nnnninfen  15581  sbthom  15586  trirec0  15604  apdifflemr  15607  reap0  15618  nconstwlpolem  15625