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

Theorem anass 396
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 395 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  -> 
( ph  /\  ( ps  /\  ch ) ) )
3 id 19 . . 3  |-  ( ( ( ph  /\  ps )  /\  ch )  -> 
( ( ph  /\  ps )  /\  ch )
)
43anasss 394 . 2  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  -> 
( ( ph  /\  ps )  /\  ch )
)
52, 4impbii 125 1  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 103    <-> wb 104
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  mpan10  463  an12  533  an32  534  an13  535  an31  536  an4  558  3anass  949  sbidm  1805  4exdistr  1868  2sb5  1934  2sb5rf  1940  sbel2x  1949  r2exf  2427  r19.41  2560  ceqsex3v  2699  ceqsrex2v  2787  rexrab  2816  rexrab2  2820  rexss  3130  inass  3252  difin2  3304  difrab  3316  reupick3  3327  inssdif0im  3396  rexdifsn  3621  unidif0  4051  bnd2  4057  eqvinop  4125  copsexg  4126  uniuni  4332  rabxp  4536  elvvv  4562  rexiunxp  4641  resopab2  4824  ssrnres  4939  elxp4  4984  elxp5  4985  cnvresima  4986  mptpreima  4990  coass  5015  dff1o2  5328  eqfnfv3  5474  rexsupp  5498  isoini  5673  f1oiso  5681  oprabid  5757  dfoprab2  5772  mpoeq123  5784  mpomptx  5816  resoprab2  5822  ovi3  5861  oprabex3  5981  spc2ed  6084  f1od2  6086  brtpos2  6102  mapsnen  6659  xpsnen  6668  xpcomco  6673  xpassen  6677  ltexpi  7090  enq0enq  7184  enq0tr  7187  prnmaxl  7241  prnminu  7242  genpdflem  7260  ltexprlemm  7353  axaddf  7600  axmulf  7601  rexuz  9274  rexuz2  9275  rexrp  9362  elixx3g  9574  elfz2  9687  fzdifsuc  9751  fzind2  9906  divalgb  11467  gcdass  11546  lcmass  11609  isprm2  11641  ntreq0  12141  tx1cn  12277  tx2cn  12278  blres  12420  metrest  12492  elcncf1di  12549
  Copyright terms: Public domain W3C validator