Theorem sylancl 417

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 415	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  419  sylanblrc  420  equveli  1812  sseqtrid  3298  ssdifin0  3606  uneqdifeqim  3610  unimax  3964  opth  4372  djussxp  4920  iss  5104  relresfld  5312  eldmrexrn  5840  f1oresrab  5864  fmptco  5865  fsn  5871  fnressn  5892  foima2  5947  foeqcnvco  5986  isoini2  6015  relmptopab  6281  ofres  6307  ofco  6311  suppval1  6469  suppimacnvfn  6476  tposexg  6519  tfrlemisucaccv  6586  tfrlemibex  6590  tfri1dALT  6612  tfrcl  6625  rdgivallem  6642  frecabex  6659  frectfr  6661  frecrdg  6669  pmresg  6947  mapsnd  6960  mapsn  6962  mapsncnv  6967  ixpsnf1o  7008  en1  7076  2dom  7083  mapsnend  7089  enpr2d  7101  en2  7102  mapxpen  7138  mapunen  7141  phplem4  7146  exmidpw2en  7209  fiintim  7228  sbthlem2  7265  elfir  7297  2omap  7308  infglbti  7355  caseinl  7421  caseinr  7422  difinfsnlem  7429  difinfsn  7430  nninfisollemne  7461  exmidfodomrlemim  7543  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  2omotaplemap  7613  archnqq  7774  prarloclemlt  7850  prarloclemlo  7851  prarloclemcalc  7859  recexprlemm  7981  recexprlemex  7994  caucvgprlemm  8025  caucvgprprlemmu  8052  suplocexprlem2b  8071  suplocexprlemmu  8075  suplocexprlemlub  8081  1idsr  8125  recexgt0sr  8130  archsr  8139  caucvgsrlemoffval  8153  caucvgsrlemofff  8154  caucvgsrlemoffres  8157  caucvgsr  8159  ltpsrprg  8160  suplocsrlem  8165  pitonnlem2  8204  pitonn  8205  pitoregt0  8206  pitore  8207  recnnre  8208  axrnegex  8236  nntopi  8251  msqge0  8934  mulge0  8937  recexaplem2  8970  recexap  8971  recgt0  9170  recreclt  9220  nn1m1nn  9301  nn1suc  9302  nnle1eq1  9307  nn1gt1  9317  nnsub  9322  addltmul  9521  nn0le0eq0  9570  elnn0nn  9584  elnnz  9633  elznn0  9638  zlem1lt  9680  zltlem1  9681  elz2  9695  nn0n0n1ge2b  9704  nn0lt2  9706  nn0le2is012  9707  eluzaddi  9928  eluzsubi  9929  uzp1  9935  peano2uzr  9964  nn01to3  9996  qreccl  10021  irrmulap  10027  ltpnf  10161  xaddass2  10251  iccen  10388  fz01en  10437  fzpreddisj  10456  fzsuc2  10464  fseq1p1m1  10479  fseq1m1p1  10480  elfzp1b  10482  fzoss2  10559  fzval3  10600  fzosplitsnm1  10605  fzosplitprm1  10631  flhalf  10715  fldiv4lem1div2uz2  10719  modqmulnn  10757  modqmuladdnn0  10783  frec2uzrand  10820  frecuzrdg0  10828  frecuzrdg0t  10837  frecfzennn  10841  frecfzen2  10842  uzennn  10851  seqeq1  10865  seqp1g  10881  seqclg  10887  seq3m1  10888  monoord2  10901  ser3mono  10902  seqf1oglem1  10934  seqf1oglem2  10935  seqfeq4g  10946  ser0f  10949  exp3vallem  10955  expm1t  10982  expeq0  10985  expubnd  11011  binom3  11072  facndiv  11155  facavg  11162  bcn0  11171  bcnp1n  11175  bcm1k  11176  bcp1nk  11178  bcval5  11179  bcn2  11180  bcp1m1  11181  bcpasc  11182  bcn2m1  11186  hashsng  11215  hashun  11223  hashfz  11240  hashfzo  11241  hashmap  11246  hashfibclem  11260  hashf1lem1  11263  hashf1  11265  seq3coll  11272  hash2en  11273  iswrdiz  11289  snopiswrd  11292  ccat1st1st  11387  swrds1  11418  cats1un  11471  wrdind  11472  wrd2ind  11473  swrdccatin1  11475  swrdccat3blem  11489  shftfval  11564  2shfti  11574  resqrexlemf1  11752  abs00ap  11806  sqabs  11826  ltabs  11831  caubnd2  11861  max0addsup  11963  rexico  11965  mulcn2  12056  climaddc1  12073  climmulc2  12075  climsubc1  12076  climsubc2  12077  iserex  12083  climlec2  12085  iser3shft  12090  climcvg1nlem  12093  serf0  12096  sumrbdc  12124  fsumm1  12161  fsump1  12165  fsum00  12207  telfsumo  12211  fsumparts  12215  hashiun  12223  binomlem  12228  binom1dif  12232  bcxmas  12234  isumsplit  12236  isum1p  12237  arisum  12243  arisum2  12244  trireciplem  12245  explecnv  12250  geolim  12256  georeclim  12258  mertenslem2  12281  mertensabs  12282  prodf1f  12288  prodrbdclem2  12318  efcllemp  12403  ef0lem  12405  efgt0  12429  eftlub  12435  efsep  12436  effsumlt  12437  tanval3ap  12459  efi4p  12462  resin4p  12463  recos4p  12464  ef01bndlem  12501  sin01bnd  12502  cos01bnd  12503  sinltxirr  12506  sin01gt0  12507  cos01gt0  12508  absefib  12516  efieq1re  12517  eirraplem  12522  dvdsdc  12543  dvdscmulr  12565  fsumdvds  12587  dvdslelemd  12588  3dvds  12609  odd2np1lem  12617  odd2np1  12618  flodddiv4  12681  bitsfzo  12700  bitsmod  12701  gcdsupex  12712  gcdsupcl  12713  gcd1  12742  nninfctlemfo  12795  nn0seqcvgd  12797  algcvg  12804  algcvgblem  12805  eucalg  12815  prmind2  12876  qden1elz  12961  dfphi2  12976  phiprm  12979  phimullem  12981  prmdiv  12991  prmdiveq  12992  prm23lt5  13020  pcpre1  13049  pczpre  13054  pcdiv  13059  pc1  13062  pcqdiv  13064  pcexp  13066  pcxnn0cl  13067  pcxcl  13068  pcdvdstr  13084  pc2dvds  13087  sumhashdc  13104  fldivp1  13105  pcfaclem  13106  qexpz  13109  expnprm  13110  prmpwdvds  13112  pockthlem  13113  4sqlem5  13139  4sqlem6  13140  4sqlem11  13158  4sqlem13m  13160  4sqlem19  13166  ballotfilemofi  13197  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilemodife  13218  ballotfilemscl  13225  ballotfilemsle  13226  oddennn  13261  xpct  13265  ennnfonelemj0  13270  ennnfonelemen  13290  ctinfomlemom  13296  omctfn  13312  restid  13581  imasbas  13605  imasplusg  13606  imasmulr  13607  imasaddfnlemg  13612  xpscf  13645  gzsumvalx  13686  gzsumsplit1r  13692  gzsumcl  13781  mulgnngzsum  13907  mulgnndir  13931  mulgneg2  13936  gsumvalfi  14129  prdsex  14149  prdsval  14150  prdsbaslemss  14151  prdsbas  14153  prdsgrpd  14174  prdsinvgd  14175  dvdsrmuld  14376  zsssubrg  14894  znval  14943  znle  14944  znbaslemnn  14946  znf1o  14958  znleval  14960  psrval  14973  restuni2  15201  cnrest2r  15261  lmfss  15268  lmres  15272  lmtopcnp  15274  ispsmet  15347  isxmet2d  15372  ismet2  15378  blfvalps  15409  blex  15411  xblss2  15429  reopnap  15570  divcnap  15589  climcncf  15608  cncfmpt2fcntop  15623  hovera  15671  limcdifap  15686  cnplimcim  15691  cnlimcim  15695  cnlimc  15696  cnlimci  15697  dvbss  15709  dvcnp2cntop  15723  dvcn  15724  dvaddxxbr  15725  dvmulxxbr  15726  dvexp  15735  dveflem  15750  plyval  15756  elply2  15759  plyf  15761  plyss  15762  plyssc  15763  elplyr  15764  plyaddlem1  15771  plymullem1  15772  plyaddlem  15773  plymullem  15774  plyco  15783  plycj  15785  dvply1  15789  reeff1olem  15795  sinperlem  15832  sin2kpi  15835  cos2kpi  15836  sin2pim  15837  cos2pim  15838  cosq14gt0  15856  coseq0q4123  15858  tangtx  15862  abssinper  15870  sinkpi  15871  coskpi  15872  cosq34lt1  15874  logrpap0b  15900  logdivlti  15905  rpcxpsqrtth  15955  rpabscxpbnd  15965  binom4  16004  wilthlem1  16008  0sgm  16013  1sgmprm  16022  1sgm2ppw  16023  mersenne  16025  perfect1  16026  perfectlem1  16027  perfectlem2  16028  perfect  16029  lgslem1  16033  lgsval  16037  lgsfvalg  16038  lgsfcl2  16039  lgsfcl  16041  lgsval2lem  16043  lgsvalmod  16052  lgsneg  16057  lgsdilem  16060  lgsdir2lem3  16063  lgsdir  16068  lgsdilem2  16069  lgsdi  16070  lgsne0  16071  lgsabs1  16072  lgsprme0  16075  lgsdirnn0  16080  lgsdinn0  16081  gausslemma2dlem0d  16085  gausslemma2dlem1a  16091  gausslemma2dlem1f1o  16093  gausslemma2dlem3  16096  gausslemma2dlem4  16097  gausslemma2dlem5a  16098  gausslemma2dlem5  16099  gausslemma2dlem6  16100  lgseisenlem2  16104  lgseisen  16107  lgsquadlem1  16110  lgsquadlem2  16111  lgsquad2lem1  16114  lgsquad2lem2  16115  lgsquad2  16116  m1lgs  16118  2lgslem1  16124  2lgslem2  16125  2lgs  16137  2sqlem9  16157  2sqlem10  16158  ushgredgedg  16381  ushgredgedgloop  16383  uhgrspansubgrlem  16431  wlkvtxiedg  16500  wlkvtxiedgg  16501  wlk1walkdom  16514  upgr2wlkdc  16532  clwwlkccatlem  16555  umgrclwwlkge2  16557  clwwlknonmpo  16583  clwwlknonex2lem2  16593  clwwlknonex2  16594  konigsberglem1  16643  pwle2  16942  pw1nct  16947  nninfsellemdc  16958  nnnninfen  16969  nnnninfex  16970  nninfnfiinf  16971  sbthom  16976  repiecelem  16979  repiecele0  16980  trirec0  16998  apdifflemr  17001  reap0  17013  nconstwlpolem  17020