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

Theorem anass 381
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 380 . 2 (((φ ψ) χ) → (φ (ψ χ)))
3 id 19 . . 3 (((φ ψ) χ) → ((φ ψ) χ))
43anasss 379 . 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  443  an12  480  an32  481  an13  482  an31  483  an4  505  3anass  873  sbidm  1707  4exdistr  1769  2sb5  1835  2sb5rf  1841  sbel2x  1850  r2exf  2314  r19.41  2437  ceqsex3v  2567  ceqsrex2v  2647  rexrab  2675  rexrab2  2679  rexss  2978  inass  3118  difin2  3170  difrab  3182  reupick3  3193  inssdif0im  3262  rexdifsn  3465  unidif0  3886  bnd2  3892  eqvinop  3946  copsexg  3947  uniuni  4124  rabxp  4298  elvvv  4321  rexiunxp  4396  resopab2  4573  ssrnres  4681  elxp4  4726  elxp5  4727  cnvresima  4728  mptpreima  4732  coass  4757  dff1o2  5047  eqfnfv3  5183  rexsupp  5207  isoini  5373  f1oiso  5381  oprabid  5452  dfoprab2  5466  mpt2eq123  5478  mpt2mptx  5509  resoprab2  5512  ovi3  5551  oprabex3  5670  brtpos2  5779  ltexpi  6186  enq0enq  6275  enq0tr  6278  prnmaxl  6331  prnminu  6332  genpdflem  6350  ltexprlemm  6426  rexrp  8089  elixx3g  8249
  Copyright terms: Public domain W3C validator