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  1782  sseqtrid  3243  ssdifin0  3542  uneqdifeqim  3546  unimax  3884  opth  4282  djussxp  4824  iss  5006  relresfld  5213  eldmrexrn  5723  f1oresrab  5747  fmptco  5748  fsn  5754  fnressn  5772  foima2  5822  foeqcnvco  5861  isoini2  5890  ofres  6175  ofco  6179  tposexg  6346  tfrlemisucaccv  6413  tfrlemibex  6417  tfri1dALT  6439  tfrcl  6452  rdgivallem  6469  frecabex  6486  frectfr  6488  frecrdg  6496  pmresg  6765  mapsn  6779  mapsncnv  6784  ixpsnf1o  6825  en1  6893  2dom  6899  enpr2d  6913  en2  6914  mapxpen  6947  phplem4  6954  exmidpw2en  7011  fiintim  7030  sbthlem2  7062  elfir  7077  infglbti  7129  caseinl  7195  caseinr  7196  difinfsnlem  7203  difinfsn  7204  nninfisollemne  7235  exmidfodomrlemim  7311  exmidfodomrlemr  7312  exmidfodomrlemrALT  7313  2omotaplemap  7371  archnqq  7532  prarloclemlt  7608  prarloclemlo  7609  prarloclemcalc  7617  recexprlemm  7739  recexprlemex  7752  caucvgprlemm  7783  caucvgprprlemmu  7810  suplocexprlem2b  7829  suplocexprlemmu  7833  suplocexprlemlub  7839  1idsr  7883  recexgt0sr  7888  archsr  7897  caucvgsrlemoffval  7911  caucvgsrlemofff  7912  caucvgsrlemoffres  7915  caucvgsr  7917  ltpsrprg  7918  suplocsrlem  7923  pitonnlem2  7962  pitonn  7963  pitoregt0  7964  pitore  7965  recnnre  7966  axrnegex  7994  nntopi  8009  msqge0  8691  mulge0  8694  recexaplem2  8727  recexap  8728  recgt0  8925  recreclt  8975  nn1m1nn  9056  nn1suc  9057  nnle1eq1  9062  nn1gt1  9072  nnsub  9077  addltmul  9276  nn0le0eq0  9325  elnn0nn  9339  elnnz  9384  elznn0  9389  zlem1lt  9431  zltlem1  9432  elz2  9446  nn0n0n1ge2b  9454  nn0lt2  9456  nn0le2is012  9457  eluzaddi  9677  eluzsubi  9678  uzp1  9684  peano2uzr  9708  nn01to3  9740  qreccl  9765  irrmulap  9771  ltpnf  9904  xaddass2  9994  iccen  10130  fz01en  10177  fzpreddisj  10195  fzsuc2  10203  fseq1p1m1  10218  fseq1m1p1  10219  elfzp1b  10221  fzoss2  10298  fzval3  10335  fzosplitsnm1  10340  fzosplitprm1  10365  flhalf  10447  fldiv4lem1div2uz2  10451  modqmulnn  10489  modqmuladdnn0  10515  frec2uzrand  10552  frecuzrdg0  10560  frecuzrdg0t  10569  frecfzennn  10573  frecfzen2  10574  uzennn  10583  seqeq1  10597  seqp1g  10613  seqclg  10619  seq3m1  10620  monoord2  10633  ser3mono  10634  seqf1oglem1  10666  seqf1oglem2  10667  seqfeq4g  10678  ser0f  10681  exp3vallem  10687  expm1t  10714  expeq0  10717  expubnd  10743  binom3  10804  facndiv  10886  facavg  10893  bcn0  10902  bcnp1n  10906  bcm1k  10907  bcp1nk  10909  bcval5  10910  bcn2  10911  bcp1m1  10912  bcpasc  10913  bcn2m1  10916  hashsng  10945  hashun  10952  hashfz  10968  hashfzo  10969  seq3coll  10989  hash2en  10990  iswrdiz  11003  snopiswrd  11006  ccat1st1st  11096  swrds1  11124  shftfval  11165  2shfti  11175  resqrexlemf1  11352  abs00ap  11406  sqabs  11426  ltabs  11431  caubnd2  11461  max0addsup  11563  rexico  11565  mulcn2  11656  climaddc1  11673  climmulc2  11675  climsubc1  11676  climsubc2  11677  iserex  11683  climlec2  11685  iser3shft  11690  climcvg1nlem  11693  serf0  11696  sumrbdc  11723  fsumm1  11760  fsump1  11764  fsum00  11806  telfsumo  11810  fsumparts  11814  hashiun  11822  binomlem  11827  binom1dif  11831  bcxmas  11833  isumsplit  11835  isum1p  11836  arisum  11842  arisum2  11843  trireciplem  11844  explecnv  11849  geolim  11855  georeclim  11857  mertenslem2  11880  mertensabs  11881  prodf1f  11887  prodrbdclem2  11917  efcllemp  12002  ef0lem  12004  efgt0  12028  eftlub  12034  efsep  12035  effsumlt  12036  tanval3ap  12058  efi4p  12061  resin4p  12062  recos4p  12063  ef01bndlem  12100  sin01bnd  12101  cos01bnd  12102  sinltxirr  12105  sin01gt0  12106  cos01gt0  12107  absefib  12115  efieq1re  12116  eirraplem  12121  dvdsdc  12142  dvdscmulr  12164  fsumdvds  12186  dvdslelemd  12187  3dvds  12208  odd2np1lem  12216  odd2np1  12217  flodddiv4  12280  bitsfzo  12299  bitsmod  12300  gcdsupex  12311  gcdsupcl  12312  gcd1  12341  nninfctlemfo  12394  nn0seqcvgd  12396  algcvg  12403  algcvgblem  12404  eucalg  12414  prmind2  12475  qden1elz  12560  dfphi2  12575  phiprm  12578  phimullem  12580  prmdiv  12590  prmdiveq  12591  prm23lt5  12619  pcpre1  12648  pczpre  12653  pcdiv  12658  pc1  12661  pcqdiv  12663  pcexp  12665  pcxnn0cl  12666  pcxcl  12667  pcdvdstr  12683  pc2dvds  12686  sumhashdc  12703  fldivp1  12704  pcfaclem  12705  qexpz  12708  expnprm  12709  prmpwdvds  12711  pockthlem  12712  4sqlem5  12738  4sqlem6  12739  4sqlem11  12757  4sqlem13m  12759  4sqlem19  12765  oddennn  12796  xpct  12800  ennnfonelemj0  12805  ennnfonelemen  12825  ctinfomlemom  12831  omctfn  12847  restid  13115  prdsex  13134  prdsval  13138  prdsbaslemss  13139  prdsbas  13141  imasbas  13172  imasplusg  13173  imasmulr  13174  imasaddfnlemg  13179  xpscf  13212  igsumvalx  13254  gsumsplit1r  13263  gsumprval  13264  gsumfzz  13360  gsumfzcl  13364  prdsgrpd  13474  prdsinvgd  13475  mulgnngsum  13496  mulgnndir  13520  mulgneg2  13525  dvdsrmuld  13891  zsssubrg  14380  znval  14431  znle  14432  znbaslemnn  14434  znf1o  14446  znleval  14448  psrval  14461  restuni2  14682  cnrest2r  14742  lmfss  14749  lmres  14753  lmtopcnp  14755  ispsmet  14828  isxmet2d  14853  ismet2  14859  blfvalps  14890  blex  14892  xblss2  14910  reopnap  15051  divcnap  15070  climcncf  15089  cncfmpt2fcntop  15104  hovera  15152  limcdifap  15167  cnplimcim  15172  cnlimcim  15176  cnlimc  15177  cnlimci  15178  dvbss  15190  dvcnp2cntop  15204  dvcn  15205  dvaddxxbr  15206  dvmulxxbr  15207  dvexp  15216  dveflem  15231  plyval  15237  elply2  15240  plyf  15242  plyss  15243  plyssc  15244  elplyr  15245  plyaddlem1  15252  plymullem1  15253  plyaddlem  15254  plymullem  15255  plyco  15264  plycj  15266  dvply1  15270  reeff1olem  15276  sinperlem  15313  sin2kpi  15316  cos2kpi  15317  sin2pim  15318  cos2pim  15319  cosq14gt0  15337  coseq0q4123  15339  tangtx  15343  abssinper  15351  sinkpi  15352  coskpi  15353  cosq34lt1  15355  logrpap0b  15381  logdivlti  15386  rpcxpsqrtth  15435  rpabscxpbnd  15445  binom4  15484  wilthlem1  15485  0sgm  15490  1sgmprm  15499  1sgm2ppw  15500  mersenne  15502  perfect1  15503  perfectlem1  15504  perfectlem2  15505  perfect  15506  lgslem1  15510  lgsval  15514  lgsfvalg  15515  lgsfcl2  15516  lgsfcl  15518  lgsval2lem  15520  lgsvalmod  15529  lgsneg  15534  lgsdilem  15537  lgsdir2lem3  15540  lgsdir  15545  lgsdilem2  15546  lgsdi  15547  lgsne0  15548  lgsabs1  15549  lgsprme0  15552  lgsdirnn0  15557  lgsdinn0  15558  gausslemma2dlem0d  15562  gausslemma2dlem1a  15568  gausslemma2dlem1f1o  15570  gausslemma2dlem3  15573  gausslemma2dlem4  15574  gausslemma2dlem5a  15575  gausslemma2dlem5  15576  gausslemma2dlem6  15577  lgseisenlem2  15581  lgseisen  15584  lgsquadlem1  15587  lgsquadlem2  15588  lgsquad2lem1  15591  lgsquad2lem2  15592  lgsquad2  15593  m1lgs  15595  2lgslem1  15601  2lgslem2  15602  2lgs  15614  2sqlem9  15634  2sqlem10  15635  2omap  15969  pwle2  15972  pw1nct  15977  nninfsellemdc  15984  nnnninfen  15995  nnnninfex  15996  nninfnfiinf  15997  sbthom  16002  trirec0  16020  apdifflemr  16023  reap0  16034  nconstwlpolem  16041