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  944  dfifp2dc  987  3adantl1  1177  3adantl2  1178  3adantl3  1179  syl3anl1  1319  syl3anl3  1321  syl3anl  1322  stoic3  1473  eupick  2157  csbiebt  3164  csbnestgf  3177  reuss2  3484  mpteq12  4167  otexg  4316  opelopabt  4350  sonr  4408  sotr  4409  issod  4410  so2nr  4412  so3nr  4413  ordelss  4470  onelon  4475  elrnmpt1s  4974  iota2  5308  funeu  5343  imadif  5401  fnbr  5425  feu  5510  f1ss  5539  f1ssres  5542  f1resf1  5543  dffo2  5554  foco  5561  foun  5593  fun11iun  5595  ffoss  5606  funbrfv  5672  fvco3  5707  fvopab6  5733  funfvbrb  5750  elpreima  5756  ffvelcdm  5770  ffvelcdmda  5772  dffo4  5785  fmptco  5803  fsn2  5811  fncofn  5821  fvconst2g  5857  fex  5872  funfvima  5875  f1elima  5903  f1ocnvfv1  5907  f1ocnvfv2  5908  cocan2  5918  foeqcnvco  5920  isocnv  5941  isores2  5943  isoini  5948  isoselem  5950  f1oiso  5956  f1ofveu  5995  eloprabga  6097  suppssof1  6242  ofco  6243  offveqb  6244  ofc1g  6246  ofc2g  6247  caofid0l  6251  caofid0r  6252  caofid1  6253  caofid2  6254  fnexALT  6262  f1dmex  6267  ot1stg  6304  ot2ndg  6305  ot3rdgg  6306  eqopi  6324  2ndrn  6335  fo2ndf  6379  smores3  6445  smores2  6446  smoel  6452  smoiso  6454  tfrlem1  6460  tfrlemisucaccv  6477  tfrlemibxssdm  6479  tfrlemiubacc  6482  tfr1onlemsucaccv  6493  tfr1onlembfn  6496  tfr1onlemubacc  6498  tfr1onlemaccex  6500  tfr1onlemres  6501  tfrcllemsucaccv  6506  tfrcllembfn  6509  tfrcllemubacc  6511  tfrcllemaccex  6513  tfrcllemres  6514  tfrcl  6516  frecrdg  6560  omv2  6619  nnasuc  6630  nnmsuc  6631  nnacom  6638  nnaass  6639  nnmass  6641  nntri1  6650  nndifsnid  6661  nnmordi  6670  swoer  6716  erth  6734  riinerm  6763  qliftlem  6768  ecovass  6799  ecoviass  6800  elmapssres  6828  fvixp  6858  f1domg  6917  domssr  6937  endomtr  6950  xpsnen2g  6996  enen1  7009  enen2  7010  domen1  7011  domen2  7012  mapen  7015  mapxpen  7017  ssenen  7020  phplem1  7021  fidifsnid  7041  findcard  7058  findcard2  7059  findcard2s  7060  fidcen  7069  fieq0  7154  isotilem  7184  supisolem  7186  inflbti  7202  ordiso2  7213  djuex  7221  updjudhcoinlf  7258  updjudhcoinrg  7259  updjud  7260  ctssdccl  7289  enumctlemm  7292  nnnninf  7304  finomni  7318  pm54.43  7374  acfun  7400  ccfunen  7461  cc2lem  7463  cc3  7465  addclpi  7525  addasspig  7528  mulasspig  7530  addnidpig  7534  nnppipi  7541  ltanqi  7600  ltmnqi  7601  ltexnqq  7606  archnqq  7615  prarloclemarch2  7617  enq0sym  7630  enq0tr  7632  nqnq0pi  7636  nqnq0  7639  mulcanenq0ec  7643  addclnq0  7649  nqpnq0nq  7651  distrnq0  7657  addassnq0lemcl  7659  addassnq0  7660  prubl  7684  prarloclemlt  7691  genpdf  7706  genipv  7707  genpelvl  7710  genpelvu  7711  genpml  7715  genpmu  7716  genprndl  7719  genprndu  7720  genpassl  7722  genpassu  7723  genpassg  7724  addnqprl  7727  addnqpru  7728  addlocpr  7734  nqprm  7740  nqprl  7749  nqpru  7750  mulnqprl  7766  mulnqpru  7767  mullocprlem  7768  mullocpr  7769  addcomprg  7776  mulcomprg  7778  distrlem1prl  7780  distrlem1pru  7781  distrlem4prl  7782  distrlem4pru  7783  ltprordil  7787  1idprl  7788  1idpru  7789  ltpopr  7793  ltsopr  7794  ltaddpr  7795  ltexprlemm  7798  ltexprlemopl  7799  ltexprlemlol  7800  ltexprlemopu  7801  ltexprlemupu  7802  ltexprlemdisj  7804  ltexprlemloc  7805  ltexprlemfl  7807  ltexprlemrl  7808  ltexprlemfu  7809  ltexprlemru  7810  addcanprleml  7812  addcanprlemu  7813  prplnqu  7818  recexprlemloc  7829  recexprlem1ssl  7831  recexprlem1ssu  7832  recexprlemss1l  7833  recexprlemss1u  7834  aptiprleml  7837  aptiprlemu  7838  cauappcvgprlemloc  7850  cauappcvgprlemladdru  7854  cauappcvgprlemladdrl  7855  caucvgprlemloc  7873  caucvgprlemladdrl  7876  caucvgprprlemml  7892  caucvgprprlemloc  7901  00sr  7967  map2psrprg  8003  suplocsrlempr  8005  suplocsrlem  8006  adddir  8148  axsuploc  8230  eqle  8249  le2tri3i  8266  mul4  8289  muladd11  8290  cnegexlem3  8334  addsub12  8370  2addsub  8371  addsubeq4  8372  subadd4  8401  negcon1  8409  negdi2  8415  negsubdi2  8416  neg2sub  8417  renegcl  8418  muladd  8541  subdir  8543  gt0ne0  8585  ltnegcon1  8621  lenegcon1  8624  eqord1  8641  eqord2  8642  recexre  8736  ltmul1  8750  recexap  8811  div12ap  8852  rerecapb  9001  p1le  9007  ltmul2  9014  gt0div  9028  ge0div  9029  zlem1lt  9514  nnaddm1cl  9519  zdceq  9533  gtndiv  9553  prime  9557  msqznn  9558  btwnz  9577  uzss  9755  eluzadd  9763  nn0pzuz  9794  supinfneg  9802  infsupneg  9803  divfnzn  9828  qnegcl  9843  qreccl  9849  elpqb  9857  xaddass  10077  xleadd1a  10081  xlesubadd  10091  elico2  10145  iccss  10149  iccsupr  10174  elfz5  10225  fznn  10297  difelfznle  10343  fzoaddel  10405  elincfzoext  10411  qdceq  10476  qbtwnxr  10489  flqbi2  10523  adddivflid  10524  fldivnn0  10527  divfl0  10528  flqmulnn0  10531  fldivnn0le  10535  fldiv4p1lem1div2  10537  ceiqle  10547  flqdiv  10555  modqmulnn  10576  frecuzrdgtcl  10646  frecuzrdgsuc  10648  frecuzrdgdomlem  10651  frecuzrdgfunlem  10653  frecuzrdgsuctlem  10657  seqm1g  10708  seq3caopr2  10727  seqcaopr2g  10728  iseqf1olemkle  10731  seq3f1olemp  10749  seqf1oglem2  10754  seqf1og  10755  seq3id  10759  seq3z  10762  expap0  10803  mulexp  10812  mulexpzap  10813  expmul  10818  leexp1a  10828  expubnd  10830  zesq  10892  bernneq  10894  bernneq3  10896  modqexp  10900  facdiv  10972  facndiv  10973  faclbnd3  10977  faclbnd6  10978  bccmpl  10988  bcpasc  11000  bccl  11001  seq3coll  11077  fundm2domnop  11081  wrdsymb1  11121  ccatfv0  11151  ccatrn  11157  ccat2s1cl  11181  lswccats1fst  11191  swrdspsleq  11215  pfxtrcfv  11241  pfxsuffeqwrdeq  11246  pfxlswccat  11261  wrdeqs1cat  11268  cats1un  11269  swrdccatin1  11273  pfxccatin12lem4  11274  swrdccatin2  11277  pfxccatin12  11281  swrdccat  11283  shftlem  11343  ovshftex  11346  shftval4  11355  shftf  11357  shftcan2  11362  crim  11385  mulreap  11391  remul2  11400  immul2  11407  cjexp  11420  caucvgre  11508  r19.2uz  11520  sqrtsq2  11570  absnid  11600  absexp  11606  nn0abscl  11612  abslt  11615  lenegsq  11622  cau3lem  11641  minmax  11757  xrmaxadd  11788  clim  11808  climshftlemg  11829  climcn1  11835  climcn1lem  11846  clim2ser  11864  clim2ser2  11865  iserex  11866  isermulc2  11867  climub  11871  climcaucn  11878  serf0  11879  summodclem3  11907  summodclem2a  11908  summodclem2  11909  summodc  11910  fsum3  11914  fsumf1o  11917  fisumss  11919  isumss2  11920  fsumcl2lem  11925  fsumadd  11933  fsumsplit  11934  isummulc2  11953  fsum2d  11962  fsummulc2  11975  telfsumo  11993  fsumparts  11997  hash2iun1dif1  12007  bcxmas  12016  isumshft  12017  isumsplit  12018  expcnvap0  12029  geolim  12038  geolim2  12039  cvgratnnlemmn  12052  cvgratnnlemseq  12053  mertenslemi1  12062  mertenslem2  12063  mertensabs  12064  clim2divap  12067  prodmodclem3  12102  prodmodclem2a  12103  fprodseq  12110  fprodf1o  12115  fprodmul  12118  fprodsplitdc  12123  efcllemp  12185  reefcl  12195  efcj  12200  efaddlem  12201  efexp  12209  reeftlcl  12216  eftlub  12217  efsep  12218  effsumlt  12219  eflegeo  12228  retanclap  12249  demoivre  12300  demoivreALT  12301  eirraplem  12304  dvdsval3  12318  p1modz1  12321  iddvdsexp  12342  alzdvds  12381  addmodlteqALT  12386  nnehalf  12431  nno  12433  ndvdsadd  12458  bitsp1e  12479  bitsp1o  12480  bitsinv1  12489  divgcdnnr  12513  neggcd  12520  gcdabs  12525  bezoutlemmain  12535  bezoutlemaz  12540  bezoutlembz  12541  gcdmultiplez  12558  gcdzeq  12559  dvdssq  12568  nninfctlemfo  12577  algrf  12583  algcvg  12586  algcvga  12589  algfx  12590  eucalgf  12593  eucalgcvga  12596  neglcm  12613  lcmabs  12614  lcmdvds  12617  lcmgcdeq  12621  qredeq  12634  isprm3  12656  coprm  12682  prmrp  12683  isprm6  12685  prmdvdsexpb  12687  rpexp  12691  cncongrprm  12695  sqrt2irraplemnn  12717  phibndlem  12754  phiprmpw  12760  eulerthlemh  12769  eulerthlemth  12770  fermltl  12772  prmdivdiv  12775  modprm1div  12786  m1dvdsndvds  12787  coprimeprodsq  12796  pczpre  12836  pczcl  12837  pcexp  12848  pczdvds  12853  pczndvds  12855  pczndvds2  12857  pcdvdsb  12859  pcneg  12864  pcprmpw  12873  difsqpwdvds  12877  pcmptcl  12881  pcprod  12885  fldivp1  12887  infpnlem2  12899  1arithlem4  12905  ennnfonelemrn  13006  topnidg  13301  pwselbasb  13342  pwsplusgval  13344  pwsmulrval  13345  imasaddfnlemg  13363  imasaddflemg  13365  qusin  13375  mgmlrid  13428  mndass  13473  prdsidlem  13496  mhmco  13539  gsumsubm  13543  gsumwcl  13546  gsumwmhm  13547  grpass  13558  grpinvex  13559  dfgrp2  13576  grplid  13580  grprid  13581  grprcan  13586  grpinvssd  13626  grpinvval2  13632  prdsinvlem  13657  pwsinvg  13661  mhmid  13668  mhmmnd  13669  ghmgrp  13671  mulgnn  13679  mulgnnp1  13683  mulgnegnn  13685  mulgnnsubcl  13687  mulgz  13703  issubg2m  13742  issubg4m  13746  subgintm  13751  nmzbi  13762  eqger  13777  eqgid  13779  eqgen  13780  qusgrp  13785  qusadd  13787  qusinv  13789  qussub  13790  ghminv  13803  ghmsub  13804  ghmrn  13810  resghm2b  13815  ghmf1  13826  conjsubg  13830  conjsubgen  13831  qusghm  13835  cmncom  13855  ablsubadd  13865  ablsubsub23  13878  ghmcmn  13880  gsumfzreidx  13890  mgpress  13910  srg1expzeq1  13974  ringinvnz1ne0  14028  ringinvnzdiv  14029  dvdsrd  14074  dvdsunit  14092  unitinvcl  14103  unitinvinv  14104  unitlinv  14106  unitrinv  14107  rhmunitinv  14158  subrngintm  14192  subrg1  14211  subrguss  14216  subrginv  14217  subrgunit  14219  subrgugrp  14220  subrgintm  14223  resrhm  14228  resrhm2b  14229  lmodass  14283  lmodlcan  14284  lmod0vlid  14298  lmod0vrid  14299  lmod0vid  14300  lmodvs0  14302  lcomf  14307  lmodvnegcl  14308  lmodvnegid  14309  lmodvsubadd  14318  lmodsubid  14327  lss1d  14363  lspval  14370  lspsnel6  14388  lspsnneg  14400  sralmod  14430  dflidl2rng  14461  lidlacl  14464  dflidl2  14468  df2idl2  14489  qusmul2  14509  quscrng  14513  cnfldmulg  14556  znf1o  14631  znidom  14637  psraddcl  14660  psr0lid  14662  tgss3  14768  clsval  14801  clsss3  14820  neiss2  14832  resttop  14860  resttopon2  14868  lmconst  14906  cnima  14910  cnntri  14914  cncnp  14920  cnrest  14925  cndis  14931  lmss  14936  lmff  14939  lmtopcnp  14940  txcnp  14961  upxp  14962  uptx  14964  cnmpt11  14973  hmeoima  15000  hmeoopn  15001  hmeocld  15002  hmeontr  15003  hmeoimaf1o  15004  mettri2  15052  met0  15054  metres2  15071  blpnf  15090  xblss2ps  15094  xblss2  15095  blbas  15123  blres  15124  xmetec  15127  mopnss  15140  xmstri2  15160  mstri2  15161  xmstri  15162  mstri  15163  xmstri3  15164  mstri3  15165  msrtri  15166  mopni3  15174  unimopn  15176  comet  15189  bdxmet  15191  climcncf  15274  dedekindeulemuub  15307  dedekindicclemuub  15316  ivthdichlem  15341  dvfgg  15378  dvidlemap  15381  dvidrelem  15382  dvidsslem  15383  dvfre  15400  dvmptfsum  15415  plyadd  15441  plymul  15442  reeff1olem  15461  reeff1o  15463  sinperlem  15498  abssinper  15536  reexplog  15561  relogexp  15562  cxpexpnn  15586  cxprec  15600  rpcxpmul2  15603  abscxp  15605  wilthlem1  15670  sgmval2  15674  sgmnncl  15678  0sgmppw  15683  perfectlem1  15689  lgsdir  15730  lgsprme0  15737  lgsdinn0  15743  gausslemma2dlem3  15758  gausslemma2dlem5a  15760  2lgslem1a2  15782  2lgslem1a  15783  2lgslem3  15796  2lgs  15799  umgredgprv  15931  umgrislfupgrdom  15945  uspgredgiedg  15992  uspgriedgedg  15993  usgrislfuspgrdom  16004  usgredg2en  16009  usgredgprv  16010  usgrpredgv  16012  usgredg  16014  usgrnloopv  16015  usgredgne  16018  usgredg3  16028  usgredgedg  16041  usgredgdomord  16044  umgrwlknloop  16114  wlkres  16123  clwwlkccatlem  16143  clwwlkccat  16144  bj-inex  16353  bj-nn0suc  16410  bj-nn0sucALT  16424  trilpolemeq1  16496  trilpolemlt1  16497  trirec0  16500  nconstwlpolemgt0  16520