ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  anass Unicode 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  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )

Proof of Theorem anass
StepHypRef Expression
1 id 19 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  -> 
( ph  /\  ( ps  /\  ch ) ) )
21anassrs 392 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  -> 
( ph  /\  ( ps  /\  ch ) ) )
3 id 19 . . 3  |-  ( ( ( ph  /\  ps )  /\  ch )  -> 
( ( ph  /\  ps )  /\  ch )
)
43anasss 391 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  -> 
( ( ph  /\  ps )  /\  ch )
)
52, 4impbii 124 1  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )
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  3183  difin2  3233  difrab  3245  reupick3  3256  inssdif0im  3318  rexdifsn  3529  unidif0  3949  bnd2  3955  eqvinop  4006  copsexg  4007  uniuni  4209  rabxp  4406  elvvv  4429  rexiunxp  4506  resopab2  4685  ssrnres  4793  elxp4  4838  elxp5  4839  cnvresima  4840  mptpreima  4844  coass  4869  dff1o2  5162  eqfnfv3  5299  rexsupp  5323  isoini  5488  f1oiso  5496  oprabid  5568  dfoprab2  5583  mpt2eq123  5595  mpt2mptx  5626  resoprab2  5629  ovi3  5668  oprabex3  5787  spc2ed  5885  f1od2  5887  brtpos2  5900  xpsnen  6365  xpcomco  6370  xpassen  6374  ltexpi  6589  enq0enq  6683  enq0tr  6686  prnmaxl  6740  prnminu  6741  genpdflem  6759  ltexprlemm  6852  rexuz  8749  rexuz2  8750  rexrp  8837  elixx3g  9000  elfz2  9112  fzdifsuc  9174  fzind2  9325  divalgb  10469  gcdass  10548  lcmass  10611  isprm2  10643
  Copyright terms: Public domain W3C validator