Theorem anandi 824

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 644	. . 3 |- ( ( ph /\ ph ) <-> ph )
2	1	anbi1i 695	. 2 |- ( ( ( ph /\ ph ) /\ ( ps /\ ch ) ) <-> ( ph /\ ( ps /\ ch ) ) )
3		an4 820	. 2 |- ( ( ( ph /\ ph ) /\ ( ps /\ ch ) ) <-> ( ( ph /\ ps ) /\ ( ph /\ ch ) ) )
4	2, 3	bitr3i 251	1 |- ( ( ph /\ ( ps /\ ch ) ) <-> ( ( ph /\ ps ) /\ ( ph /\ ch ) ) )

Syntax hints:   <-> wb 184   /\ wa 369

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 185  df-an 371

This theorem is referenced by:  anandi3  979  an3andi  1331  2eu4  2368  inrab  3622  uniin  4111  xpco  5377  fin  5591  fndmin  5810  oaord  6986  nnaord  7058  ixpin  7288  isffth2  14826  fucinv  14883  setcinv  14958  unocv  18105  bldisj  19973  blin  19996  mbfmax  21127  mbfimaopnlem  21133  mbfaddlem  21138  i1faddlem  21171  i1fmullem  21172  lgsquadlem3  22695  ofpreima  25984  ordtconlem1  26354  dfpo2  27565  mbfposadd  28439  fneval  28559  prtlem70  28996  fz1eqin  29107  fgraphopab  29578  2wlkeq  30288