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

Theorem anass 633
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 21 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  -> 
( ph  /\  ( ps  /\  ch ) ) )
21anassrs 632 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  -> 
( ph  /\  ( ps  /\  ch ) ) )
3 id 21 . . 3  |-  ( ( ( ph  /\  ps )  /\  ch )  -> 
( ( ph  /\  ps )  /\  ch )
)
43anasss 631 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  -> 
( ( ph  /\  ps )  /\  ch )
)
52, 4impbii 182 1  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    /\ wa 360
This theorem is referenced by:  an12  775  an32  776  an13  777  an31  778  an4  800  3anass  943  4exdistr  2045  2sb5  2075  2sb5rf  2080  sbel2x  2088  r2exf  2552  r19.41  2665  ceqsex3v  2794  ceqsrex2v  2871  rexrab  2897  rexrab2  2901  rexss  3201  inass  3340  indifdir  3386  difin2  3391  difrab  3403  reupick3  3414  inssdif0  3482  rexdifsn  3713  eqvinop  4209  copsexg  4210  wefrc  4345  uniuni  4485  reusv2lem4  4496  reusv2  4498  rabxp  4699  elvvv  4723  resopab2  4973  ssrnres  5090  elxp4  5133  elxp5  5134  cnvresima  5135  mptpreima  5139  coass  5164  imadif  5251  dff1o2  5401  eqfnfv3  5544  rexsupp  5570  isoini  5755  f1oiso  5768  oprabid  5802  dfoprab2  5815  mpt2eq123  5827  mpt2mptx  5858  resoprab2  5861  oprabex3  5882  ov3  5904  difxp  6073  frxp  6145  brtpos2  6160  oeeui  6554  oeeu  6555  omabs  6599  mapsnen  6892  xpsnen  6900  xpcomco  6906  xpassen  6910  wemapso2lem  7219  epfrs  7367  bnd2  7517  aceq1  7698  dfac5lem1  7704  dfac5lem2  7705  dfac5lem5  7708  kmlem3  7732  kmlem14  7743  pwfseqlem1  8234  ltexpi  8480  ltexprlem4  8617  axaddf  8721  axmulf  8722  rexuz  10222  rexuz2  10223  nnwos  10239  zmin  10265  rexrp  10326  elixx3g  10621  elfz2  10741  fzind2  10875  hashbclem  11341  resqrex  11687  rlim  11920  divalglem10  12549  divalgb  12551  gcdass  12672  isprm2  12714  infpn2  12908  ispos2  14030  issubg3  14585  resscntz  14755  subgdmdprd  15217  dprd2d2  15227  dfrhm2  15446  isassa  16004  aspval2  16034  istps2OLD  16607  istps3OLD  16608  ntreq0  16762  cmpcov2  17065  llyi  17148  nllyi  17149  subislly  17155  ptpjpre1  17214  tx1cn  17251  tx2cn  17252  txtube  17282  txkgen  17294  trfil2  17530  elflim2  17607  cnpflfi  17642  isfcls  17652  istlm  17815  blres  17925  metrest  18018  isnlm  18134  elcncf1di  18347  elpi1  18491  iscph  18554  itg1climres  19017  itgsubst  19344  ulmdvlem3  19727  cubic  20093  vmasum  20403  logfac2  20404  lgsquadlem1  20541  lgsquadlem2  20542  grpoidinvlem3  20819  h2hlm  21506  issh  21733  issh3  21745  ocsh  21808  cvbr2  22809  cvnbtwn2  22813  mdsl2i  22848  cvmdi  22850  mdsymlem2  22930  sumdmdii  22941  iscvm  23148  axacprim  23411  dfpo2  23469  dfdm5  23487  dfrn5  23488  preduz  23555  wfi  23562  frind  23598  sltval2  23664  dfon3  23794  brimg  23837  brsuccf  23841  dfrdg4  23849  tfrqfree  23850  axcontlem5  23957  ifscgr  24028  cgrxfr  24039  segcon2  24089  seglecgr12im  24094  segletr  24098  ellines  24136  eqvinopb  24317  copsexgb  24318  elo  24393  dfdir2  24644  cnvresimaOLD  25579  neifg  25673  isbnd2  25860  heibor1  25887  prtlem70  26068  prtlem100  26074  diophrex  26208  rmxdioph  26462  dford4  26475  islmodfg  26520  islssfg2  26522  isdomn3  26876  fgraphopab  26882  2sbc5g  26970  bnj250  27759  bnj251  27760  bnj256  27764  bnj168  27791  lsateln0  28336  islshpat  28358  lcvbr2  28363  lcvnbtwn2  28368  isopos  28521  cvrval2  28615  cvrnbtwn2  28616  ishlat2  28694  3dim0  28797  islvol5  28919  pmapjat1  29193  pclcmpatN  29241  pclfinclN  29290  cdlemefrs29pre00  29735  cdlemefrs29bpre0  29736  cdlemefrs29cpre1  29738  cdleme32a  29781  cdlemftr3  29905  dvhopellsm  30458  dibelval3  30488  diblsmopel  30512  mapdvalc  30970  mapdval4N  30973  mapdordlem1a  30975
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-an 362
  Copyright terms: Public domain W3C validator