Theorem sylancl 411

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  413  sylanblrc  414  equveli  1752  sseqtrid  3197  ssdifin0  3496  uneqdifeqim  3500  unimax  3830  opth  4222  djussxp  4756  iss  4937  relresfld  5140  eldmrexrn  5637  f1oresrab  5661  fmptco  5662  fsn  5668  fnressn  5682  foima2  5731  foeqcnvco  5769  isoini2  5798  ofres  6075  ofco  6079  tposexg  6237  tfrlemisucaccv  6304  tfrlemibex  6308  tfri1dALT  6330  tfrcl  6343  rdgivallem  6360  frecabex  6377  frectfr  6379  frecrdg  6387  pmresg  6654  mapsn  6668  mapsncnv  6673  ixpsnf1o  6714  en1  6777  2dom  6783  enpr2d  6795  mapxpen  6826  phplem4  6833  fiintim  6906  sbthlem2  6935  elfir  6950  infglbti  7002  caseinl  7068  caseinr  7069  difinfsnlem  7076  difinfsn  7077  nninfisollemne  7107  exmidfodomrlemim  7178  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  archnqq  7379  prarloclemlt  7455  prarloclemlo  7456  prarloclemcalc  7464  recexprlemm  7586  recexprlemex  7599  caucvgprlemm  7630  caucvgprprlemmu  7657  suplocexprlem2b  7676  suplocexprlemmu  7680  suplocexprlemlub  7686  1idsr  7730  recexgt0sr  7735  archsr  7744  caucvgsrlemoffval  7758  caucvgsrlemofff  7759  caucvgsrlemoffres  7762  caucvgsr  7764  ltpsrprg  7765  suplocsrlem  7770  pitonnlem2  7809  pitonn  7810  pitoregt0  7811  pitore  7812  recnnre  7813  axrnegex  7841  nntopi  7856  msqge0  8535  mulge0  8538  recexaplem2  8570  recexap  8571  recgt0  8766  recreclt  8816  nn1m1nn  8896  nn1suc  8897  nnle1eq1  8902  nn1gt1  8912  nnsub  8917  addltmul  9114  nn0le0eq0  9163  elnn0nn  9177  elnnz  9222  elznn0  9227  zlem1lt  9268  zltlem1  9269  elz2  9283  nn0n0n1ge2b  9291  nn0lt2  9293  nn0le2is012  9294  eluzaddi  9513  eluzsubi  9514  uzp1  9520  peano2uzr  9544  nn01to3  9576  qreccl  9601  ltpnf  9737  xaddass2  9827  iccen  9963  fz01en  10009  fzpreddisj  10027  fzsuc2  10035  fseq1p1m1  10050  fseq1m1p1  10051  elfzp1b  10053  fzoss2  10128  fzval3  10160  fzosplitsnm1  10165  fzosplitprm1  10190  flhalf  10258  modqmulnn  10298  modqmuladdnn0  10324  frec2uzrand  10361  frecuzrdg0  10369  frecuzrdg0t  10378  frecfzennn  10382  frecfzen2  10383  uzennn  10392  seqeq1  10404  seq3m1  10424  monoord2  10433  ser3mono  10434  ser0f  10471  exp3vallem  10477  expm1t  10504  expeq0  10507  expubnd  10533  binom3  10593  facndiv  10673  facavg  10680  bcn0  10689  bcnp1n  10693  bcm1k  10694  bcp1nk  10696  bcval5  10697  bcn2  10698  bcp1m1  10699  bcpasc  10700  bcn2m1  10703  hashsng  10733  hashun  10740  hashfz  10756  hashfzo  10757  seq3coll  10777  shftfval  10785  2shfti  10795  resqrexlemf1  10972  abs00ap  11026  sqabs  11046  ltabs  11051  caubnd2  11081  max0addsup  11183  rexico  11185  mulcn2  11275  climaddc1  11292  climmulc2  11294  climsubc1  11295  climsubc2  11296  iserex  11302  climlec2  11304  iser3shft  11309  climcvg1nlem  11312  serf0  11315  sumrbdc  11342  fsumm1  11379  fsump1  11383  fsum00  11425  telfsumo  11429  fsumparts  11433  hashiun  11441  binomlem  11446  binom1dif  11450  bcxmas  11452  isumsplit  11454  isum1p  11455  arisum  11461  arisum2  11462  trireciplem  11463  explecnv  11468  geolim  11474  georeclim  11476  mertenslem2  11499  mertensabs  11500  prodf1f  11506  prodrbdclem2  11536  efcllemp  11621  ef0lem  11623  efgt0  11647  eftlub  11653  efsep  11654  effsumlt  11655  tanval3ap  11677  efi4p  11680  resin4p  11681  recos4p  11682  ef01bndlem  11719  sin01bnd  11720  cos01bnd  11721  sin01gt0  11724  cos01gt0  11725  absefib  11733  efieq1re  11734  eirraplem  11739  dvdsdc  11760  dvdscmulr  11782  dvdslelemd  11803  odd2np1lem  11831  odd2np1  11832  flodddiv4  11893  gcdsupex  11912  gcdsupcl  11913  gcd1  11942  nn0seqcvgd  11995  algcvg  12002  algcvgblem  12003  eucalg  12013  prmind2  12074  qden1elz  12159  dfphi2  12174  phiprm  12177  phimullem  12179  prmdiv  12189  prmdiveq  12190  prm23lt5  12217  pcpre1  12246  pczpre  12251  pcdiv  12256  pc1  12259  pcqdiv  12261  pcexp  12263  pcxnn0cl  12264  pcxcl  12265  pcdvdstr  12280  pc2dvds  12283  sumhashdc  12299  fldivp1  12300  pcfaclem  12301  qexpz  12304  expnprm  12305  prmpwdvds  12307  pockthlem  12308  4sqlem5  12334  4sqlem6  12335  oddennn  12347  xpct  12351  ennnfonelemj0  12356  ennnfonelemen  12376  ctinfomlemom  12382  omctfn  12398  restid  12590  restuni2  12971  cnrest2r  13031  lmfss  13038  lmres  13042  lmtopcnp  13044  ispsmet  13117  isxmet2d  13142  ismet2  13148  blfvalps  13179  blex  13181  xblss2  13199  reopnap  13332  divcnap  13349  climcncf  13365  cncfmpt2fcntop  13379  limcdifap  13425  cnplimcim  13430  cnlimcim  13434  cnlimc  13435  cnlimci  13436  dvbss  13448  dvcnp2cntop  13457  dvcn  13458  dvaddxxbr  13459  dvmulxxbr  13460  dvexp  13469  dveflem  13481  reeff1olem  13486  sinperlem  13523  sin2kpi  13526  cos2kpi  13527  sin2pim  13528  cos2pim  13529  cosq14gt0  13547  coseq0q4123  13549  tangtx  13553  abssinper  13561  sinkpi  13562  coskpi  13563  cosq34lt1  13565  logrpap0b  13591  logdivlti  13596  rpcxpsqrtth  13644  rpabscxpbnd  13653  binom4  13691  lgslem1  13695  lgsval  13699  lgsfvalg  13700  lgsfcl2  13701  lgsfcl  13703  lgsval2lem  13705  lgsvalmod  13714  lgsneg  13719  lgsdilem  13722  lgsdir2lem3  13725  lgsdir  13730  lgsdilem2  13731  lgsdi  13732  lgsne0  13733  lgsabs1  13734  lgsprme0  13737  lgsdirnn0  13742  lgsdinn0  13743  2sqlem9  13754  2sqlem10  13755  pwle2  14031  pw1nct  14036  nninfsellemdc  14043  sbthom  14058  trirec0  14076  apdifflemr  14079  reap0  14090  nconstwlpolem  14096