Theorem anassrs 489

Description: Associative law for conjunction applied to antecedent (eliminates syllogism).

Hypothesis

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

Assertion

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

Proof of Theorem anassrs

Step	Hyp	Ref	Expression
1		anassrs.1	. . 3 |- ((ph /\ (ps /\ ch)) -> th)
2	1	exp32 408	. 2 |- (ph -> (ps -> (ch -> th)))
3	2	imp31 389	1 |- (((ph /\ ps) /\ ch) -> th)

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  anabsan2 563  mpanr1 774  mpanr2 776  2ralbida 2137  2rexbidva 2139  sspr 3144  tfindsg2 3945  imainss 4331  fnex 4535  f1oiso 4881  oalim 5212  omlim 5213  oaass 5243  oarec 5244  omlimcl 5257  omass 5259  oelim2 5270  oeoa 5272  oeoelem 5273  undom 5497  sbthlem4 5513  mapenlem1 5583  mapenlem2 5584  mapxpen 5589  mapunen 5596  aceq5 5902  ondomon 6008  ltexprlem6 6299  recexsrlem 6364  recextlem2 6875  uzind3OLD 7421  qreccl 7453  uz11 7601  fzrevral 7698  ser1add2i 7751  ser1addi 7752  shftf 7764  seqzrn2 7799  cau5ii 8169  cau5i 8171  cvg2i 8174  faclbnd4lem4 8203  fsumcmpndx2 8302  clm4lei 8341  2climnn 8362  2climnn0 8363  climrecl 8370  climge0 8372  climmullem3 8382  climmullem5 8384  caucvglem6 8422  caucvgi 8423  cvgratlem1 8512  fsum0diaglem2 8519  fsum0diag4 8523  elcncf1di 8532  acdc5lem1 8760  infxpidmlem11 8831  basgen2 8909  txbas 8933  neips 9003  neindisj 9007  islp2 9023  cnpco 9046  blrn3 9124  blssex 9131  isopn4 9139  metcnplem 9164  metcnp 9165  metcnp3 9174  lmbr 9206  lmnn 9213  iscau5 9219  iscaunns 9222  lmss 9231  causs 9233  lmle 9238  metelcls 9243  metcnp4 9248  xpcn 9254  cmsss 9275  grplcan 9359  nvmul0or 9604  nvcni 9661  nvcni2 9662  nvcni3 9663  nvlmle 9665  sspival 9736  nmosetre 9766  0lno 9790  blocni 9805  minveclem9 9898  minveclem27 9916  minveclem28 9917  htthlem7 9973  fipreima 10175  dif1card 10177  uptx 10226  cncomp 10331  hcau2 10688  shsel3 10912  homulcl 11322  adjsym 11396  cnvadj 11453  lnopl 11475  unoplin 11481  counop 11482  lnfnl 11492  hmoplin 11503  hmopm 11583  nmophmi 11598  lnopconi 11600  lnfnconi 11627  riesz3i 11632  leopmul 11705  hstle 11802  mdsl0 11882  mdslmd1lem2 11898  atcvatlem 11957  irredi 11966  atcvat4i 11969  cdj1i 12005  fseq1cl 13619  dvdsnegb 13672  gcdcllem1 13718  eucalgf 13751  eucalginv 13752  eucalglt 13753  isprm2lem 13774  dfon2lem6 13854  tz6.26 13913  poseq 13954  nocvxminlem 14028  axfelem15 14045  axfelem16 14046  cnsubsp2 15427  topfneec 15501  neibastop1 15518  limfilcf 15587  fmfnfmlem4 15597  fcluscf 15612  flimfcls 15613  fcluscomplem 15620  fcluscomp 15621  isfclusf 15625  fclsfcnp 15631  anass1rs 15646  cover2 15673  foco2 15686  cocanfo 15689  difxp 15690  f1elima 15719  upixp 15729  fisupg 15748  fipreimaOLD 15756  inficl 15757  infmrgelb 15766  fimax2g 15769  pofun 15772  fimaxre 15774  filbcmb 15776  fzsplit 15792  sdclem1 15809  sdc 15811  fdc 15812  fdc1 15813  seqpo 15814  incsequz 15815  incsequz2 15816  neificl 15841  metf1o 15843  blhalf 15846  mettrifi 15847  mettrifi2 15848  geomcau 15849  lmclim2 15850  cnimass 15888  cnresima 15891  cnss 15892  lmtlm 15908  txsubsp 15912  txcld 15914  txmet 15925  sstotbnd 15936  totbndss 15937  isbnd3 15941  bndss 15942  totbndbnd 15944  ismtyhmeolem 15950  ismtybndlem 15952  ismtyres 15954  heiborlem15 15969  heiborlem23 15977  heiborlem30 15984  heiborlem35 15989  heiborlem36 15990  heiborlem37 15991  rrncms 16019  rrntotbndlem1 16020  rrntotbndlem2 16021  rrntotbnd 16022  exidreslem 16030  ghomco 16040  phtpycom 16050  phtpycolem5 16055  reparpht 16065  pcohtpylem2 16081  pcoass 16085  pi1gp 16095  isdivrng3 16112  rngisocnv 16135  isidlc 16163  idlnegcl 16170  divrngidl 16176  intidl 16177  unichnidl 16179  keridl 16180  igenmin 16212  prnc 16215  ispridlc 16218  glbconx 17029  atltcvr 17072  cvrat4 17076  ps2 17079  grplcanNEW 17134  linepsub 17232  pexmidOLD 17386

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-an 242

Copyright terms: Public domain