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  1769  sseqtrid  3217  ssdifin0  3516  uneqdifeqim  3520  unimax  3855  opth  4249  djussxp  4784  iss  4965  relresfld  5170  eldmrexrn  5670  f1oresrab  5694  fmptco  5695  fsn  5701  fnressn  5715  foima2  5765  foeqcnvco  5804  isoini2  5833  ofres  6111  ofco  6115  tposexg  6273  tfrlemisucaccv  6340  tfrlemibex  6344  tfri1dALT  6366  tfrcl  6379  rdgivallem  6396  frecabex  6413  frectfr  6415  frecrdg  6423  pmresg  6690  mapsn  6704  mapsncnv  6709  ixpsnf1o  6750  en1  6813  2dom  6819  enpr2d  6831  mapxpen  6862  phplem4  6869  fiintim  6942  sbthlem2  6971  elfir  6986  infglbti  7038  caseinl  7104  caseinr  7105  difinfsnlem  7112  difinfsn  7113  nninfisollemne  7143  exmidfodomrlemim  7214  exmidfodomrlemr  7215  exmidfodomrlemrALT  7216  2omotaplemap  7270  archnqq  7430  prarloclemlt  7506  prarloclemlo  7507  prarloclemcalc  7515  recexprlemm  7637  recexprlemex  7650  caucvgprlemm  7681  caucvgprprlemmu  7708  suplocexprlem2b  7727  suplocexprlemmu  7731  suplocexprlemlub  7737  1idsr  7781  recexgt0sr  7786  archsr  7795  caucvgsrlemoffval  7809  caucvgsrlemofff  7810  caucvgsrlemoffres  7813  caucvgsr  7815  ltpsrprg  7816  suplocsrlem  7821  pitonnlem2  7860  pitonn  7861  pitoregt0  7862  pitore  7863  recnnre  7864  axrnegex  7892  nntopi  7907  msqge0  8587  mulge0  8590  recexaplem2  8623  recexap  8624  recgt0  8821  recreclt  8871  nn1m1nn  8951  nn1suc  8952  nnle1eq1  8957  nn1gt1  8967  nnsub  8972  addltmul  9169  nn0le0eq0  9218  elnn0nn  9232  elnnz  9277  elznn0  9282  zlem1lt  9323  zltlem1  9324  elz2  9338  nn0n0n1ge2b  9346  nn0lt2  9348  nn0le2is012  9349  eluzaddi  9568  eluzsubi  9569  uzp1  9575  peano2uzr  9599  nn01to3  9631  qreccl  9656  ltpnf  9794  xaddass2  9884  iccen  10020  fz01en  10067  fzpreddisj  10085  fzsuc2  10093  fseq1p1m1  10108  fseq1m1p1  10109  elfzp1b  10111  fzoss2  10186  fzval3  10218  fzosplitsnm1  10223  fzosplitprm1  10248  flhalf  10316  modqmulnn  10356  modqmuladdnn0  10382  frec2uzrand  10419  frecuzrdg0  10427  frecuzrdg0t  10436  frecfzennn  10440  frecfzen2  10441  uzennn  10450  seqeq1  10462  seq3m1  10482  monoord2  10491  ser3mono  10492  ser0f  10529  exp3vallem  10535  expm1t  10562  expeq0  10565  expubnd  10591  binom3  10652  facndiv  10733  facavg  10740  bcn0  10749  bcnp1n  10753  bcm1k  10754  bcp1nk  10756  bcval5  10757  bcn2  10758  bcp1m1  10759  bcpasc  10760  bcn2m1  10763  hashsng  10792  hashun  10799  hashfz  10815  hashfzo  10816  seq3coll  10836  shftfval  10844  2shfti  10854  resqrexlemf1  11031  abs00ap  11085  sqabs  11105  ltabs  11110  caubnd2  11140  max0addsup  11242  rexico  11244  mulcn2  11334  climaddc1  11351  climmulc2  11353  climsubc1  11354  climsubc2  11355  iserex  11361  climlec2  11363  iser3shft  11368  climcvg1nlem  11371  serf0  11374  sumrbdc  11401  fsumm1  11438  fsump1  11442  fsum00  11484  telfsumo  11488  fsumparts  11492  hashiun  11500  binomlem  11505  binom1dif  11509  bcxmas  11511  isumsplit  11513  isum1p  11514  arisum  11520  arisum2  11521  trireciplem  11522  explecnv  11527  geolim  11533  georeclim  11535  mertenslem2  11558  mertensabs  11559  prodf1f  11565  prodrbdclem2  11595  efcllemp  11680  ef0lem  11682  efgt0  11706  eftlub  11712  efsep  11713  effsumlt  11714  tanval3ap  11736  efi4p  11739  resin4p  11740  recos4p  11741  ef01bndlem  11778  sin01bnd  11779  cos01bnd  11780  sin01gt0  11783  cos01gt0  11784  absefib  11792  efieq1re  11793  eirraplem  11798  dvdsdc  11819  dvdscmulr  11841  dvdslelemd  11863  odd2np1lem  11891  odd2np1  11892  flodddiv4  11953  gcdsupex  11972  gcdsupcl  11973  gcd1  12002  nn0seqcvgd  12055  algcvg  12062  algcvgblem  12063  eucalg  12073  prmind2  12134  qden1elz  12219  dfphi2  12234  phiprm  12237  phimullem  12239  prmdiv  12249  prmdiveq  12250  prm23lt5  12277  pcpre1  12306  pczpre  12311  pcdiv  12316  pc1  12319  pcqdiv  12321  pcexp  12323  pcxnn0cl  12324  pcxcl  12325  pcdvdstr  12340  pc2dvds  12343  sumhashdc  12359  fldivp1  12360  pcfaclem  12361  qexpz  12364  expnprm  12365  prmpwdvds  12367  pockthlem  12368  4sqlem5  12394  4sqlem6  12395  oddennn  12407  xpct  12411  ennnfonelemj0  12416  ennnfonelemen  12436  ctinfomlemom  12442  omctfn  12458  restid  12717  prdsex  12736  imasbas  12746  imasplusg  12747  imasmulr  12748  imasaddfnlemg  12753  xpscf  12785  mulgnndir  13052  mulgneg2  13057  dvdsrmuld  13401  zsssubrg  13818  restuni2  14030  cnrest2r  14090  lmfss  14097  lmres  14101  lmtopcnp  14103  ispsmet  14176  isxmet2d  14201  ismet2  14207  blfvalps  14238  blex  14240  xblss2  14258  reopnap  14391  divcnap  14408  climcncf  14424  cncfmpt2fcntop  14438  limcdifap  14484  cnplimcim  14489  cnlimcim  14493  cnlimc  14494  cnlimci  14495  dvbss  14507  dvcnp2cntop  14516  dvcn  14517  dvaddxxbr  14518  dvmulxxbr  14519  dvexp  14528  dveflem  14540  reeff1olem  14545  sinperlem  14582  sin2kpi  14585  cos2kpi  14586  sin2pim  14587  cos2pim  14588  cosq14gt0  14606  coseq0q4123  14608  tangtx  14612  abssinper  14620  sinkpi  14621  coskpi  14622  cosq34lt1  14624  logrpap0b  14650  logdivlti  14655  rpcxpsqrtth  14703  rpabscxpbnd  14712  binom4  14750  lgslem1  14754  lgsval  14758  lgsfvalg  14759  lgsfcl2  14760  lgsfcl  14762  lgsval2lem  14764  lgsvalmod  14773  lgsneg  14778  lgsdilem  14781  lgsdir2lem3  14784  lgsdir  14789  lgsdilem2  14790  lgsdi  14791  lgsne0  14792  lgsabs1  14793  lgsprme0  14796  lgsdirnn0  14801  lgsdinn0  14802  lgseisenlem2  14804  m1lgs  14805  2sqlem9  14824  2sqlem10  14825  pwle2  15102  pw1nct  15106  nninfsellemdc  15113  sbthom  15128  trirec0  15146  apdifflemr  15149  reap0  15160  nconstwlpolem  15167