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

Theorem anass 383
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 382 . 2 (((φ ψ) χ) → (φ (ψ χ)))
3 id 19 . . 3 (((φ ψ) χ) → ((φ ψ) χ))
43anasss 381 . 2 ((φ (ψ χ)) → ((φ ψ) χ))
52, 4impbii 117 1 (((φ ψ) χ) ↔ (φ (ψ χ)))
Colors of variables: wff set class
Syntax hints:   wa 97  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  mpan10  446  an12  483  an32  484  an13  485  an31  486  an4  507  3anass  877  sbidm  1713  4exdistr  1775  2sb5  1841  2sb5rf  1847  sbel2x  1856  r2exf  2320  r19.41  2443  ceqsex3v  2573  ceqsrex2v  2653  rexrab  2681  rexrab2  2685  rexss  2984  inass  3124  difin2  3176  difrab  3188  reupick3  3199  inssdif0im  3268  rexdifsn  3473  unidif0  3894  bnd2  3900  eqvinop  3954  copsexg  3955  uniuni  4133  rabxp  4307  elvvv  4330  rexiunxp  4405  resopab2  4582  ssrnres  4690  elxp4  4735  elxp5  4736  cnvresima  4737  mptpreima  4741  coass  4766  dff1o2  5056  eqfnfv3  5192  rexsupp  5216  isoini  5382  f1oiso  5390  oprabid  5461  dfoprab2  5475  mpt2eq123  5487  mpt2mptx  5518  resoprab2  5521  ovi3  5560  oprabex3  5679  brtpos2  5788  ltexpi  6197  enq0enq  6286  enq0tr  6289  prnmaxl  6342  prnminu  6343  genpdflem  6361  ltexprlemm  6437
  Copyright terms: Public domain W3C validator