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  3207  ssdifin0  3506  uneqdifeqim  3510  unimax  3845  opth  4239  djussxp  4774  iss  4955  relresfld  5160  eldmrexrn  5659  f1oresrab  5683  fmptco  5684  fsn  5690  fnressn  5704  foima2  5754  foeqcnvco  5793  isoini2  5822  ofres  6099  ofco  6103  tposexg  6261  tfrlemisucaccv  6328  tfrlemibex  6332  tfri1dALT  6354  tfrcl  6367  rdgivallem  6384  frecabex  6401  frectfr  6403  frecrdg  6411  pmresg  6678  mapsn  6692  mapsncnv  6697  ixpsnf1o  6738  en1  6801  2dom  6807  enpr2d  6819  mapxpen  6850  phplem4  6857  fiintim  6930  sbthlem2  6959  elfir  6974  infglbti  7026  caseinl  7092  caseinr  7093  difinfsnlem  7100  difinfsn  7101  nninfisollemne  7131  exmidfodomrlemim  7202  exmidfodomrlemr  7203  exmidfodomrlemrALT  7204  2omotaplemap  7258  archnqq  7418  prarloclemlt  7494  prarloclemlo  7495  prarloclemcalc  7503  recexprlemm  7625  recexprlemex  7638  caucvgprlemm  7669  caucvgprprlemmu  7696  suplocexprlem2b  7715  suplocexprlemmu  7719  suplocexprlemlub  7725  1idsr  7769  recexgt0sr  7774  archsr  7783  caucvgsrlemoffval  7797  caucvgsrlemofff  7798  caucvgsrlemoffres  7801  caucvgsr  7803  ltpsrprg  7804  suplocsrlem  7809  pitonnlem2  7848  pitonn  7849  pitoregt0  7850  pitore  7851  recnnre  7852  axrnegex  7880  nntopi  7895  msqge0  8575  mulge0  8578  recexaplem2  8611  recexap  8612  recgt0  8809  recreclt  8859  nn1m1nn  8939  nn1suc  8940  nnle1eq1  8945  nn1gt1  8955  nnsub  8960  addltmul  9157  nn0le0eq0  9206  elnn0nn  9220  elnnz  9265  elznn0  9270  zlem1lt  9311  zltlem1  9312  elz2  9326  nn0n0n1ge2b  9334  nn0lt2  9336  nn0le2is012  9337  eluzaddi  9556  eluzsubi  9557  uzp1  9563  peano2uzr  9587  nn01to3  9619  qreccl  9644  ltpnf  9782  xaddass2  9872  iccen  10008  fz01en  10055  fzpreddisj  10073  fzsuc2  10081  fseq1p1m1  10096  fseq1m1p1  10097  elfzp1b  10099  fzoss2  10174  fzval3  10206  fzosplitsnm1  10211  fzosplitprm1  10236  flhalf  10304  modqmulnn  10344  modqmuladdnn0  10370  frec2uzrand  10407  frecuzrdg0  10415  frecuzrdg0t  10424  frecfzennn  10428  frecfzen2  10429  uzennn  10438  seqeq1  10450  seq3m1  10470  monoord2  10479  ser3mono  10480  ser0f  10517  exp3vallem  10523  expm1t  10550  expeq0  10553  expubnd  10579  binom3  10640  facndiv  10721  facavg  10728  bcn0  10737  bcnp1n  10741  bcm1k  10742  bcp1nk  10744  bcval5  10745  bcn2  10746  bcp1m1  10747  bcpasc  10748  bcn2m1  10751  hashsng  10780  hashun  10787  hashfz  10803  hashfzo  10804  seq3coll  10824  shftfval  10832  2shfti  10842  resqrexlemf1  11019  abs00ap  11073  sqabs  11093  ltabs  11098  caubnd2  11128  max0addsup  11230  rexico  11232  mulcn2  11322  climaddc1  11339  climmulc2  11341  climsubc1  11342  climsubc2  11343  iserex  11349  climlec2  11351  iser3shft  11356  climcvg1nlem  11359  serf0  11362  sumrbdc  11389  fsumm1  11426  fsump1  11430  fsum00  11472  telfsumo  11476  fsumparts  11480  hashiun  11488  binomlem  11493  binom1dif  11497  bcxmas  11499  isumsplit  11501  isum1p  11502  arisum  11508  arisum2  11509  trireciplem  11510  explecnv  11515  geolim  11521  georeclim  11523  mertenslem2  11546  mertensabs  11547  prodf1f  11553  prodrbdclem2  11583  efcllemp  11668  ef0lem  11670  efgt0  11694  eftlub  11700  efsep  11701  effsumlt  11702  tanval3ap  11724  efi4p  11727  resin4p  11728  recos4p  11729  ef01bndlem  11766  sin01bnd  11767  cos01bnd  11768  sin01gt0  11771  cos01gt0  11772  absefib  11780  efieq1re  11781  eirraplem  11786  dvdsdc  11807  dvdscmulr  11829  dvdslelemd  11851  odd2np1lem  11879  odd2np1  11880  flodddiv4  11941  gcdsupex  11960  gcdsupcl  11961  gcd1  11990  nn0seqcvgd  12043  algcvg  12050  algcvgblem  12051  eucalg  12061  prmind2  12122  qden1elz  12207  dfphi2  12222  phiprm  12225  phimullem  12227  prmdiv  12237  prmdiveq  12238  prm23lt5  12265  pcpre1  12294  pczpre  12299  pcdiv  12304  pc1  12307  pcqdiv  12309  pcexp  12311  pcxnn0cl  12312  pcxcl  12313  pcdvdstr  12328  pc2dvds  12331  sumhashdc  12347  fldivp1  12348  pcfaclem  12349  qexpz  12352  expnprm  12353  prmpwdvds  12355  pockthlem  12356  4sqlem5  12382  4sqlem6  12383  oddennn  12395  xpct  12399  ennnfonelemj0  12404  ennnfonelemen  12424  ctinfomlemom  12430  omctfn  12446  restid  12704  prdsex  12723  imasbas  12733  imasplusg  12734  imasmulr  12735  imasaddfnlemg  12740  xpscf  12771  mulgnndir  13017  mulgneg2  13022  dvdsrmuld  13270  zsssubrg  13518  restuni2  13716  cnrest2r  13776  lmfss  13783  lmres  13787  lmtopcnp  13789  ispsmet  13862  isxmet2d  13887  ismet2  13893  blfvalps  13924  blex  13926  xblss2  13944  reopnap  14077  divcnap  14094  climcncf  14110  cncfmpt2fcntop  14124  limcdifap  14170  cnplimcim  14175  cnlimcim  14179  cnlimc  14180  cnlimci  14181  dvbss  14193  dvcnp2cntop  14202  dvcn  14203  dvaddxxbr  14204  dvmulxxbr  14205  dvexp  14214  dveflem  14226  reeff1olem  14231  sinperlem  14268  sin2kpi  14271  cos2kpi  14272  sin2pim  14273  cos2pim  14274  cosq14gt0  14292  coseq0q4123  14294  tangtx  14298  abssinper  14306  sinkpi  14307  coskpi  14308  cosq34lt1  14310  logrpap0b  14336  logdivlti  14341  rpcxpsqrtth  14389  rpabscxpbnd  14398  binom4  14436  lgslem1  14440  lgsval  14444  lgsfvalg  14445  lgsfcl2  14446  lgsfcl  14448  lgsval2lem  14450  lgsvalmod  14459  lgsneg  14464  lgsdilem  14467  lgsdir2lem3  14470  lgsdir  14475  lgsdilem2  14476  lgsdi  14477  lgsne0  14478  lgsabs1  14479  lgsprme0  14482  lgsdirnn0  14487  lgsdinn0  14488  lgseisenlem2  14490  m1lgs  14491  2sqlem9  14510  2sqlem10  14511  pwle2  14787  pw1nct  14791  nninfsellemdc  14798  sbthom  14813  trirec0  14831  apdifflemr  14834  reap0  14845  nconstwlpolem  14852