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

Theorem anass 456
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 455 . 2 (((𝜑𝜓) ∧ 𝜒) → (𝜑 ∧ (𝜓𝜒)))
3 id 22 . . 3 (((𝜑𝜓) ∧ 𝜒) → ((𝜑𝜓) ∧ 𝜒))
43anasss 454 . 2 ((𝜑 ∧ (𝜓𝜒)) → ((𝜑𝜓) ∧ 𝜒))
52, 4impbii 200 1 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
Colors of variables: wff setvar class
Syntax hints:  wb 197  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 198  df-an 385
This theorem is referenced by:  bianass  625  an21  626  an12  627  an32  628  an13  629  an31  630  an4  638  3anass  1109  3an4anass  1122  2sb5  2290  eu6  2645  r19.41v  3288  r19.41  3289  rabrab  3316  ceqsex3v  3451  ceqsrex2v  3543  rexrab  3577  rexrab2  3581  2reu5  3625  rexss  3877  inass  4031  rexin  4051  indifdir  4096  difin2  4102  difrab  4113  reupick3  4124  inssdif0  4159  rexdifpr  4410  rexdifsn  4526  reusv2lem4  5083  reusv2  5085  eqvinop  5157  copsexg  5158  wefrc  5318  rabxp  5368  elvvv  5392  resopab2  5667  difxp  5783  ssrnres  5797  mptpreima  5856  coass  5882  wfi  5940  imadif  6194  dff1o2  6368  eqfnfv3  6545  f1ossf1o  6628  isoini  6822  f1oiso  6835  oprabid  6915  dfoprab2  6941  mpt2eq123  6954  mpt2mptx  6991  resoprab2  6997  ov3  7037  uniuni  7211  elxp4  7350  elxp5  7351  oprabex3  7397  frxp  7531  rexsupp  7557  brtpos2  7603  oeeui  7929  oeeu  7930  omabs  7974  mapsnend  8281  xpsnen  8293  xpcomco  8299  xpassen  8303  wemapsolem  8704  epfrs  8864  bnd2  9013  aceq1  9233  dfac5lem1  9239  dfac5lem2  9240  dfac5lem5  9243  kmlem3  9269  kmlem14  9280  pwfseqlem1  9775  ltexpi  10019  ltexprlem4  10156  axaddf  10261  axmulf  10262  rexuz  11976  rexuz2  11977  nnwos  11994  zmin  12023  rexrp  12087  elixx3g  12426  elfz2  12576  preduz  12705  fzind2  12830  hashbclem  13473  resqrex  14234  rlim  14469  divalglem10  15365  divalgb  15367  gcdass  15503  lcmass  15566  isprm2  15633  infpn2  15854  ispos2  17173  issubg3  17834  resscntz  17985  subgdmdprd  18655  dprd2d2  18665  dfrhm2  18941  isassa  19544  aspval2  19576  fvmptnn04if  20888  ntreq0  21116  cmpcov2  21428  llyi  21512  nllyi  21513  subislly  21519  ptpjpre1  21609  tx1cn  21647  tx2cn  21648  txtube  21678  txkgen  21690  trfil2  21925  elflim2  22002  cnpflfi  22037  isfcls  22047  cnextcn  22105  istlm  22222  blres  22470  metrest  22563  isnlm  22713  elcncf1di  22932  elpi1  23078  isclmp  23130  iscvsp  23161  isncvsngp  23182  iscph  23203  cfilucfil3  23351  itg1climres  23718  itgsubst  24049  ulmdvlem3  24393  cubic  24813  vmasum  25178  logfac2  25179  lgsquadlem1  25342  lgsquadlem2  25343  legov  25717  ltgov  25729  perpln1  25842  axcontlem5  26085  nbgrel  26472  nbgrelOLD  26473  nbusgredgeu0  26509  nb3grpr2  26524  finsumvtxdg2ssteplem3  26694  usgr2pth0  26912  isclwlke  26924  wwlksnfi  27066  wlksnwwlknvbijOLD  27069  elwwlks2ons3  27118  elwwlks2ons3OLD  27119  wpthswwlks2on  27125  wpthswwlks2onOLD  27126  usgr2wspthon  27130  rusgrnumwwlkl1  27133  isclwwlk  27150  isclwwlknx  27207  clwlknf1oclwwlkn  27271  clwwlknonel  27285  clwwlknon2x  27294  clwwlkvbij  27305  clwwlkvbijOLDOLD  27306  clwwlkvbijOLD  27307  iseupthf1o  27398  fusgr2wsp2nb  27532  grpoidinvlem3  27712  h2hlm  28188  issh  28416  issh3  28427  ocsh  28493  cvbr2  29493  cvnbtwn2  29497  mdsl2i  29532  cvmdi  29534  mdsymlem2  29614  sumdmdii  29625  spc2ed  29663  difrab2  29687  disjunsn  29755  mpt2mptxf  29827  1stpreima  29834  2ndpreima  29835  f1od2  29849  nndiffz1  29898  omndmul2  30060  smatrcl  30210  crefdf  30263  pcmplfin  30275  1stmbfm  30670  2ndmbfm  30671  dya2iocnei  30692  eulerpartlemgvv  30786  eulerpartlemn  30791  bnj250  31115  bnj251  31116  bnj256  31120  bnj168  31144  iscvm  31586  axacprim  31928  dfpo2  31989  dfdm5  32018  dfrn5  32019  elima4  32021  imaindm  32024  frpoind  32083  frind  32086  sltval2  32152  madeval2  32279  dfon3  32342  brimg  32387  dfrecs2  32400  dfrdg4  32401  ifscgr  32494  cgrxfr  32505  segcon2  32555  seglecgr12im  32560  segletr  32564  ellines  32602  neifg  32709  bj-dfmpt2a  33401  topdifinffinlem  33530  icorempt2  33534  finxpreclem6  33568  wl-cases2-dnf  33630  curf  33719  uncf  33720  matunitlindflem2  33738  matunitlindf  33739  poimirlem26  33767  poimirlem28  33769  poimirlem30  33771  poimirlem32  33773  poimir  33774  itg2addnc  33795  ftc1anclem5  33820  ftc1anc  33824  areacirclem5  33835  isbnd2  33912  heibor1  33939  anan  34339  inxpxrn  34485  prtlem70  34654  prtlem100  34657  lsateln0  34794  islshpat  34816  lcvbr2  34821  lcvnbtwn2  34826  isopos  34979  cvrval2  35073  cvrnbtwn2  35074  ishlat2  35152  3dim0  35256  islvol5  35378  pmapjat1  35652  pclcmpatN  35700  pclfinclN  35749  cdlemefrs29pre00  36194  cdlemefrs29bpre0  36195  cdlemefrs29cpre1  36197  cdleme32a  36240  cdlemftr3  36364  dvhopellsm  36916  dibelval3  36946  diblsmopel  36970  mapdvalc  37428  mapdval4N  37431  mapdordlem1a  37433  diophrex  37859  rmxdioph  38102  dford4  38115  islmodfg  38158  islssfg2  38160  isdomn3  38301  fgraphopab  38307  k0004lem1  38963  2sbc5g  39134  limcrecl  40359  dvnmul  40656  dvnprodlem2  40660  fourierdlem83  40903  iundjiun  41174  4an21  41877  sprvalpwn0  42319  isrnghm  42478  isrnghmmul  42479  rngcinv  42567  rngcinvALTV  42579  ringcinv  42618  ringcinvALTV  42642  mpt2mptx2  42699
  Copyright terms: Public domain W3C validator