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  1759  sseqtrid  3205  ssdifin0  3504  uneqdifeqim  3508  unimax  3843  opth  4237  djussxp  4772  iss  4953  relresfld  5158  eldmrexrn  5657  f1oresrab  5681  fmptco  5682  fsn  5688  fnressn  5702  foima2  5752  foeqcnvco  5790  isoini2  5819  ofres  6096  ofco  6100  tposexg  6258  tfrlemisucaccv  6325  tfrlemibex  6329  tfri1dALT  6351  tfrcl  6364  rdgivallem  6381  frecabex  6398  frectfr  6400  frecrdg  6408  pmresg  6675  mapsn  6689  mapsncnv  6694  ixpsnf1o  6735  en1  6798  2dom  6804  enpr2d  6816  mapxpen  6847  phplem4  6854  fiintim  6927  sbthlem2  6956  elfir  6971  infglbti  7023  caseinl  7089  caseinr  7090  difinfsnlem  7097  difinfsn  7098  nninfisollemne  7128  exmidfodomrlemim  7199  exmidfodomrlemr  7200  exmidfodomrlemrALT  7201  2omotaplemap  7255  archnqq  7415  prarloclemlt  7491  prarloclemlo  7492  prarloclemcalc  7500  recexprlemm  7622  recexprlemex  7635  caucvgprlemm  7666  caucvgprprlemmu  7693  suplocexprlem2b  7712  suplocexprlemmu  7716  suplocexprlemlub  7722  1idsr  7766  recexgt0sr  7771  archsr  7780  caucvgsrlemoffval  7794  caucvgsrlemofff  7795  caucvgsrlemoffres  7798  caucvgsr  7800  ltpsrprg  7801  suplocsrlem  7806  pitonnlem2  7845  pitonn  7846  pitoregt0  7847  pitore  7848  recnnre  7849  axrnegex  7877  nntopi  7892  msqge0  8572  mulge0  8575  recexaplem2  8608  recexap  8609  recgt0  8806  recreclt  8856  nn1m1nn  8936  nn1suc  8937  nnle1eq1  8942  nn1gt1  8952  nnsub  8957  addltmul  9154  nn0le0eq0  9203  elnn0nn  9217  elnnz  9262  elznn0  9267  zlem1lt  9308  zltlem1  9309  elz2  9323  nn0n0n1ge2b  9331  nn0lt2  9333  nn0le2is012  9334  eluzaddi  9553  eluzsubi  9554  uzp1  9560  peano2uzr  9584  nn01to3  9616  qreccl  9641  ltpnf  9779  xaddass2  9869  iccen  10005  fz01en  10052  fzpreddisj  10070  fzsuc2  10078  fseq1p1m1  10093  fseq1m1p1  10094  elfzp1b  10096  fzoss2  10171  fzval3  10203  fzosplitsnm1  10208  fzosplitprm1  10233  flhalf  10301  modqmulnn  10341  modqmuladdnn0  10367  frec2uzrand  10404  frecuzrdg0  10412  frecuzrdg0t  10421  frecfzennn  10425  frecfzen2  10426  uzennn  10435  seqeq1  10447  seq3m1  10467  monoord2  10476  ser3mono  10477  ser0f  10514  exp3vallem  10520  expm1t  10547  expeq0  10550  expubnd  10576  binom3  10637  facndiv  10718  facavg  10725  bcn0  10734  bcnp1n  10738  bcm1k  10739  bcp1nk  10741  bcval5  10742  bcn2  10743  bcp1m1  10744  bcpasc  10745  bcn2m1  10748  hashsng  10777  hashun  10784  hashfz  10800  hashfzo  10801  seq3coll  10821  shftfval  10829  2shfti  10839  resqrexlemf1  11016  abs00ap  11070  sqabs  11090  ltabs  11095  caubnd2  11125  max0addsup  11227  rexico  11229  mulcn2  11319  climaddc1  11336  climmulc2  11338  climsubc1  11339  climsubc2  11340  iserex  11346  climlec2  11348  iser3shft  11353  climcvg1nlem  11356  serf0  11359  sumrbdc  11386  fsumm1  11423  fsump1  11427  fsum00  11469  telfsumo  11473  fsumparts  11477  hashiun  11485  binomlem  11490  binom1dif  11494  bcxmas  11496  isumsplit  11498  isum1p  11499  arisum  11505  arisum2  11506  trireciplem  11507  explecnv  11512  geolim  11518  georeclim  11520  mertenslem2  11543  mertensabs  11544  prodf1f  11550  prodrbdclem2  11580  efcllemp  11665  ef0lem  11667  efgt0  11691  eftlub  11697  efsep  11698  effsumlt  11699  tanval3ap  11721  efi4p  11724  resin4p  11725  recos4p  11726  ef01bndlem  11763  sin01bnd  11764  cos01bnd  11765  sin01gt0  11768  cos01gt0  11769  absefib  11777  efieq1re  11778  eirraplem  11783  dvdsdc  11804  dvdscmulr  11826  dvdslelemd  11848  odd2np1lem  11876  odd2np1  11877  flodddiv4  11938  gcdsupex  11957  gcdsupcl  11958  gcd1  11987  nn0seqcvgd  12040  algcvg  12047  algcvgblem  12048  eucalg  12058  prmind2  12119  qden1elz  12204  dfphi2  12219  phiprm  12222  phimullem  12224  prmdiv  12234  prmdiveq  12235  prm23lt5  12262  pcpre1  12291  pczpre  12296  pcdiv  12301  pc1  12304  pcqdiv  12306  pcexp  12308  pcxnn0cl  12309  pcxcl  12310  pcdvdstr  12325  pc2dvds  12328  sumhashdc  12344  fldivp1  12345  pcfaclem  12346  qexpz  12349  expnprm  12350  prmpwdvds  12352  pockthlem  12353  4sqlem5  12379  4sqlem6  12380  oddennn  12392  xpct  12396  ennnfonelemj0  12401  ennnfonelemen  12421  ctinfomlemom  12427  omctfn  12443  restid  12698  prdsex  12717  imasbas  12727  imasplusg  12728  imasmulr  12729  imasaddfnlemg  12734  xpscf  12765  mulgnndir  13010  mulgneg2  13015  dvdsrmuld  13263  zsssubrg  13449  restuni2  13647  cnrest2r  13707  lmfss  13714  lmres  13718  lmtopcnp  13720  ispsmet  13793  isxmet2d  13818  ismet2  13824  blfvalps  13855  blex  13857  xblss2  13875  reopnap  14008  divcnap  14025  climcncf  14041  cncfmpt2fcntop  14055  limcdifap  14101  cnplimcim  14106  cnlimcim  14110  cnlimc  14111  cnlimci  14112  dvbss  14124  dvcnp2cntop  14133  dvcn  14134  dvaddxxbr  14135  dvmulxxbr  14136  dvexp  14145  dveflem  14157  reeff1olem  14162  sinperlem  14199  sin2kpi  14202  cos2kpi  14203  sin2pim  14204  cos2pim  14205  cosq14gt0  14223  coseq0q4123  14225  tangtx  14229  abssinper  14237  sinkpi  14238  coskpi  14239  cosq34lt1  14241  logrpap0b  14267  logdivlti  14272  rpcxpsqrtth  14320  rpabscxpbnd  14329  binom4  14367  lgslem1  14371  lgsval  14375  lgsfvalg  14376  lgsfcl2  14377  lgsfcl  14379  lgsval2lem  14381  lgsvalmod  14390  lgsneg  14395  lgsdilem  14398  lgsdir2lem3  14401  lgsdir  14406  lgsdilem2  14407  lgsdi  14408  lgsne0  14409  lgsabs1  14410  lgsprme0  14413  lgsdirnn0  14418  lgsdinn0  14419  lgseisenlem2  14421  m1lgs  14422  2sqlem9  14441  2sqlem10  14442  pwle2  14718  pw1nct  14722  nninfsellemdc  14729  sbthom  14744  trirec0  14762  apdifflemr  14765  reap0  14776  nconstwlpolem  14782