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  1773  sseqtrid  3234  ssdifin0  3533  uneqdifeqim  3537  unimax  3874  opth  4271  djussxp  4812  iss  4993  relresfld  5200  eldmrexrn  5706  f1oresrab  5730  fmptco  5731  fsn  5737  fnressn  5751  foima2  5801  foeqcnvco  5840  isoini2  5869  ofres  6154  ofco  6158  tposexg  6325  tfrlemisucaccv  6392  tfrlemibex  6396  tfri1dALT  6418  tfrcl  6431  rdgivallem  6448  frecabex  6465  frectfr  6467  frecrdg  6475  pmresg  6744  mapsn  6758  mapsncnv  6763  ixpsnf1o  6804  en1  6867  2dom  6873  enpr2d  6885  mapxpen  6918  phplem4  6925  exmidpw2en  6982  fiintim  7001  sbthlem2  7033  elfir  7048  infglbti  7100  caseinl  7166  caseinr  7167  difinfsnlem  7174  difinfsn  7175  nninfisollemne  7206  exmidfodomrlemim  7282  exmidfodomrlemr  7283  exmidfodomrlemrALT  7284  2omotaplemap  7342  archnqq  7503  prarloclemlt  7579  prarloclemlo  7580  prarloclemcalc  7588  recexprlemm  7710  recexprlemex  7723  caucvgprlemm  7754  caucvgprprlemmu  7781  suplocexprlem2b  7800  suplocexprlemmu  7804  suplocexprlemlub  7810  1idsr  7854  recexgt0sr  7859  archsr  7868  caucvgsrlemoffval  7882  caucvgsrlemofff  7883  caucvgsrlemoffres  7886  caucvgsr  7888  ltpsrprg  7889  suplocsrlem  7894  pitonnlem2  7933  pitonn  7934  pitoregt0  7935  pitore  7936  recnnre  7937  axrnegex  7965  nntopi  7980  msqge0  8662  mulge0  8665  recexaplem2  8698  recexap  8699  recgt0  8896  recreclt  8946  nn1m1nn  9027  nn1suc  9028  nnle1eq1  9033  nn1gt1  9043  nnsub  9048  addltmul  9247  nn0le0eq0  9296  elnn0nn  9310  elnnz  9355  elznn0  9360  zlem1lt  9401  zltlem1  9402  elz2  9416  nn0n0n1ge2b  9424  nn0lt2  9426  nn0le2is012  9427  eluzaddi  9647  eluzsubi  9648  uzp1  9654  peano2uzr  9678  nn01to3  9710  qreccl  9735  irrmulap  9741  ltpnf  9874  xaddass2  9964  iccen  10100  fz01en  10147  fzpreddisj  10165  fzsuc2  10173  fseq1p1m1  10188  fseq1m1p1  10189  elfzp1b  10191  fzoss2  10267  fzval3  10299  fzosplitsnm1  10304  fzosplitprm1  10329  flhalf  10411  fldiv4lem1div2uz2  10415  modqmulnn  10453  modqmuladdnn0  10479  frec2uzrand  10516  frecuzrdg0  10524  frecuzrdg0t  10533  frecfzennn  10537  frecfzen2  10538  uzennn  10547  seqeq1  10561  seqp1g  10577  seqclg  10583  seq3m1  10584  monoord2  10597  ser3mono  10598  seqf1oglem1  10630  seqf1oglem2  10631  seqfeq4g  10642  ser0f  10645  exp3vallem  10651  expm1t  10678  expeq0  10681  expubnd  10707  binom3  10768  facndiv  10850  facavg  10857  bcn0  10866  bcnp1n  10870  bcm1k  10871  bcp1nk  10873  bcval5  10874  bcn2  10875  bcp1m1  10876  bcpasc  10877  bcn2m1  10880  hashsng  10909  hashun  10916  hashfz  10932  hashfzo  10933  seq3coll  10953  iswrdiz  10961  snopiswrd  10964  shftfval  11005  2shfti  11015  resqrexlemf1  11192  abs00ap  11246  sqabs  11266  ltabs  11271  caubnd2  11301  max0addsup  11403  rexico  11405  mulcn2  11496  climaddc1  11513  climmulc2  11515  climsubc1  11516  climsubc2  11517  iserex  11523  climlec2  11525  iser3shft  11530  climcvg1nlem  11533  serf0  11536  sumrbdc  11563  fsumm1  11600  fsump1  11604  fsum00  11646  telfsumo  11650  fsumparts  11654  hashiun  11662  binomlem  11667  binom1dif  11671  bcxmas  11673  isumsplit  11675  isum1p  11676  arisum  11682  arisum2  11683  trireciplem  11684  explecnv  11689  geolim  11695  georeclim  11697  mertenslem2  11720  mertensabs  11721  prodf1f  11727  prodrbdclem2  11757  efcllemp  11842  ef0lem  11844  efgt0  11868  eftlub  11874  efsep  11875  effsumlt  11876  tanval3ap  11898  efi4p  11901  resin4p  11902  recos4p  11903  ef01bndlem  11940  sin01bnd  11941  cos01bnd  11942  sinltxirr  11945  sin01gt0  11946  cos01gt0  11947  absefib  11955  efieq1re  11956  eirraplem  11961  dvdsdc  11982  dvdscmulr  12004  fsumdvds  12026  dvdslelemd  12027  3dvds  12048  odd2np1lem  12056  odd2np1  12057  flodddiv4  12120  bitsfzo  12139  bitsmod  12140  gcdsupex  12151  gcdsupcl  12152  gcd1  12181  nninfctlemfo  12234  nn0seqcvgd  12236  algcvg  12243  algcvgblem  12244  eucalg  12254  prmind2  12315  qden1elz  12400  dfphi2  12415  phiprm  12418  phimullem  12420  prmdiv  12430  prmdiveq  12431  prm23lt5  12459  pcpre1  12488  pczpre  12493  pcdiv  12498  pc1  12501  pcqdiv  12503  pcexp  12505  pcxnn0cl  12506  pcxcl  12507  pcdvdstr  12523  pc2dvds  12526  sumhashdc  12543  fldivp1  12544  pcfaclem  12545  qexpz  12548  expnprm  12549  prmpwdvds  12551  pockthlem  12552  4sqlem5  12578  4sqlem6  12579  4sqlem11  12597  4sqlem13m  12599  4sqlem19  12605  oddennn  12636  xpct  12640  ennnfonelemj0  12645  ennnfonelemen  12665  ctinfomlemom  12671  omctfn  12687  restid  12954  prdsex  12973  prdsval  12977  prdsbaslemss  12978  prdsbas  12980  imasbas  13011  imasplusg  13012  imasmulr  13013  imasaddfnlemg  13018  xpscf  13051  igsumvalx  13093  gsumsplit1r  13102  gsumprval  13103  gsumfzz  13199  gsumfzcl  13203  prdsgrpd  13313  prdsinvgd  13314  mulgnngsum  13335  mulgnndir  13359  mulgneg2  13364  dvdsrmuld  13730  zsssubrg  14219  znval  14270  znle  14271  znbaslemnn  14273  znf1o  14285  znleval  14287  psrval  14300  restuni2  14521  cnrest2r  14581  lmfss  14588  lmres  14592  lmtopcnp  14594  ispsmet  14667  isxmet2d  14692  ismet2  14698  blfvalps  14729  blex  14731  xblss2  14749  reopnap  14890  divcnap  14909  climcncf  14928  cncfmpt2fcntop  14943  hovera  14991  limcdifap  15006  cnplimcim  15011  cnlimcim  15015  cnlimc  15016  cnlimci  15017  dvbss  15029  dvcnp2cntop  15043  dvcn  15044  dvaddxxbr  15045  dvmulxxbr  15046  dvexp  15055  dveflem  15070  plyval  15076  elply2  15079  plyf  15081  plyss  15082  plyssc  15083  elplyr  15084  plyaddlem1  15091  plymullem1  15092  plyaddlem  15093  plymullem  15094  plyco  15103  plycj  15105  dvply1  15109  reeff1olem  15115  sinperlem  15152  sin2kpi  15155  cos2kpi  15156  sin2pim  15157  cos2pim  15158  cosq14gt0  15176  coseq0q4123  15178  tangtx  15182  abssinper  15190  sinkpi  15191  coskpi  15192  cosq34lt1  15194  logrpap0b  15220  logdivlti  15225  rpcxpsqrtth  15274  rpabscxpbnd  15284  binom4  15323  wilthlem1  15324  0sgm  15329  1sgmprm  15338  1sgm2ppw  15339  mersenne  15341  perfect1  15342  perfectlem1  15343  perfectlem2  15344  perfect  15345  lgslem1  15349  lgsval  15353  lgsfvalg  15354  lgsfcl2  15355  lgsfcl  15357  lgsval2lem  15359  lgsvalmod  15368  lgsneg  15373  lgsdilem  15376  lgsdir2lem3  15379  lgsdir  15384  lgsdilem2  15385  lgsdi  15386  lgsne0  15387  lgsabs1  15388  lgsprme0  15391  lgsdirnn0  15396  lgsdinn0  15397  gausslemma2dlem0d  15401  gausslemma2dlem1a  15407  gausslemma2dlem1f1o  15409  gausslemma2dlem3  15412  gausslemma2dlem4  15413  gausslemma2dlem5a  15414  gausslemma2dlem5  15415  gausslemma2dlem6  15416  lgseisenlem2  15420  lgseisen  15423  lgsquadlem1  15426  lgsquadlem2  15427  lgsquad2lem1  15430  lgsquad2lem2  15431  lgsquad2  15432  m1lgs  15434  2lgslem1  15440  2lgslem2  15441  2lgs  15453  2sqlem9  15473  2sqlem10  15474  2omap  15750  pwle2  15753  pw1nct  15758  nninfsellemdc  15765  nnnninfen  15776  nnnninfex  15777  nninfnfiinf  15778  sbthom  15783  trirec0  15801  apdifflemr  15804  reap0  15815  nconstwlpolem  15822