Theorem sylan 283

Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)

Hypotheses

Ref	Expression
sylan.1	|- ( ph -> ps )
sylan.2	|- ( ( ps /\ ch ) -> th )

Assertion

Ref	Expression
sylan	|- ( ( ph /\ ch ) -> th )

Proof of Theorem sylan

Step	Hyp	Ref	Expression
1		sylan.1	. 2 |- ( ph -> ps )
2		sylan.2	. . 3 |- ( ( ps /\ ch ) -> th )
3	2	expcom 116	. 2 |- ( ch -> ( ps -> th ) )
4	1, 3	mpan9 281	1 |- ( ( ph /\ ch ) -> th )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  sylanb  284  sylanbr  285  syl2an  289  sylanl1  402  sylanl2  403  mpanl1  434  mpanl2  435  syldanl  449  adantll  476  adantlr  477  ancom1s  569  pm4.55dc  940  3adantl1  1155  3adantl2  1156  3adantl3  1157  syl3anl1  1297  syl3anl3  1299  syl3anl  1300  stoic3  1442  eupick  2124  csbiebt  3124  csbnestgf  3137  reuss2  3444  mpteq12  4117  otexg  4264  opelopabt  4297  sonr  4353  sotr  4354  issod  4355  so2nr  4357  so3nr  4358  ordelss  4415  onelon  4420  elrnmpt1s  4917  iota2  5249  funeu  5284  imadif  5339  fnbr  5361  feu  5441  f1ss  5470  f1ssres  5473  f1resf1  5474  dffo2  5485  foco  5492  foun  5524  fun11iun  5526  ffoss  5537  funbrfv  5600  fvco3  5633  fvopab6  5659  funfvbrb  5676  elpreima  5682  ffvelcdm  5696  ffvelcdmda  5698  dffo4  5711  fmptco  5729  fsn2  5737  fvconst2g  5777  fex  5792  funfvima  5795  f1elima  5821  f1ocnvfv1  5825  f1ocnvfv2  5826  cocan2  5836  foeqcnvco  5838  isocnv  5859  isores2  5861  isoini  5866  isoselem  5868  f1oiso  5874  f1ofveu  5911  eloprabga  6010  suppssof1  6154  ofco  6155  offveqb  6156  ofc1g  6157  ofc2g  6158  fnexALT  6169  f1dmex  6174  ot1stg  6211  ot2ndg  6212  ot3rdgg  6213  eqopi  6231  2ndrn  6242  fo2ndf  6286  smores3  6352  smores2  6353  smoel  6359  smoiso  6361  tfrlem1  6367  tfrlemisucaccv  6384  tfrlemibxssdm  6386  tfrlemiubacc  6389  tfr1onlemsucaccv  6400  tfr1onlembfn  6403  tfr1onlemubacc  6405  tfr1onlemaccex  6407  tfr1onlemres  6408  tfrcllemsucaccv  6413  tfrcllembfn  6416  tfrcllemubacc  6418  tfrcllemaccex  6420  tfrcllemres  6421  tfrcl  6423  frecrdg  6467  omv2  6524  nnasuc  6535  nnmsuc  6536  nnacom  6543  nnaass  6544  nnmass  6546  nntri1  6555  nndifsnid  6566  nnmordi  6575  swoer  6621  erth  6639  riinerm  6668  qliftlem  6673  ecovass  6704  ecoviass  6705  elmapssres  6733  fvixp  6763  f1domg  6818  endomtr  6850  xpsnen2g  6889  enen1  6902  enen2  6903  domen1  6904  domen2  6905  mapen  6908  mapxpen  6910  ssenen  6913  phplem1  6914  fidifsnid  6933  findcard  6950  findcard2  6951  findcard2s  6952  fieq0  7043  isotilem  7073  supisolem  7075  inflbti  7091  ordiso2  7102  djuex  7110  updjudhcoinlf  7147  updjudhcoinrg  7148  updjud  7149  ctssdccl  7178  enumctlemm  7181  nnnninf  7193  finomni  7207  pm54.43  7259  acfun  7276  ccfunen  7333  cc2lem  7335  cc3  7337  addclpi  7396  addasspig  7399  mulasspig  7401  addnidpig  7405  nnppipi  7412  ltanqi  7471  ltmnqi  7472  ltexnqq  7477  archnqq  7486  prarloclemarch2  7488  enq0sym  7501  enq0tr  7503  nqnq0pi  7507  nqnq0  7510  mulcanenq0ec  7514  addclnq0  7520  nqpnq0nq  7522  distrnq0  7528  addassnq0lemcl  7530  addassnq0  7531  prubl  7555  prarloclemlt  7562  genpdf  7577  genipv  7578  genpelvl  7581  genpelvu  7582  genpml  7586  genpmu  7587  genprndl  7590  genprndu  7591  genpassl  7593  genpassu  7594  genpassg  7595  addnqprl  7598  addnqpru  7599  addlocpr  7605  nqprm  7611  nqprl  7620  nqpru  7621  mulnqprl  7637  mulnqpru  7638  mullocprlem  7639  mullocpr  7640  addcomprg  7647  mulcomprg  7649  distrlem1prl  7651  distrlem1pru  7652  distrlem4prl  7653  distrlem4pru  7654  ltprordil  7658  1idprl  7659  1idpru  7660  ltpopr  7664  ltsopr  7665  ltaddpr  7666  ltexprlemm  7669  ltexprlemopl  7670  ltexprlemlol  7671  ltexprlemopu  7672  ltexprlemupu  7673  ltexprlemdisj  7675  ltexprlemloc  7676  ltexprlemfl  7678  ltexprlemrl  7679  ltexprlemfu  7680  ltexprlemru  7681  addcanprleml  7683  addcanprlemu  7684  prplnqu  7689  recexprlemloc  7700  recexprlem1ssl  7702  recexprlem1ssu  7703  recexprlemss1l  7704  recexprlemss1u  7705  aptiprleml  7708  aptiprlemu  7709  cauappcvgprlemloc  7721  cauappcvgprlemladdru  7725  cauappcvgprlemladdrl  7726  caucvgprlemloc  7744  caucvgprlemladdrl  7747  caucvgprprlemml  7763  caucvgprprlemloc  7772  00sr  7838  map2psrprg  7874  suplocsrlempr  7876  suplocsrlem  7877  adddir  8019  axsuploc  8101  eqle  8120  le2tri3i  8137  mul4  8160  muladd11  8161  cnegexlem3  8205  addsub12  8241  2addsub  8242  addsubeq4  8243  subadd4  8272  negcon1  8280  negdi2  8286  negsubdi2  8287  neg2sub  8288  renegcl  8289  muladd  8412  subdir  8414  gt0ne0  8456  ltnegcon1  8492  lenegcon1  8495  eqord1  8512  eqord2  8513  recexre  8607  ltmul1  8621  recexap  8682  div12ap  8723  rerecapb  8872  p1le  8878  ltmul2  8885  gt0div  8899  ge0div  8900  zlem1lt  9384  nnaddm1cl  9389  zdceq  9403  gtndiv  9423  prime  9427  msqznn  9428  btwnz  9447  uzss  9624  eluzadd  9632  nn0pzuz  9663  supinfneg  9671  infsupneg  9672  divfnzn  9697  qnegcl  9712  qreccl  9718  elpqb  9726  xaddass  9946  xleadd1a  9950  xlesubadd  9960  elico2  10014  iccss  10018  iccsupr  10043  elfz5  10094  fznn  10166  difelfznle  10212  fzoaddel  10270  qdceq  10336  qbtwnxr  10349  flqbi2  10383  adddivflid  10384  fldivnn0  10387  divfl0  10388  flqmulnn0  10391  fldivnn0le  10395  fldiv4p1lem1div2  10397  ceiqle  10407  flqdiv  10415  modqmulnn  10436  frecuzrdgtcl  10506  frecuzrdgsuc  10508  frecuzrdgdomlem  10511  frecuzrdgfunlem  10513  frecuzrdgsuctlem  10517  seqm1g  10568  seq3caopr2  10587  seqcaopr2g  10588  iseqf1olemkle  10591  seq3f1olemp  10609  seqf1oglem2  10614  seqf1og  10615  seq3id  10619  seq3z  10622  expap0  10663  mulexp  10672  mulexpzap  10673  expmul  10678  leexp1a  10688  expubnd  10690  zesq  10752  bernneq  10754  bernneq3  10756  modqexp  10760  facdiv  10832  facndiv  10833  faclbnd3  10837  faclbnd6  10838  bccmpl  10848  bcpasc  10860  bccl  10861  seq3coll  10936  wrdsymb1  10973  shftlem  10983  ovshftex  10986  shftval4  10995  shftf  10997  shftcan2  11002  crim  11025  mulreap  11031  remul2  11040  immul2  11047  cjexp  11060  caucvgre  11148  r19.2uz  11160  sqrtsq2  11210  absnid  11240  absexp  11246  nn0abscl  11252  abslt  11255  lenegsq  11262  cau3lem  11281  minmax  11397  xrmaxadd  11428  clim  11448  climshftlemg  11469  climcn1  11475  climcn1lem  11486  clim2ser  11504  clim2ser2  11505  iserex  11506  isermulc2  11507  climub  11511  climcaucn  11518  serf0  11519  summodclem3  11547  summodclem2a  11548  summodclem2  11549  summodc  11550  fsum3  11554  fsumf1o  11557  fisumss  11559  isumss2  11560  fsumcl2lem  11565  fsumadd  11573  fsumsplit  11574  isummulc2  11593  fsum2d  11602  fsummulc2  11615  telfsumo  11633  fsumparts  11637  hash2iun1dif1  11647  bcxmas  11656  isumshft  11657  isumsplit  11658  expcnvap0  11669  geolim  11678  geolim2  11679  cvgratnnlemmn  11692  cvgratnnlemseq  11693  mertenslemi1  11702  mertenslem2  11703  mertensabs  11704  clim2divap  11707  prodmodclem3  11742  prodmodclem2a  11743  fprodseq  11750  fprodf1o  11755  fprodmul  11758  fprodsplitdc  11763  efcllemp  11825  reefcl  11835  efcj  11840  efaddlem  11841  efexp  11849  reeftlcl  11856  eftlub  11857  efsep  11858  effsumlt  11859  eflegeo  11868  retanclap  11889  demoivre  11940  demoivreALT  11941  eirraplem  11944  dvdsval3  11958  p1modz1  11961  iddvdsexp  11982  alzdvds  12021  addmodlteqALT  12026  nnehalf  12071  nno  12073  ndvdsadd  12098  bitsp1e  12119  bitsp1o  12120  bitsinv1  12129  divgcdnnr  12153  neggcd  12160  gcdabs  12165  bezoutlemmain  12175  bezoutlemaz  12180  bezoutlembz  12181  gcdmultiplez  12198  gcdzeq  12199  dvdssq  12208  nninfctlemfo  12217  algrf  12223  algcvg  12226  algcvga  12229  algfx  12230  eucalgf  12233  eucalgcvga  12236  neglcm  12253  lcmabs  12254  lcmdvds  12257  lcmgcdeq  12261  qredeq  12274  isprm3  12296  coprm  12322  prmrp  12323  isprm6  12325  prmdvdsexpb  12327  rpexp  12331  cncongrprm  12335  sqrt2irraplemnn  12357  phibndlem  12394  phiprmpw  12400  eulerthlemh  12409  eulerthlemth  12410  fermltl  12412  prmdivdiv  12415  modprm1div  12426  m1dvdsndvds  12427  coprimeprodsq  12436  pczpre  12476  pczcl  12477  pcexp  12488  pczdvds  12493  pczndvds  12495  pczndvds2  12497  pcdvdsb  12499  pcneg  12504  pcprmpw  12513  difsqpwdvds  12517  pcmptcl  12521  pcprod  12525  fldivp1  12527  infpnlem2  12539  1arithlem4  12545  ennnfonelemrn  12646  topnidg  12933  imasaddfnlemg  12967  imasaddflemg  12969  qusin  12979  mgmlrid  13032  mndass  13075  mhmco  13132  gsumsubm  13136  gsumwcl  13139  gsumwmhm  13140  grpass  13151  grpinvex  13152  dfgrp2  13169  grplid  13173  grprid  13174  grprcan  13179  grpinvssd  13219  grpinvval2  13225  mhmid  13255  mhmmnd  13256  ghmgrp  13258  mulgnn  13266  mulgnnp1  13270  mulgnegnn  13272  mulgnnsubcl  13274  mulgz  13290  issubg2m  13329  issubg4m  13333  subgintm  13338  nmzbi  13349  eqger  13364  eqgid  13366  eqgen  13367  qusgrp  13372  qusadd  13374  qusinv  13376  qussub  13377  ghminv  13390  ghmsub  13391  ghmrn  13397  resghm2b  13402  ghmf1  13413  conjsubg  13417  conjsubgen  13418  qusghm  13422  cmncom  13442  ablsubadd  13452  ablsubsub23  13465  ghmcmn  13467  gsumfzreidx  13477  mgpress  13497  srg1expzeq1  13561  ringinvnz1ne0  13615  ringinvnzdiv  13616  dvdsrd  13660  dvdsunit  13678  unitinvcl  13689  unitinvinv  13690  unitlinv  13692  unitrinv  13693  rhmunitinv  13744  subrngintm  13778  subrg1  13797  subrguss  13802  subrginv  13803  subrgunit  13805  subrgugrp  13806  subrgintm  13809  resrhm  13814  resrhm2b  13815  lmodass  13869  lmodlcan  13870  lmod0vlid  13884  lmod0vrid  13885  lmod0vid  13886  lmodvs0  13888  lcomf  13893  lmodvnegcl  13894  lmodvnegid  13895  lmodvsubadd  13904  lmodsubid  13913  lss1d  13949  lspval  13956  lspsnel6  13974  lspsnneg  13986  sralmod  14016  dflidl2rng  14047  lidlacl  14050  dflidl2  14054  df2idl2  14075  qusmul2  14095  quscrng  14099  cnfldmulg  14142  znf1o  14217  znidom  14223  psraddcl  14242  tgss3  14324  clsval  14357  clsss3  14376  neiss2  14388  resttop  14416  resttopon2  14424  lmconst  14462  cnima  14466  cnntri  14470  cncnp  14476  cnrest  14481  cndis  14487  lmss  14492  lmff  14495  lmtopcnp  14496  txcnp  14517  upxp  14518  uptx  14520  cnmpt11  14529  hmeoima  14556  hmeoopn  14557  hmeocld  14558  hmeontr  14559  hmeoimaf1o  14560  mettri2  14608  met0  14610  metres2  14627  blpnf  14646  xblss2ps  14650  xblss2  14651  blbas  14679  blres  14680  xmetec  14683  mopnss  14696  xmstri2  14716  mstri2  14717  xmstri  14718  mstri  14719  xmstri3  14720  mstri3  14721  msrtri  14722  mopni3  14730  unimopn  14732  comet  14745  bdxmet  14747  climcncf  14830  dedekindeulemuub  14863  dedekindicclemuub  14872  ivthdichlem  14897  dvfgg  14934  dvidlemap  14937  dvidrelem  14938  dvidsslem  14939  dvfre  14956  dvmptfsum  14971  plyadd  14997  plymul  14998  reeff1olem  15017  reeff1o  15019  sinperlem  15054  abssinper  15092  reexplog  15117  relogexp  15118  cxpexpnn  15142  cxprec  15156  rpcxpmul2  15159  abscxp  15161  wilthlem1  15226  sgmval2  15230  sgmnncl  15234  0sgmppw  15239  perfectlem1  15245  lgsdir  15286  lgsprme0  15293  lgsdinn0  15299  gausslemma2dlem3  15314  gausslemma2dlem5a  15316  2lgslem1a2  15338  2lgslem1a  15339  2lgslem3  15352  2lgs  15355  bj-inex  15563  bj-nn0suc  15620  bj-nn0sucALT  15634  trilpolemeq1  15694  trilpolemlt1  15695  trirec0  15698  nconstwlpolemgt0  15718