Theorem sylancl 410

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 409	1 |- ( ph -> th )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107

This theorem is referenced by:  sylanblc  412  sylanblrc  413  equveli  1747  sseqtrid  3191  ssdifin0  3489  uneqdifeqim  3493  unimax  3822  opth  4214  djussxp  4748  iss  4929  relresfld  5132  eldmrexrn  5625  f1oresrab  5649  fmptco  5650  fsn  5656  fnressn  5670  foima2  5719  foeqcnvco  5757  isoini2  5786  ofres  6063  ofco  6067  tposexg  6222  tfrlemisucaccv  6289  tfrlemibex  6293  tfri1dALT  6315  tfrcl  6328  rdgivallem  6345  frecabex  6362  frectfr  6364  frecrdg  6372  pmresg  6638  mapsn  6652  mapsncnv  6657  ixpsnf1o  6698  en1  6761  2dom  6767  enpr2d  6779  mapxpen  6810  phplem4  6817  fiintim  6890  sbthlem2  6919  elfir  6934  infglbti  6986  caseinl  7052  caseinr  7053  difinfsnlem  7060  difinfsn  7061  nninfisollemne  7091  exmidfodomrlemim  7153  exmidfodomrlemr  7154  exmidfodomrlemrALT  7155  archnqq  7354  prarloclemlt  7430  prarloclemlo  7431  prarloclemcalc  7439  recexprlemm  7561  recexprlemex  7574  caucvgprlemm  7605  caucvgprprlemmu  7632  suplocexprlem2b  7651  suplocexprlemmu  7655  suplocexprlemlub  7661  1idsr  7705  recexgt0sr  7710  archsr  7719  caucvgsrlemoffval  7733  caucvgsrlemofff  7734  caucvgsrlemoffres  7737  caucvgsr  7739  ltpsrprg  7740  suplocsrlem  7745  pitonnlem2  7784  pitonn  7785  pitoregt0  7786  pitore  7787  recnnre  7788  axrnegex  7816  nntopi  7831  msqge0  8510  mulge0  8513  recexaplem2  8545  recexap  8546  recgt0  8741  recreclt  8791  nn1m1nn  8871  nn1suc  8872  nnle1eq1  8877  nn1gt1  8887  nnsub  8892  addltmul  9089  nn0le0eq0  9138  elnn0nn  9152  elnnz  9197  elznn0  9202  zlem1lt  9243  zltlem1  9244  elz2  9258  nn0n0n1ge2b  9266  nn0lt2  9268  nn0le2is012  9269  eluzaddi  9488  eluzsubi  9489  uzp1  9495  peano2uzr  9519  nn01to3  9551  qreccl  9576  ltpnf  9712  xaddass2  9802  iccen  9938  fz01en  9984  fzpreddisj  10002  fzsuc2  10010  fseq1p1m1  10025  fseq1m1p1  10026  elfzp1b  10028  fzoss2  10103  fzval3  10135  fzosplitsnm1  10140  fzosplitprm1  10165  flhalf  10233  modqmulnn  10273  modqmuladdnn0  10299  frec2uzrand  10336  frecuzrdg0  10344  frecuzrdg0t  10353  frecfzennn  10357  frecfzen2  10358  uzennn  10367  seqeq1  10379  seq3m1  10399  monoord2  10408  ser3mono  10409  ser0f  10446  exp3vallem  10452  expm1t  10479  expeq0  10482  expubnd  10508  binom3  10568  facndiv  10648  facavg  10655  bcn0  10664  bcnp1n  10668  bcm1k  10669  bcp1nk  10671  bcval5  10672  bcn2  10673  bcp1m1  10674  bcpasc  10675  bcn2m1  10678  hashsng  10707  hashun  10714  hashfz  10730  hashfzo  10731  seq3coll  10751  shftfval  10759  2shfti  10769  resqrexlemf1  10946  abs00ap  11000  sqabs  11020  ltabs  11025  caubnd2  11055  max0addsup  11157  rexico  11159  mulcn2  11249  climaddc1  11266  climmulc2  11268  climsubc1  11269  climsubc2  11270  iserex  11276  climlec2  11278  iser3shft  11283  climcvg1nlem  11286  serf0  11289  sumrbdc  11316  fsumm1  11353  fsump1  11357  fsum00  11399  telfsumo  11403  fsumparts  11407  hashiun  11415  binomlem  11420  binom1dif  11424  bcxmas  11426  isumsplit  11428  isum1p  11429  arisum  11435  arisum2  11436  trireciplem  11437  explecnv  11442  geolim  11448  georeclim  11450  mertenslem2  11473  mertensabs  11474  prodf1f  11480  prodrbdclem2  11510  efcllemp  11595  ef0lem  11597  efgt0  11621  eftlub  11627  efsep  11628  effsumlt  11629  tanval3ap  11651  efi4p  11654  resin4p  11655  recos4p  11656  ef01bndlem  11693  sin01bnd  11694  cos01bnd  11695  sin01gt0  11698  cos01gt0  11699  absefib  11707  efieq1re  11708  eirraplem  11713  dvdsdc  11734  dvdscmulr  11756  dvdslelemd  11777  odd2np1lem  11805  odd2np1  11806  flodddiv4  11867  gcdsupex  11886  gcdsupcl  11887  gcd1  11916  nn0seqcvgd  11969  algcvg  11976  algcvgblem  11977  eucalg  11987  prmind2  12048  qden1elz  12133  dfphi2  12148  phiprm  12151  phimullem  12153  prmdiv  12163  prmdiveq  12164  prm23lt5  12191  pcpre1  12220  pczpre  12225  pcdiv  12230  pc1  12233  pcqdiv  12235  pcexp  12237  pcxnn0cl  12238  pcxcl  12239  pcdvdstr  12254  pc2dvds  12257  sumhashdc  12273  fldivp1  12274  pcfaclem  12275  qexpz  12278  expnprm  12279  prmpwdvds  12281  pockthlem  12282  4sqlem5  12308  4sqlem6  12309  oddennn  12321  xpct  12325  ennnfonelemj0  12330  ennnfonelemen  12350  ctinfomlemom  12356  omctfn  12372  restid  12562  restuni2  12777  cnrest2r  12837  lmfss  12844  lmres  12848  lmtopcnp  12850  ispsmet  12923  isxmet2d  12948  ismet2  12954  blfvalps  12985  blex  12987  xblss2  13005  reopnap  13138  divcnap  13155  climcncf  13171  cncfmpt2fcntop  13185  limcdifap  13231  cnplimcim  13236  cnlimcim  13240  cnlimc  13241  cnlimci  13242  dvbss  13254  dvcnp2cntop  13263  dvcn  13264  dvaddxxbr  13265  dvmulxxbr  13266  dvexp  13275  dveflem  13287  reeff1olem  13292  sinperlem  13329  sin2kpi  13332  cos2kpi  13333  sin2pim  13334  cos2pim  13335  cosq14gt0  13353  coseq0q4123  13355  tangtx  13359  abssinper  13367  sinkpi  13368  coskpi  13369  cosq34lt1  13371  logrpap0b  13397  logdivlti  13402  rpcxpsqrtth  13450  rpabscxpbnd  13459  binom4  13497  lgslem1  13501  lgsval  13505  lgsfvalg  13506  lgsfcl2  13507  lgsfcl  13509  lgsval2lem  13511  lgsvalmod  13520  lgsneg  13525  lgsdilem  13528  lgsdir2lem3  13531  lgsdir  13536  lgsdilem2  13537  lgsdi  13538  lgsne0  13539  lgsabs1  13540  lgsprme0  13543  lgsdirnn0  13548  lgsdinn0  13549  2sqlem9  13560  2sqlem10  13561  pwle2  13838  pw1nct  13843  nninfsellemdc  13850  sbthom  13865  trirec0  13883  apdifflemr  13886  reap0  13897  nconstwlpolem  13903