ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  anass GIF version

Theorem anass 398
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 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))

Proof of Theorem anass
StepHypRef Expression
1 id 19 . . 3 ((𝜑 ∧ (𝜓𝜒)) → (𝜑 ∧ (𝜓𝜒)))
21anassrs 397 . 2 (((𝜑𝜓) ∧ 𝜒) → (𝜑 ∧ (𝜓𝜒)))
3 id 19 . . 3 (((𝜑𝜓) ∧ 𝜒) → ((𝜑𝜓) ∧ 𝜒))
43anasss 396 . 2 ((𝜑 ∧ (𝜓𝜒)) → ((𝜑𝜓) ∧ 𝜒))
52, 4impbii 125 1 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
Colors of variables: wff set class
Syntax hints:  wa 103  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  mpan10  465  an12  550  an32  551  an13  552  an31  553  an4  575  3anass  966  sbidm  1823  4exdistr  1888  2sb5  1958  2sb5rf  1964  sbel2x  1973  r2exf  2453  r19.41  2586  ceqsex3v  2728  ceqsrex2v  2817  rexrab  2847  rexrab2  2851  rexss  3164  inass  3286  difin2  3338  difrab  3350  reupick3  3361  inssdif0im  3430  rexdifsn  3655  unidif0  4091  bnd2  4097  eqvinop  4165  copsexg  4166  uniuni  4372  rabxp  4576  elvvv  4602  rexiunxp  4681  resopab2  4866  ssrnres  4981  elxp4  5026  elxp5  5027  cnvresima  5028  mptpreima  5032  coass  5057  dff1o2  5372  eqfnfv3  5520  rexsupp  5544  isoini  5719  f1oiso  5727  oprabid  5803  dfoprab2  5818  mpoeq123  5830  mpomptx  5862  resoprab2  5868  ovi3  5907  oprabex3  6027  spc2ed  6130  f1od2  6132  brtpos2  6148  mapsnen  6705  xpsnen  6715  xpcomco  6720  xpassen  6724  ltexpi  7157  enq0enq  7251  enq0tr  7254  prnmaxl  7308  prnminu  7309  genpdflem  7327  ltexprlemm  7420  suplocsrlemb  7626  axaddf  7688  axmulf  7689  rexuz  9387  rexuz2  9388  rexrp  9476  elixx3g  9696  elfz2  9809  fzdifsuc  9873  fzind2  10028  divalgb  11633  gcdass  11714  lcmass  11777  isprm2  11809  ntreq0  12315  tx1cn  12452  tx2cn  12453  blres  12617  metrest  12689  elcncf1di  12749  dedekindicclemicc  12793
  Copyright terms: Public domain W3C validator