Theorem anandi 835

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 648	. . 3 |- ( ( ph /\ ph ) <-> ph )
2	1	anbi1i 699	. 2 |- ( ( ( ph /\ ph ) /\ ( ps /\ ch ) ) <-> ( ph /\ ( ps /\ ch ) ) )
3		an4 831	. 2 |- ( ( ( ph /\ ph ) /\ ( ps /\ ch ) ) <-> ( ( ph /\ ps ) /\ ( ph /\ ch ) ) )
4	2, 3	bitr3i 254	1 |- ( ( ph /\ ( ps /\ ch ) ) <-> ( ( ph /\ ps ) /\ ( ph /\ ch ) ) )

Syntax hints:   <-> wb 187   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  anandi3  996  an3andi  1377  2eu4  2354  inrab  3745  uniin  4236  xpco  5391  fin  5776  fndmin  6000  oaord  7252  nnaord  7324  ixpin  7551  isffth2  15808  fucinv  15865  setcinv  15972  unocv  19229  bldisj  21399  blin  21422  mbfmax  22591  mbfimaopnlem  22597  mbfaddlem  22602  i1faddlem  22637  i1fmullem  22638  lgsquadlem3  24270  2wlkeq  25420  ofpreima  28257  ordtconlem1  28725  dfpo2  30389  fneval  31000  mbfposadd  31901  prtlem70  32340  fz1eqin  35529  fgraphopab  36006  rngcinv  39254  rngcinvALTV  39266  ringcinv  39305  ringcinvALTV  39329