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

Theorem anass 680
Description: Associative law for conjunction. Theorem *4.32 of [WhiteheadRussell] p. 118. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
Assertion
Ref Expression
anass (((𝜑𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))

Proof of Theorem anass
StepHypRef Expression
1 id 22 . . 3 ((𝜑 ∧ (𝜓𝜒)) → (𝜑 ∧ (𝜓𝜒)))
21anassrs 679 . 2 (((𝜑𝜓) ∧ 𝜒) → (𝜑 ∧ (𝜓𝜒)))
3 id 22 . . 3 (((𝜑𝜓) ∧ 𝜒) → ((𝜑𝜓) ∧ 𝜒))
43anasss 678 . 2 ((𝜑 ∧ (𝜓𝜒)) → ((𝜑𝜓) ∧ 𝜒))
52, 4impbii 199 1 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-an 386
This theorem is referenced by:  an12  837  an32  838  an13  839  an31  840  bianass  841  an4  864  3anass  1040  3an4anass  1289  2sb5  2441  r19.41v  3084  r19.41  3085  ceqsex3v  3241  ceqsrex2v  3332  rexrab  3364  rexrab2  3368  2reu5  3410  rexss  3661  inass  3815  indifdir  3875  difin2  3882  difrab  3893  reupick3  3904  inssdif0  3938  rexdifpr  4196  rexdifsn  4314  reusv2lem4  4863  reusv2  4865  eqvinop  4945  copsexg  4946  wefrc  5098  rabxp  5144  elvvv  5168  resopab2  5436  difxp  5546  ssrnres  5560  mptpreima  5616  coass  5642  wfi  5701  imadif  5961  dff1o2  6129  eqfnfv3  6299  isoini  6573  f1oiso  6586  oprabid  6662  dfoprab2  6686  mpt2eq123  6699  mpt2mptx  6736  resoprab2  6742  ov3  6782  uniuni  6956  elxp4  7095  elxp5  7096  oprabex3  7142  frxp  7272  rexsupp  7298  brtpos2  7343  oeeui  7667  oeeu  7668  omabs  7712  mapsnen  8020  xpsnen  8029  xpcomco  8035  xpassen  8039  wemapsolem  8440  epfrs  8592  bnd2  8741  aceq1  8925  dfac5lem1  8931  dfac5lem2  8932  dfac5lem5  8935  kmlem3  8959  kmlem14  8970  pwfseqlem1  9465  ltexpi  9709  ltexprlem4  9846  axaddf  9951  axmulf  9952  rexuz  11723  rexuz2  11724  nnwos  11740  zmin  11769  rexrp  11838  elixx3g  12173  elfz2  12318  preduz  12445  fzind2  12569  hashbclem  13219  resqrex  13972  rlim  14207  divalglem10  15106  divalgb  15108  gcdass  15245  lcmass  15308  isprm2  15376  infpn2  15598  ispos2  16929  issubg3  17593  resscntz  17745  subgdmdprd  18414  dprd2d2  18424  dfrhm2  18698  isassa  19296  aspval2  19328  fvmptnn04if  20635  ntreq0  20862  cmpcov2  21174  llyi  21258  nllyi  21259  subislly  21265  ptpjpre1  21355  tx1cn  21393  tx2cn  21394  txtube  21424  txkgen  21436  trfil2  21672  elflim2  21749  cnpflfi  21784  isfcls  21794  cnextcn  21852  istlm  21969  blres  22217  metrest  22310  isnlm  22460  elcncf1di  22679  elpi1  22826  isclmp  22878  iscvsp  22909  isncvsngp  22930  iscph  22951  cfilucfil3  23098  itg1climres  23462  itgsubst  23793  ulmdvlem3  24137  cubic  24557  vmasum  24922  logfac2  24923  lgsquadlem1  25086  lgsquadlem2  25087  legov  25461  ltgov  25473  perpln1  25586  axcontlem5  25829  nbgrel  26219  nbusgredgeu0  26251  nb3grpr2  26266  finsumvtxdg2ssteplem3  26424  usgr2pth0  26642  isclwlke  26654  wwlksnfi  26782  wlksnwwlknvbij  26784  elwwlks2ons3  26829  wpthswwlks2on  26835  usgr2wspthon  26839  rusgrnumwwlkl1  26844  isclwwlks  26861  isclwwlksnx  26870  clwwlksvbij  26902  iseupthf1o  27042  fusgr2wsp2nb  27172  numclwwlkovf2  27189  grpoidinvlem3  27330  h2hlm  27807  issh  28035  issh3  28046  ocsh  28112  cvbr2  29112  cvnbtwn2  29116  mdsl2i  29151  cvmdi  29153  mdsymlem2  29233  sumdmdii  29244  spc2ed  29282  rabrab  29310  difrab2  29311  disjunsn  29379  mpt2mptxf  29451  1stpreima  29458  2ndpreima  29459  f1od2  29473  nndiffz1  29522  omndmul2  29686  smatrcl  29836  crefdf  29889  pcmplfin  29901  1stmbfm  30296  2ndmbfm  30297  dya2iocnei  30318  eulerpartlemgvv  30412  eulerpartlemn  30417  bnj250  30741  bnj251  30742  bnj256  30746  bnj168  30772  iscvm  31215  axacprim  31558  dfpo2  31620  dfdm5  31650  dfrn5  31651  elima4  31653  imaindm  31656  frind  31714  sltval2  31783  madeval2  31910  dfon3  31974  brimg  32019  dfrecs2  32032  dfrdg4  32033  ifscgr  32126  cgrxfr  32137  segcon2  32187  seglecgr12im  32192  segletr  32196  ellines  32234  neifg  32341  bj-dfmpt2a  33046  topdifinffinlem  33166  icorempt2  33170  finxpreclem6  33204  wl-cases2-dnf  33266  curf  33358  uncf  33359  matunitlindflem2  33377  matunitlindf  33378  poimirlem26  33406  poimirlem28  33408  poimirlem30  33410  poimirlem32  33412  poimir  33413  itg2addnc  33435  ftc1anclem5  33460  ftc1anc  33464  areacirclem5  33475  isbnd2  33553  heibor1  33580  prtlem70  33958  prtlem100  33962  lsateln0  34101  islshpat  34123  lcvbr2  34128  lcvnbtwn2  34133  isopos  34286  cvrval2  34380  cvrnbtwn2  34381  ishlat2  34459  3dim0  34562  islvol5  34684  pmapjat1  34958  pclcmpatN  35006  pclfinclN  35055  cdlemefrs29pre00  35502  cdlemefrs29bpre0  35503  cdlemefrs29cpre1  35505  cdleme32a  35548  cdlemftr3  35672  dvhopellsm  36225  dibelval3  36255  diblsmopel  36279  mapdvalc  36737  mapdval4N  36740  mapdordlem1a  36742  diophrex  37158  rmxdioph  37402  dford4  37415  islmodfg  37458  islssfg2  37460  isdomn3  37601  fgraphopab  37607  k0004lem1  38265  2sbc5g  38437  mapsnend  39207  limcrecl  39661  dvnmul  39921  dvnprodlem2  39925  fourierdlem83  40169  iundjiun  40440  sprvalpwn0  41498  isrnghm  41657  isrnghmmul  41658  rngcinv  41746  rngcinvALTV  41758  ringcinv  41797  ringcinvALTV  41821  mpt2mptx2  41878
  Copyright terms: Public domain W3C validator