MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  anass Unicode version

Theorem anass 631
Description: Associative law for conjunction. Theorem *4.32 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
Assertion
Ref Expression
anass  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )

Proof of Theorem anass
StepHypRef Expression
1 id 20 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  -> 
( ph  /\  ( ps  /\  ch ) ) )
21anassrs 630 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  -> 
( ph  /\  ( ps  /\  ch ) ) )
3 id 20 . . 3  |-  ( ( ( ph  /\  ps )  /\  ch )  -> 
( ( ph  /\  ps )  /\  ch )
)
43anasss 629 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  -> 
( ( ph  /\  ps )  /\  ch )
)
52, 4impbii 181 1  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359
This theorem is referenced by:  an12  773  an32  774  an13  775  an31  776  an4  798  3anass  940  4exdistrOLD  1931  2sb5  2169  2sb5rf  2175  sbel2x  2183  r2exf  2710  r19.41  2828  ceqsex3v  2962  ceqsrex2v  3039  rexrab  3066  rexrab2  3070  2reu5  3110  rexss  3378  inass  3519  indifdir  3565  difin2  3571  difrab  3583  reupick3  3594  inssdif0  3663  rexdifsn  3899  eqvinop  4409  copsexg  4410  wefrc  4544  uniuni  4683  reusv2lem4  4694  reusv2  4696  rabxp  4881  elvvv  4904  resopab2  5157  ssrnres  5276  elxp4  5324  elxp5  5325  cnvresima  5326  mptpreima  5330  coass  5355  imadif  5495  dff1o2  5646  eqfnfv3  5796  rexsupp  5822  isoini  6025  f1oiso  6038  oprabid  6072  dfoprab2  6088  mpt2eq123  6100  mpt2mptx  6131  resoprab2  6134  oprabex3  6155  ov3  6177  difxp  6347  frxp  6423  brtpos2  6452  oeeui  6812  oeeu  6813  omabs  6857  mapsnen  7151  xpsnen  7159  xpcomco  7165  xpassen  7169  wemapso2lem  7483  epfrs  7631  bnd2  7781  aceq1  7962  dfac5lem1  7968  dfac5lem2  7969  dfac5lem5  7972  kmlem3  7996  kmlem14  8007  pwfseqlem1  8497  ltexpi  8743  ltexprlem4  8880  axaddf  8984  axmulf  8985  rexuz  10491  rexuz2  10492  nnwos  10508  zmin  10534  rexrp  10595  elixx3g  10893  elfz2  11014  fzind2  11161  hashbclem  11664  resqrex  12019  rlim  12252  divalglem10  12885  divalgb  12887  gcdass  13008  isprm2  13050  infpn2  13244  ispos2  14368  issubg3  14923  resscntz  15093  subgdmdprd  15555  dprd2d2  15565  dfrhm2  15784  isassa  16338  aspval2  16368  istps2OLD  16949  istps3OLD  16950  ntreq0  17104  cmpcov2  17415  llyi  17498  nllyi  17499  subislly  17505  ptpjpre1  17564  tx1cn  17602  tx2cn  17603  txtube  17633  txkgen  17645  trfil2  17880  elflim2  17957  cnpflfi  17992  isfcls  18002  cnextcn  18059  istlm  18175  blres  18422  metrest  18515  isnlm  18672  elcncf1di  18886  elpi1  19031  iscph  19094  cfilucfil3OLD  19232  cfilucfil3  19233  itg1climres  19567  itgsubst  19894  ulmdvlem3  20279  cubic  20650  vmasum  20961  logfac2  20962  lgsquadlem1  21099  lgsquadlem2  21100  nb3grapr2  21424  trls  21497  3v3e3cycl2  21612  grpoidinvlem3  21755  h2hlm  22444  issh  22671  issh3  22683  ocsh  22746  cvbr2  23747  cvnbtwn2  23751  mdsl2i  23786  cvmdi  23788  mdsymlem2  23868  sumdmdii  23879  1stpreima  24056  2ndpreima  24057  1stmbfm  24571  2ndmbfm  24572  dya2iocnei  24593  iscvm  24907  axacprim  25117  dfpo2  25334  dfdm5  25354  dfrn5  25355  preduz  25422  wfi  25429  frind  25465  sltval2  25532  nofulllem5  25582  dfon3  25654  elfuns  25676  brimg  25698  brsuccf  25702  dfrdg4  25711  tfrqfree  25712  axcontlem5  25819  ifscgr  25890  cgrxfr  25901  segcon2  25951  seglecgr12im  25956  segletr  25960  ellines  25998  itg2addnc  26166  areacirclem6  26194  neifg  26298  isbnd2  26390  heibor1  26417  prtlem70  26596  prtlem100  26602  diophrex  26732  rmxdioph  26985  dford4  26998  islmodfg  27043  islssfg2  27045  isdomn3  27399  fgraphopab  27405  2sbc5g  27492  rexdifpr  27955  usgra2pth0  28050  usg2spthonot0  28094  usg2spthonot1  28095  1to2vfriswmgra  28118  usgreg2spot  28178  bnj250  28783  bnj251  28784  bnj256  28788  bnj168  28815  2sb5NEW7  29322  sbel2xNEW7  29327  2sb5rfOLD7  29458  lsateln0  29490  islshpat  29512  lcvbr2  29517  lcvnbtwn2  29522  isopos  29675  cvrval2  29769  cvrnbtwn2  29770  ishlat2  29848  3dim0  29951  islvol5  30073  pmapjat1  30347  pclcmpatN  30395  pclfinclN  30444  cdlemefrs29pre00  30889  cdlemefrs29bpre0  30890  cdlemefrs29cpre1  30892  cdleme32a  30935  cdlemftr3  31059  dvhopellsm  31612  dibelval3  31642  diblsmopel  31666  mapdvalc  32124  mapdval4N  32127  mapdordlem1a  32129
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator