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  571  pm4.55dc  947  dfifp2dc  990  3adantl1  1180  3adantl2  1181  3adantl3  1182  syl3anl1  1322  syl3anl3  1324  syl3anl  1325  stoic3  1476  eupick  2159  csbiebt  3168  csbnestgf  3181  reuss2  3489  mpteq12  4177  otexg  4328  opelopabt  4362  sonr  4420  sotr  4421  issod  4422  so2nr  4424  so3nr  4425  ordelss  4482  onelon  4487  elrnmpt1s  4988  iota2  5323  funeu  5358  imadif  5417  fnbr  5441  feu  5527  f1ss  5557  f1ssres  5560  f1resf1  5561  dffo2  5572  foco  5579  foun  5611  fun11iun  5613  ffoss  5625  funbrfv  5691  fvco3  5726  fvopab6  5752  funfvbrb  5769  elpreima  5775  ffvelcdm  5788  ffvelcdmda  5790  dffo4  5803  fmptco  5821  fsn2  5829  fncofn  5840  fvconst2g  5876  fex  5893  funfvima  5896  f1elima  5924  f1ocnvfv1  5928  f1ocnvfv2  5929  cocan2  5939  foeqcnvco  5941  isocnv  5962  isores2  5964  isoini  5969  isoselem  5971  f1oiso  5977  f1ofveu  6016  eloprabga  6118  suppssof1  6262  ofco  6263  offveqb  6264  ofc1g  6266  ofc2g  6267  caofid0l  6271  caofid0r  6272  caofid1  6273  caofid2  6274  fnexALT  6282  f1dmex  6287  ot1stg  6324  ot2ndg  6325  ot3rdgg  6326  eqopi  6344  2ndrn  6355  fo2ndf  6401  suppval1  6417  ressuppss  6432  suppssrst  6439  suppssrgst  6440  smores3  6502  smores2  6503  smoel  6509  smoiso  6511  tfrlem1  6517  tfrlemisucaccv  6534  tfrlemibxssdm  6536  tfrlemiubacc  6539  tfr1onlemsucaccv  6550  tfr1onlembfn  6553  tfr1onlemubacc  6555  tfr1onlemaccex  6557  tfr1onlemres  6558  tfrcllemsucaccv  6563  tfrcllembfn  6566  tfrcllemubacc  6568  tfrcllemaccex  6570  tfrcllemres  6571  tfrcl  6573  frecrdg  6617  omv2  6676  nnasuc  6687  nnmsuc  6688  nnacom  6695  nnaass  6696  nnmass  6698  nntri1  6707  nndifsnid  6718  nnmordi  6727  swoer  6773  erth  6791  riinerm  6820  qliftlem  6825  ecovass  6856  ecoviass  6857  elmapssres  6885  fvixp  6915  f1domg  6974  domssr  6994  endomtr  7007  xpsnen2g  7056  enen1  7069  enen2  7070  domen1  7071  domen2  7072  mapen  7075  mapxpen  7077  ssenen  7080  phplem1  7081  fidifsnid  7101  findcard  7120  findcard2  7121  findcard2s  7122  fidcen  7131  fieq0  7235  isotilem  7265  supisolem  7267  inflbti  7283  ordiso2  7294  djuex  7302  updjudhcoinlf  7339  updjudhcoinrg  7340  updjud  7341  ctssdccl  7370  enumctlemm  7373  nnnninf  7385  finomni  7399  pm54.43  7455  acfun  7482  ccfunen  7543  cc2lem  7545  cc3  7547  addclpi  7607  addasspig  7610  mulasspig  7612  addnidpig  7616  nnppipi  7623  ltanqi  7682  ltmnqi  7683  ltexnqq  7688  archnqq  7697  prarloclemarch2  7699  enq0sym  7712  enq0tr  7714  nqnq0pi  7718  nqnq0  7721  mulcanenq0ec  7725  addclnq0  7731  nqpnq0nq  7733  distrnq0  7739  addassnq0lemcl  7741  addassnq0  7742  prubl  7766  prarloclemlt  7773  genpdf  7788  genipv  7789  genpelvl  7792  genpelvu  7793  genpml  7797  genpmu  7798  genprndl  7801  genprndu  7802  genpassl  7804  genpassu  7805  genpassg  7806  addnqprl  7809  addnqpru  7810  addlocpr  7816  nqprm  7822  nqprl  7831  nqpru  7832  mulnqprl  7848  mulnqpru  7849  mullocprlem  7850  mullocpr  7851  addcomprg  7858  mulcomprg  7860  distrlem1prl  7862  distrlem1pru  7863  distrlem4prl  7864  distrlem4pru  7865  ltprordil  7869  1idprl  7870  1idpru  7871  ltpopr  7875  ltsopr  7876  ltaddpr  7877  ltexprlemm  7880  ltexprlemopl  7881  ltexprlemlol  7882  ltexprlemopu  7883  ltexprlemupu  7884  ltexprlemdisj  7886  ltexprlemloc  7887  ltexprlemfl  7889  ltexprlemrl  7890  ltexprlemfu  7891  ltexprlemru  7892  addcanprleml  7894  addcanprlemu  7895  prplnqu  7900  recexprlemloc  7911  recexprlem1ssl  7913  recexprlem1ssu  7914  recexprlemss1l  7915  recexprlemss1u  7916  aptiprleml  7919  aptiprlemu  7920  cauappcvgprlemloc  7932  cauappcvgprlemladdru  7936  cauappcvgprlemladdrl  7937  caucvgprlemloc  7955  caucvgprlemladdrl  7958  caucvgprprlemml  7974  caucvgprprlemloc  7983  00sr  8049  map2psrprg  8085  suplocsrlempr  8087  suplocsrlem  8088  adddir  8230  axsuploc  8311  eqle  8330  le2tri3i  8347  mul4  8370  muladd11  8371  cnegexlem3  8415  addsub12  8451  2addsub  8452  addsubeq4  8453  subadd4  8482  negcon1  8490  negdi2  8496  negsubdi2  8497  neg2sub  8498  renegcl  8499  muladd  8622  subdir  8624  gt0ne0  8666  ltnegcon1  8702  lenegcon1  8705  eqord1  8722  eqord2  8723  recexre  8817  ltmul1  8831  recexap  8892  div12ap  8933  rerecapb  9082  p1le  9088  ltmul2  9095  gt0div  9109  ge0div  9110  zlem1lt  9597  nnaddm1cl  9602  zdceq  9616  gtndiv  9636  prime  9640  msqznn  9641  btwnz  9660  uzss  9838  eluzadd  9846  nn0pzuz  9882  supinfneg  9890  infsupneg  9891  divfnzn  9916  qnegcl  9931  qreccl  9937  elpqb  9945  xaddass  10165  xleadd1a  10169  xlesubadd  10179  elico2  10233  iccss  10237  iccsupr  10262  elfz5  10314  fznn  10386  difelfznle  10432  fzoaddel  10495  elincfzoext  10501  qdceq  10567  qbtwnxr  10580  flqbi2  10614  adddivflid  10615  fldivnn0  10618  divfl0  10619  flqmulnn0  10622  fldivnn0le  10626  fldiv4p1lem1div2  10628  ceiqle  10638  flqdiv  10646  modqmulnn  10667  frecuzrdgtcl  10737  frecuzrdgsuc  10739  frecuzrdgdomlem  10742  frecuzrdgfunlem  10744  frecuzrdgsuctlem  10748  seqm1g  10799  seq3caopr2  10818  seqcaopr2g  10819  iseqf1olemkle  10822  seq3f1olemp  10840  seqf1oglem2  10845  seqf1og  10846  seq3id  10850  seq3z  10853  expap0  10894  mulexp  10903  mulexpzap  10904  expmul  10909  leexp1a  10919  expubnd  10921  zesq  10983  bernneq  10985  bernneq3  10987  modqexp  10991  facdiv  11063  facndiv  11064  faclbnd3  11068  faclbnd6  11069  bccmpl  11079  bcpasc  11091  bccl  11092  seq3coll  11169  fundm2domnop  11176  wrdsymb1  11216  ccatfv0  11246  ccatrn  11252  ccat2s1cl  11276  lswccats1fst  11287  swrdspsleq  11314  pfxtrcfv  11340  pfxsuffeqwrdeq  11345  pfxlswccat  11360  wrdeqs1cat  11367  cats1un  11368  swrdccatin1  11372  pfxccatin12lem4  11373  swrdccatin2  11376  pfxccatin12  11380  swrdccat  11382  shftlem  11456  ovshftex  11459  shftval4  11468  shftf  11470  shftcan2  11475  crim  11498  mulreap  11504  remul2  11513  immul2  11520  cjexp  11533  caucvgre  11621  r19.2uz  11633  sqrtsq2  11683  absnid  11713  absexp  11719  nn0abscl  11725  abslt  11728  lenegsq  11735  cau3lem  11754  minmax  11870  xrmaxadd  11901  clim  11921  climshftlemg  11942  climcn1  11948  climcn1lem  11959  clim2ser  11977  clim2ser2  11978  iserex  11979  isermulc2  11980  climub  11984  climcaucn  11991  serf0  11992  summodclem3  12021  summodclem2a  12022  summodclem2  12023  summodc  12024  fsum3  12028  fsumf1o  12031  fisumss  12033  isumss2  12034  fsumcl2lem  12039  fsumadd  12047  fsumsplit  12048  isummulc2  12067  fsum2d  12076  fsummulc2  12089  telfsumo  12107  fsumparts  12111  hash2iun1dif1  12121  bcxmas  12130  isumshft  12131  isumsplit  12132  expcnvap0  12143  geolim  12152  geolim2  12153  cvgratnnlemmn  12166  cvgratnnlemseq  12167  mertenslemi1  12176  mertenslem2  12177  mertensabs  12178  clim2divap  12181  prodmodclem3  12216  prodmodclem2a  12217  fprodseq  12224  fprodf1o  12229  fprodmul  12232  fprodsplitdc  12237  efcllemp  12299  reefcl  12309  efcj  12314  efaddlem  12315  efexp  12323  reeftlcl  12330  eftlub  12331  efsep  12332  effsumlt  12333  eflegeo  12342  retanclap  12363  demoivre  12414  demoivreALT  12415  eirraplem  12418  dvdsval3  12432  p1modz1  12435  iddvdsexp  12456  alzdvds  12495  addmodlteqALT  12500  nnehalf  12545  nno  12547  ndvdsadd  12572  bitsp1e  12593  bitsp1o  12594  bitsinv1  12603  divgcdnnr  12627  neggcd  12634  gcdabs  12639  bezoutlemmain  12649  bezoutlemaz  12654  bezoutlembz  12655  gcdmultiplez  12672  gcdzeq  12673  dvdssq  12682  nninfctlemfo  12691  algrf  12697  algcvg  12700  algcvga  12703  algfx  12704  eucalgf  12707  eucalgcvga  12710  neglcm  12727  lcmabs  12728  lcmdvds  12731  lcmgcdeq  12735  qredeq  12748  isprm3  12770  coprm  12796  prmrp  12797  isprm6  12799  prmdvdsexpb  12801  rpexp  12805  cncongrprm  12809  sqrt2irraplemnn  12831  phibndlem  12868  phiprmpw  12874  eulerthlemh  12883  eulerthlemth  12884  fermltl  12886  prmdivdiv  12889  modprm1div  12900  m1dvdsndvds  12901  coprimeprodsq  12910  pczpre  12950  pczcl  12951  pcexp  12962  pczdvds  12967  pczndvds  12969  pczndvds2  12971  pcdvdsb  12973  pcneg  12978  pcprmpw  12987  difsqpwdvds  12991  pcmptcl  12995  pcprod  12999  fldivp1  13001  infpnlem2  13013  1arithlem4  13019  ennnfonelemrn  13120  topnidg  13415  pwselbasb  13456  pwsplusgval  13458  pwsmulrval  13459  imasaddfnlemg  13477  imasaddflemg  13479  qusin  13489  mgmlrid  13542  mndass  13587  prdsidlem  13610  mhmco  13653  gsumsubm  13657  gsumwcl  13660  gsumwmhm  13661  grpass  13672  grpinvex  13673  dfgrp2  13690  grplid  13694  grprid  13695  grprcan  13700  grpinvssd  13740  grpinvval2  13746  prdsinvlem  13771  pwsinvg  13775  mhmid  13782  mhmmnd  13783  ghmgrp  13785  mulgnn  13793  mulgnnp1  13797  mulgnegnn  13799  mulgnnsubcl  13801  mulgz  13817  issubg2m  13856  issubg4m  13860  subgintm  13865  nmzbi  13876  eqger  13891  eqgid  13893  eqgen  13894  qusgrp  13899  qusadd  13901  qusinv  13903  qussub  13904  ghminv  13917  ghmsub  13918  ghmrn  13924  resghm2b  13929  ghmf1  13940  conjsubg  13944  conjsubgen  13945  qusghm  13949  cmncom  13969  ablsubadd  13979  ablsubsub23  13992  ghmcmn  13994  gsumfzreidx  14004  mgpress  14025  srg1expzeq1  14089  ringinvnz1ne0  14143  ringinvnzdiv  14144  dvdsrd  14189  dvdsunit  14207  unitinvcl  14218  unitinvinv  14219  unitlinv  14221  unitrinv  14222  rhmunitinv  14273  subrngintm  14307  subrg1  14326  subrguss  14331  subrginv  14332  subrgunit  14334  subrgugrp  14335  subrgintm  14338  resrhm  14343  resrhm2b  14344  lmodass  14399  lmodlcan  14400  lmod0vlid  14414  lmod0vrid  14415  lmod0vid  14416  lmodvs0  14418  lcomf  14423  lmodvnegcl  14424  lmodvnegid  14425  lmodvsubadd  14434  lmodsubid  14443  lss1d  14479  lspval  14486  lspsnel6  14504  lspsnneg  14516  sralmod  14546  dflidl2rng  14577  lidlacl  14580  dflidl2  14584  df2idl2  14605  qusmul2  14625  quscrng  14629  cnfldmulg  14672  znf1o  14747  znidom  14753  psraddcl  14781  psr0lid  14783  tgss3  14889  clsval  14922  clsss3  14941  neiss2  14953  resttop  14981  resttopon2  14989  lmconst  15027  cnima  15031  cnntri  15035  cncnp  15041  cnrest  15046  cndis  15052  lmss  15057  lmff  15060  lmtopcnp  15061  txcnp  15082  upxp  15083  uptx  15085  cnmpt11  15094  hmeoima  15121  hmeoopn  15122  hmeocld  15123  hmeontr  15124  hmeoimaf1o  15125  mettri2  15173  met0  15175  metres2  15192  blpnf  15211  xblss2ps  15215  xblss2  15216  blbas  15244  blres  15245  xmetec  15248  mopnss  15261  xmstri2  15281  mstri2  15282  xmstri  15283  mstri  15284  xmstri3  15285  mstri3  15286  msrtri  15287  mopni3  15295  unimopn  15297  comet  15310  bdxmet  15312  climcncf  15395  dedekindeulemuub  15428  dedekindicclemuub  15437  ivthdichlem  15462  dvfgg  15499  dvidlemap  15502  dvidrelem  15503  dvidsslem  15504  dvfre  15521  dvmptfsum  15536  plyadd  15562  plymul  15563  reeff1olem  15582  reeff1o  15584  sinperlem  15619  abssinper  15657  reexplog  15682  relogexp  15683  cxpexpnn  15707  cxprec  15721  rpcxpmul2  15724  abscxp  15726  wilthlem1  15794  sgmval2  15798  sgmnncl  15802  0sgmppw  15807  perfectlem1  15813  lgsdir  15854  lgsprme0  15861  lgsdinn0  15867  gausslemma2dlem3  15882  gausslemma2dlem5a  15884  2lgslem1a2  15906  2lgslem1a  15907  2lgslem3  15920  2lgs  15923  umgredgprv  16056  umgrislfupgrdom  16072  uspgredgiedg  16119  uspgriedgedg  16120  usgrislfuspgrdom  16131  usgredg2en  16136  usgredgprv  16137  usgrpredgv  16139  usgredg  16141  usgrnloopv  16142  usgredgne  16145  usgredg3  16155  usgredgedg  16168  usgredgdomord  16171  usgr1vr  16189  subgruhgrfun  16209  subupgr  16214  subumgr  16215  subusgr  16216  umgrwlknloop  16309  wlkres  16320  clwwlkccatlem  16341  clwwlkccat  16342  depindlem1  16447  depindlem2  16448  depindlem3  16449  bj-inex  16623  bj-nn0suc  16680  bj-nn0sucALT  16694  trilpolemeq1  16772  trilpolemlt1  16773  trirec0  16776  nconstwlpolemgt0  16797