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  1805  sseqtrid  3275  ssdifin0  3574  uneqdifeqim  3578  unimax  3925  opth  4327  djussxp  4873  iss  5057  relresfld  5264  eldmrexrn  5784  f1oresrab  5808  fmptco  5809  fsn  5815  fnressn  5835  foima2  5887  foeqcnvco  5926  isoini2  5955  relmptopab  6219  ofres  6245  ofco  6249  tposexg  6419  tfrlemisucaccv  6486  tfrlemibex  6490  tfri1dALT  6512  tfrcl  6525  rdgivallem  6542  frecabex  6559  frectfr  6561  frecrdg  6569  pmresg  6840  mapsn  6854  mapsncnv  6859  ixpsnf1o  6900  en1  6968  2dom  6975  enpr2d  6992  en2  6993  mapxpen  7029  phplem4  7036  exmidpw2en  7097  fiintim  7116  sbthlem2  7148  elfir  7163  infglbti  7215  caseinl  7281  caseinr  7282  difinfsnlem  7289  difinfsn  7290  nninfisollemne  7321  exmidfodomrlemim  7402  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  2omotaplemap  7466  archnqq  7627  prarloclemlt  7703  prarloclemlo  7704  prarloclemcalc  7712  recexprlemm  7834  recexprlemex  7847  caucvgprlemm  7878  caucvgprprlemmu  7905  suplocexprlem2b  7924  suplocexprlemmu  7928  suplocexprlemlub  7934  1idsr  7978  recexgt0sr  7983  archsr  7992  caucvgsrlemoffval  8006  caucvgsrlemofff  8007  caucvgsrlemoffres  8010  caucvgsr  8012  ltpsrprg  8013  suplocsrlem  8018  pitonnlem2  8057  pitonn  8058  pitoregt0  8059  pitore  8060  recnnre  8061  axrnegex  8089  nntopi  8104  msqge0  8786  mulge0  8789  recexaplem2  8822  recexap  8823  recgt0  9020  recreclt  9070  nn1m1nn  9151  nn1suc  9152  nnle1eq1  9157  nn1gt1  9167  nnsub  9172  addltmul  9371  nn0le0eq0  9420  elnn0nn  9434  elnnz  9479  elznn0  9484  zlem1lt  9526  zltlem1  9527  elz2  9541  nn0n0n1ge2b  9549  nn0lt2  9551  nn0le2is012  9552  eluzaddi  9773  eluzsubi  9774  uzp1  9780  peano2uzr  9809  nn01to3  9841  qreccl  9866  irrmulap  9872  ltpnf  10005  xaddass2  10095  iccen  10231  fz01en  10278  fzpreddisj  10296  fzsuc2  10304  fseq1p1m1  10319  fseq1m1p1  10320  elfzp1b  10322  fzoss2  10399  fzval3  10439  fzosplitsnm1  10444  fzosplitprm1  10470  flhalf  10552  fldiv4lem1div2uz2  10556  modqmulnn  10594  modqmuladdnn0  10620  frec2uzrand  10657  frecuzrdg0  10665  frecuzrdg0t  10674  frecfzennn  10678  frecfzen2  10679  uzennn  10688  seqeq1  10702  seqp1g  10718  seqclg  10724  seq3m1  10725  monoord2  10738  ser3mono  10739  seqf1oglem1  10771  seqf1oglem2  10772  seqfeq4g  10783  ser0f  10786  exp3vallem  10792  expm1t  10819  expeq0  10822  expubnd  10848  binom3  10909  facndiv  10991  facavg  10998  bcn0  11007  bcnp1n  11011  bcm1k  11012  bcp1nk  11014  bcval5  11015  bcn2  11016  bcp1m1  11017  bcpasc  11018  bcn2m1  11021  hashsng  11050  hashun  11058  hashfz  11075  hashfzo  11076  seq3coll  11096  hash2en  11097  iswrdiz  11110  snopiswrd  11113  ccat1st1st  11208  swrds1  11239  cats1un  11292  wrdind  11293  wrd2ind  11294  swrdccatin1  11296  swrdccat3blem  11310  shftfval  11372  2shfti  11382  resqrexlemf1  11559  abs00ap  11613  sqabs  11633  ltabs  11638  caubnd2  11668  max0addsup  11770  rexico  11772  mulcn2  11863  climaddc1  11880  climmulc2  11882  climsubc1  11883  climsubc2  11884  iserex  11890  climlec2  11892  iser3shft  11897  climcvg1nlem  11900  serf0  11903  sumrbdc  11930  fsumm1  11967  fsump1  11971  fsum00  12013  telfsumo  12017  fsumparts  12021  hashiun  12029  binomlem  12034  binom1dif  12038  bcxmas  12040  isumsplit  12042  isum1p  12043  arisum  12049  arisum2  12050  trireciplem  12051  explecnv  12056  geolim  12062  georeclim  12064  mertenslem2  12087  mertensabs  12088  prodf1f  12094  prodrbdclem2  12124  efcllemp  12209  ef0lem  12211  efgt0  12235  eftlub  12241  efsep  12242  effsumlt  12243  tanval3ap  12265  efi4p  12268  resin4p  12269  recos4p  12270  ef01bndlem  12307  sin01bnd  12308  cos01bnd  12309  sinltxirr  12312  sin01gt0  12313  cos01gt0  12314  absefib  12322  efieq1re  12323  eirraplem  12328  dvdsdc  12349  dvdscmulr  12371  fsumdvds  12393  dvdslelemd  12394  3dvds  12415  odd2np1lem  12423  odd2np1  12424  flodddiv4  12487  bitsfzo  12506  bitsmod  12507  gcdsupex  12518  gcdsupcl  12519  gcd1  12548  nninfctlemfo  12601  nn0seqcvgd  12603  algcvg  12610  algcvgblem  12611  eucalg  12621  prmind2  12682  qden1elz  12767  dfphi2  12782  phiprm  12785  phimullem  12787  prmdiv  12797  prmdiveq  12798  prm23lt5  12826  pcpre1  12855  pczpre  12860  pcdiv  12865  pc1  12868  pcqdiv  12870  pcexp  12872  pcxnn0cl  12873  pcxcl  12874  pcdvdstr  12890  pc2dvds  12893  sumhashdc  12910  fldivp1  12911  pcfaclem  12912  qexpz  12915  expnprm  12916  prmpwdvds  12918  pockthlem  12919  4sqlem5  12945  4sqlem6  12946  4sqlem11  12964  4sqlem13m  12966  4sqlem19  12972  oddennn  13003  xpct  13007  ennnfonelemj0  13012  ennnfonelemen  13032  ctinfomlemom  13038  omctfn  13054  restid  13323  prdsex  13342  prdsval  13346  prdsbaslemss  13347  prdsbas  13349  imasbas  13380  imasplusg  13381  imasmulr  13382  imasaddfnlemg  13387  xpscf  13420  igsumvalx  13462  gsumsplit1r  13471  gsumprval  13472  gsumfzz  13568  gsumfzcl  13572  prdsgrpd  13682  prdsinvgd  13683  mulgnngsum  13704  mulgnndir  13728  mulgneg2  13733  dvdsrmuld  14100  zsssubrg  14589  znval  14640  znle  14641  znbaslemnn  14643  znf1o  14655  znleval  14657  psrval  14670  restuni2  14891  cnrest2r  14951  lmfss  14958  lmres  14962  lmtopcnp  14964  ispsmet  15037  isxmet2d  15062  ismet2  15068  blfvalps  15099  blex  15101  xblss2  15119  reopnap  15260  divcnap  15279  climcncf  15298  cncfmpt2fcntop  15313  hovera  15361  limcdifap  15376  cnplimcim  15381  cnlimcim  15385  cnlimc  15386  cnlimci  15387  dvbss  15399  dvcnp2cntop  15413  dvcn  15414  dvaddxxbr  15415  dvmulxxbr  15416  dvexp  15425  dveflem  15440  plyval  15446  elply2  15449  plyf  15451  plyss  15452  plyssc  15453  elplyr  15454  plyaddlem1  15461  plymullem1  15462  plyaddlem  15463  plymullem  15464  plyco  15473  plycj  15475  dvply1  15479  reeff1olem  15485  sinperlem  15522  sin2kpi  15525  cos2kpi  15526  sin2pim  15527  cos2pim  15528  cosq14gt0  15546  coseq0q4123  15548  tangtx  15552  abssinper  15560  sinkpi  15561  coskpi  15562  cosq34lt1  15564  logrpap0b  15590  logdivlti  15595  rpcxpsqrtth  15644  rpabscxpbnd  15654  binom4  15693  wilthlem1  15694  0sgm  15699  1sgmprm  15708  1sgm2ppw  15709  mersenne  15711  perfect1  15712  perfectlem1  15713  perfectlem2  15714  perfect  15715  lgslem1  15719  lgsval  15723  lgsfvalg  15724  lgsfcl2  15725  lgsfcl  15727  lgsval2lem  15729  lgsvalmod  15738  lgsneg  15743  lgsdilem  15746  lgsdir2lem3  15749  lgsdir  15754  lgsdilem2  15755  lgsdi  15756  lgsne0  15757  lgsabs1  15758  lgsprme0  15761  lgsdirnn0  15766  lgsdinn0  15767  gausslemma2dlem0d  15771  gausslemma2dlem1a  15777  gausslemma2dlem1f1o  15779  gausslemma2dlem3  15782  gausslemma2dlem4  15783  gausslemma2dlem5a  15784  gausslemma2dlem5  15785  gausslemma2dlem6  15786  lgseisenlem2  15790  lgseisen  15793  lgsquadlem1  15796  lgsquadlem2  15797  lgsquad2lem1  15800  lgsquad2lem2  15801  lgsquad2  15802  m1lgs  15804  2lgslem1  15810  2lgslem2  15811  2lgs  15823  2sqlem9  15843  2sqlem10  15844  ushgredgedg  16065  ushgredgedgloop  16067  wlkvtxiedg  16142  wlkvtxiedgg  16143  wlk1walkdom  16156  upgr2wlkdc  16172  clwwlkccatlem  16195  umgrclwwlkge2  16197  clwwlknonmpo  16223  clwwlknonex2lem2  16233  clwwlknonex2  16234  2omap  16530  pwle2  16535  pw1nct  16540  nninfsellemdc  16548  nnnninfen  16559  nnnninfex  16560  nninfnfiinf  16561  sbthom  16566  trirec0  16584  apdifflemr  16587  reap0  16598  nconstwlpolem  16605