Theorem anandi 871

Description: Distribution of conjunction over conjunction. (Contributed by NM, 14-Aug-1995.)

Assertion

Ref	Expression
anandi	|- ( ( ph /\ ( ps /\ ch ) ) <-> ( ( ph /\ ps ) /\ ( ph /\ ch ) ) )

Proof of Theorem anandi

Step	Hyp	Ref	Expression
1		anidm 676	. . 3 |- ( ( ph /\ ph ) <-> ph )
2	1	anbi1i 731	. 2 |- ( ( ( ph /\ ph ) /\ ( ps /\ ch ) ) <-> ( ph /\ ( ps /\ ch ) ) )
3		an4 865	. 2 |- ( ( ( ph /\ ph ) /\ ( ps /\ ch ) ) <-> ( ( ph /\ ps ) /\ ( ph /\ ch ) ) )
4	2, 3	bitr3i 266	1 |- ( ( ph /\ ( ps /\ ch ) ) <-> ( ( ph /\ ps ) /\ ( ph /\ ch ) ) )

Syntax hints:   <-> wb 196   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  anandi3  1052  an3andi  1445  2eu4  2556  inrab  3899  uniin  4457  xpco  5675  fin  6085  fndmin  6324  oaord  7627  nnaord  7699  ixpin  7933  isffth2  16576  fucinv  16633  setcinv  16740  unocv  20024  bldisj  22203  blin  22226  mbfmax  23416  mbfimaopnlem  23422  mbfaddlem  23427  i1faddlem  23460  i1fmullem  23461  lgsquadlem3  25107  numedglnl  26039  wlkeq  26529  ofpreima  29465  ordtconnlem1  29970  dfpo2  31645  fneval  32347  mbfposadd  33457  anan  33999  exanres  34063  iss2  34112  prtlem70  34141  fz1eqin  37332  fgraphopab  37788  rngcinv  41981  rngcinvALTV  41993  ringcinv  42032  ringcinvALTV  42056