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  941  3adantl1  1156  3adantl2  1157  3adantl3  1158  syl3anl1  1298  syl3anl3  1300  syl3anl  1301  stoic3  1451  eupick  2133  csbiebt  3133  csbnestgf  3146  reuss2  3453  mpteq12  4127  otexg  4274  opelopabt  4308  sonr  4364  sotr  4365  issod  4366  so2nr  4368  so3nr  4369  ordelss  4426  onelon  4431  elrnmpt1s  4928  iota2  5261  funeu  5296  imadif  5354  fnbr  5378  feu  5458  f1ss  5487  f1ssres  5490  f1resf1  5491  dffo2  5502  foco  5509  foun  5541  fun11iun  5543  ffoss  5554  funbrfv  5617  fvco3  5650  fvopab6  5676  funfvbrb  5693  elpreima  5699  ffvelcdm  5713  ffvelcdmda  5715  dffo4  5728  fmptco  5746  fsn2  5754  fvconst2g  5798  fex  5813  funfvima  5816  f1elima  5842  f1ocnvfv1  5846  f1ocnvfv2  5847  cocan2  5857  foeqcnvco  5859  isocnv  5880  isores2  5882  isoini  5887  isoselem  5889  f1oiso  5895  f1ofveu  5932  eloprabga  6032  suppssof1  6176  ofco  6177  offveqb  6178  ofc1g  6180  ofc2g  6181  caofid0l  6185  caofid0r  6186  caofid1  6187  caofid2  6188  fnexALT  6196  f1dmex  6201  ot1stg  6238  ot2ndg  6239  ot3rdgg  6240  eqopi  6258  2ndrn  6269  fo2ndf  6313  smores3  6379  smores2  6380  smoel  6386  smoiso  6388  tfrlem1  6394  tfrlemisucaccv  6411  tfrlemibxssdm  6413  tfrlemiubacc  6416  tfr1onlemsucaccv  6427  tfr1onlembfn  6430  tfr1onlemubacc  6432  tfr1onlemaccex  6434  tfr1onlemres  6435  tfrcllemsucaccv  6440  tfrcllembfn  6443  tfrcllemubacc  6445  tfrcllemaccex  6447  tfrcllemres  6448  tfrcl  6450  frecrdg  6494  omv2  6551  nnasuc  6562  nnmsuc  6563  nnacom  6570  nnaass  6571  nnmass  6573  nntri1  6582  nndifsnid  6593  nnmordi  6602  swoer  6648  erth  6666  riinerm  6695  qliftlem  6700  ecovass  6731  ecoviass  6732  elmapssres  6760  fvixp  6790  f1domg  6849  domssr  6869  endomtr  6882  xpsnen2g  6924  enen1  6937  enen2  6938  domen1  6939  domen2  6940  mapen  6943  mapxpen  6945  ssenen  6948  phplem1  6949  fidifsnid  6968  findcard  6985  findcard2  6986  findcard2s  6987  fieq0  7078  isotilem  7108  supisolem  7110  inflbti  7126  ordiso2  7137  djuex  7145  updjudhcoinlf  7182  updjudhcoinrg  7183  updjud  7184  ctssdccl  7213  enumctlemm  7216  nnnninf  7228  finomni  7242  pm54.43  7298  acfun  7319  ccfunen  7376  cc2lem  7378  cc3  7380  addclpi  7440  addasspig  7443  mulasspig  7445  addnidpig  7449  nnppipi  7456  ltanqi  7515  ltmnqi  7516  ltexnqq  7521  archnqq  7530  prarloclemarch2  7532  enq0sym  7545  enq0tr  7547  nqnq0pi  7551  nqnq0  7554  mulcanenq0ec  7558  addclnq0  7564  nqpnq0nq  7566  distrnq0  7572  addassnq0lemcl  7574  addassnq0  7575  prubl  7599  prarloclemlt  7606  genpdf  7621  genipv  7622  genpelvl  7625  genpelvu  7626  genpml  7630  genpmu  7631  genprndl  7634  genprndu  7635  genpassl  7637  genpassu  7638  genpassg  7639  addnqprl  7642  addnqpru  7643  addlocpr  7649  nqprm  7655  nqprl  7664  nqpru  7665  mulnqprl  7681  mulnqpru  7682  mullocprlem  7683  mullocpr  7684  addcomprg  7691  mulcomprg  7693  distrlem1prl  7695  distrlem1pru  7696  distrlem4prl  7697  distrlem4pru  7698  ltprordil  7702  1idprl  7703  1idpru  7704  ltpopr  7708  ltsopr  7709  ltaddpr  7710  ltexprlemm  7713  ltexprlemopl  7714  ltexprlemlol  7715  ltexprlemopu  7716  ltexprlemupu  7717  ltexprlemdisj  7719  ltexprlemloc  7720  ltexprlemfl  7722  ltexprlemrl  7723  ltexprlemfu  7724  ltexprlemru  7725  addcanprleml  7727  addcanprlemu  7728  prplnqu  7733  recexprlemloc  7744  recexprlem1ssl  7746  recexprlem1ssu  7747  recexprlemss1l  7748  recexprlemss1u  7749  aptiprleml  7752  aptiprlemu  7753  cauappcvgprlemloc  7765  cauappcvgprlemladdru  7769  cauappcvgprlemladdrl  7770  caucvgprlemloc  7788  caucvgprlemladdrl  7791  caucvgprprlemml  7807  caucvgprprlemloc  7816  00sr  7882  map2psrprg  7918  suplocsrlempr  7920  suplocsrlem  7921  adddir  8063  axsuploc  8145  eqle  8164  le2tri3i  8181  mul4  8204  muladd11  8205  cnegexlem3  8249  addsub12  8285  2addsub  8286  addsubeq4  8287  subadd4  8316  negcon1  8324  negdi2  8330  negsubdi2  8331  neg2sub  8332  renegcl  8333  muladd  8456  subdir  8458  gt0ne0  8500  ltnegcon1  8536  lenegcon1  8539  eqord1  8556  eqord2  8557  recexre  8651  ltmul1  8665  recexap  8726  div12ap  8767  rerecapb  8916  p1le  8922  ltmul2  8929  gt0div  8943  ge0div  8944  zlem1lt  9429  nnaddm1cl  9434  zdceq  9448  gtndiv  9468  prime  9472  msqznn  9473  btwnz  9492  uzss  9669  eluzadd  9677  nn0pzuz  9708  supinfneg  9716  infsupneg  9717  divfnzn  9742  qnegcl  9757  qreccl  9763  elpqb  9771  xaddass  9991  xleadd1a  9995  xlesubadd  10005  elico2  10059  iccss  10063  iccsupr  10088  elfz5  10139  fznn  10211  difelfznle  10257  fzoaddel  10316  elincfzoext  10322  qdceq  10387  qbtwnxr  10400  flqbi2  10434  adddivflid  10435  fldivnn0  10438  divfl0  10439  flqmulnn0  10442  fldivnn0le  10446  fldiv4p1lem1div2  10448  ceiqle  10458  flqdiv  10466  modqmulnn  10487  frecuzrdgtcl  10557  frecuzrdgsuc  10559  frecuzrdgdomlem  10562  frecuzrdgfunlem  10564  frecuzrdgsuctlem  10568  seqm1g  10619  seq3caopr2  10638  seqcaopr2g  10639  iseqf1olemkle  10642  seq3f1olemp  10660  seqf1oglem2  10665  seqf1og  10666  seq3id  10670  seq3z  10673  expap0  10714  mulexp  10723  mulexpzap  10724  expmul  10729  leexp1a  10739  expubnd  10741  zesq  10803  bernneq  10805  bernneq3  10807  modqexp  10811  facdiv  10883  facndiv  10884  faclbnd3  10888  faclbnd6  10889  bccmpl  10899  bcpasc  10911  bccl  10912  seq3coll  10987  fundm2domnop  10991  wrdsymb1  11030  ccatfv0  11059  ccatrn  11065  ccat2s1cl  11087  lswccats1fst  11096  swrdspsleq  11120  shftlem  11127  ovshftex  11130  shftval4  11139  shftf  11141  shftcan2  11146  crim  11169  mulreap  11175  remul2  11184  immul2  11191  cjexp  11204  caucvgre  11292  r19.2uz  11304  sqrtsq2  11354  absnid  11384  absexp  11390  nn0abscl  11396  abslt  11399  lenegsq  11406  cau3lem  11425  minmax  11541  xrmaxadd  11572  clim  11592  climshftlemg  11613  climcn1  11619  climcn1lem  11630  clim2ser  11648  clim2ser2  11649  iserex  11650  isermulc2  11651  climub  11655  climcaucn  11662  serf0  11663  summodclem3  11691  summodclem2a  11692  summodclem2  11693  summodc  11694  fsum3  11698  fsumf1o  11701  fisumss  11703  isumss2  11704  fsumcl2lem  11709  fsumadd  11717  fsumsplit  11718  isummulc2  11737  fsum2d  11746  fsummulc2  11759  telfsumo  11777  fsumparts  11781  hash2iun1dif1  11791  bcxmas  11800  isumshft  11801  isumsplit  11802  expcnvap0  11813  geolim  11822  geolim2  11823  cvgratnnlemmn  11836  cvgratnnlemseq  11837  mertenslemi1  11846  mertenslem2  11847  mertensabs  11848  clim2divap  11851  prodmodclem3  11886  prodmodclem2a  11887  fprodseq  11894  fprodf1o  11899  fprodmul  11902  fprodsplitdc  11907  efcllemp  11969  reefcl  11979  efcj  11984  efaddlem  11985  efexp  11993  reeftlcl  12000  eftlub  12001  efsep  12002  effsumlt  12003  eflegeo  12012  retanclap  12033  demoivre  12084  demoivreALT  12085  eirraplem  12088  dvdsval3  12102  p1modz1  12105  iddvdsexp  12126  alzdvds  12165  addmodlteqALT  12170  nnehalf  12215  nno  12217  ndvdsadd  12242  bitsp1e  12263  bitsp1o  12264  bitsinv1  12273  divgcdnnr  12297  neggcd  12304  gcdabs  12309  bezoutlemmain  12319  bezoutlemaz  12324  bezoutlembz  12325  gcdmultiplez  12342  gcdzeq  12343  dvdssq  12352  nninfctlemfo  12361  algrf  12367  algcvg  12370  algcvga  12373  algfx  12374  eucalgf  12377  eucalgcvga  12380  neglcm  12397  lcmabs  12398  lcmdvds  12401  lcmgcdeq  12405  qredeq  12418  isprm3  12440  coprm  12466  prmrp  12467  isprm6  12469  prmdvdsexpb  12471  rpexp  12475  cncongrprm  12479  sqrt2irraplemnn  12501  phibndlem  12538  phiprmpw  12544  eulerthlemh  12553  eulerthlemth  12554  fermltl  12556  prmdivdiv  12559  modprm1div  12570  m1dvdsndvds  12571  coprimeprodsq  12580  pczpre  12620  pczcl  12621  pcexp  12632  pczdvds  12637  pczndvds  12639  pczndvds2  12641  pcdvdsb  12643  pcneg  12648  pcprmpw  12657  difsqpwdvds  12661  pcmptcl  12665  pcprod  12669  fldivp1  12671  infpnlem2  12683  1arithlem4  12689  ennnfonelemrn  12790  topnidg  13084  pwselbasb  13125  pwsplusgval  13127  pwsmulrval  13128  imasaddfnlemg  13146  imasaddflemg  13148  qusin  13158  mgmlrid  13211  mndass  13256  prdsidlem  13279  mhmco  13322  gsumsubm  13326  gsumwcl  13329  gsumwmhm  13330  grpass  13341  grpinvex  13342  dfgrp2  13359  grplid  13363  grprid  13364  grprcan  13369  grpinvssd  13409  grpinvval2  13415  prdsinvlem  13440  pwsinvg  13444  mhmid  13451  mhmmnd  13452  ghmgrp  13454  mulgnn  13462  mulgnnp1  13466  mulgnegnn  13468  mulgnnsubcl  13470  mulgz  13486  issubg2m  13525  issubg4m  13529  subgintm  13534  nmzbi  13545  eqger  13560  eqgid  13562  eqgen  13563  qusgrp  13568  qusadd  13570  qusinv  13572  qussub  13573  ghminv  13586  ghmsub  13587  ghmrn  13593  resghm2b  13598  ghmf1  13609  conjsubg  13613  conjsubgen  13614  qusghm  13618  cmncom  13638  ablsubadd  13648  ablsubsub23  13661  ghmcmn  13663  gsumfzreidx  13673  mgpress  13693  srg1expzeq1  13757  ringinvnz1ne0  13811  ringinvnzdiv  13812  dvdsrd  13856  dvdsunit  13874  unitinvcl  13885  unitinvinv  13886  unitlinv  13888  unitrinv  13889  rhmunitinv  13940  subrngintm  13974  subrg1  13993  subrguss  13998  subrginv  13999  subrgunit  14001  subrgugrp  14002  subrgintm  14005  resrhm  14010  resrhm2b  14011  lmodass  14065  lmodlcan  14066  lmod0vlid  14080  lmod0vrid  14081  lmod0vid  14082  lmodvs0  14084  lcomf  14089  lmodvnegcl  14090  lmodvnegid  14091  lmodvsubadd  14100  lmodsubid  14109  lss1d  14145  lspval  14152  lspsnel6  14170  lspsnneg  14182  sralmod  14212  dflidl2rng  14243  lidlacl  14246  dflidl2  14250  df2idl2  14271  qusmul2  14291  quscrng  14295  cnfldmulg  14338  znf1o  14413  znidom  14419  psraddcl  14442  psr0lid  14444  tgss3  14550  clsval  14583  clsss3  14602  neiss2  14614  resttop  14642  resttopon2  14650  lmconst  14688  cnima  14692  cnntri  14696  cncnp  14702  cnrest  14707  cndis  14713  lmss  14718  lmff  14721  lmtopcnp  14722  txcnp  14743  upxp  14744  uptx  14746  cnmpt11  14755  hmeoima  14782  hmeoopn  14783  hmeocld  14784  hmeontr  14785  hmeoimaf1o  14786  mettri2  14834  met0  14836  metres2  14853  blpnf  14872  xblss2ps  14876  xblss2  14877  blbas  14905  blres  14906  xmetec  14909  mopnss  14922  xmstri2  14942  mstri2  14943  xmstri  14944  mstri  14945  xmstri3  14946  mstri3  14947  msrtri  14948  mopni3  14956  unimopn  14958  comet  14971  bdxmet  14973  climcncf  15056  dedekindeulemuub  15089  dedekindicclemuub  15098  ivthdichlem  15123  dvfgg  15160  dvidlemap  15163  dvidrelem  15164  dvidsslem  15165  dvfre  15182  dvmptfsum  15197  plyadd  15223  plymul  15224  reeff1olem  15243  reeff1o  15245  sinperlem  15280  abssinper  15318  reexplog  15343  relogexp  15344  cxpexpnn  15368  cxprec  15382  rpcxpmul2  15385  abscxp  15387  wilthlem1  15452  sgmval2  15456  sgmnncl  15460  0sgmppw  15465  perfectlem1  15471  lgsdir  15512  lgsprme0  15519  lgsdinn0  15525  gausslemma2dlem3  15540  gausslemma2dlem5a  15542  2lgslem1a2  15564  2lgslem1a  15565  2lgslem3  15578  2lgs  15581  bj-inex  15843  bj-nn0suc  15900  bj-nn0sucALT  15914  trilpolemeq1  15979  trilpolemlt1  15980  trirec0  15983  nconstwlpolemgt0  16003