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

Theorem anass 393
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 392 . 2 (((𝜑𝜓) ∧ 𝜒) → (𝜑 ∧ (𝜓𝜒)))
3 id 19 . . 3 (((𝜑𝜓) ∧ 𝜒) → ((𝜑𝜓) ∧ 𝜒))
43anasss 391 . 2 ((𝜑 ∧ (𝜓𝜒)) → ((𝜑𝜓) ∧ 𝜒))
52, 4impbii 124 1 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
Colors of variables: wff set class
Syntax hints:  wa 102  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  mpan10  458  an12  526  an32  527  an13  528  an31  529  an4  551  3anass  924  sbidm  1773  4exdistr  1835  2sb5  1901  2sb5rf  1907  sbel2x  1916  r2exf  2385  r19.41  2510  ceqsex3v  2642  ceqsrex2v  2728  rexrab  2756  rexrab2  2760  rexss  3062  inass  3177  difin2  3227  difrab  3239  reupick3  3250  inssdif0im  3312  rexdifsn  3523  unidif0  3943  bnd2  3949  eqvinop  4000  copsexg  4001  uniuni  4203  rabxp  4400  elvvv  4423  rexiunxp  4500  resopab2  4679  ssrnres  4787  elxp4  4832  elxp5  4833  cnvresima  4834  mptpreima  4838  coass  4863  dff1o2  5156  eqfnfv3  5293  rexsupp  5317  isoini  5482  f1oiso  5490  oprabid  5562  dfoprab2  5577  mpt2eq123  5589  mpt2mptx  5620  resoprab2  5623  ovi3  5662  oprabex3  5781  spc2ed  5879  f1od2  5881  brtpos2  5894  xpsnen  6355  xpcomco  6360  xpassen  6364  ltexpi  6578  enq0enq  6672  enq0tr  6675  prnmaxl  6729  prnminu  6730  genpdflem  6748  ltexprlemm  6841  rexuz  8738  rexuz2  8739  rexrp  8826  elixx3g  8989  elfz2  9101  fzdifsuc  9163  fzind2  9314  divalgb  10458  gcdass  10537  lcmass  10600  isprm2  10632
  Copyright terms: Public domain W3C validator