Theorem anandi 836

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 649	. . 3 |- ( ( ph /\ ph ) <-> ph )
2	1	anbi1i 700	. 2 |- ( ( ( ph /\ ph ) /\ ( ps /\ ch ) ) <-> ( ph /\ ( ps /\ ch ) ) )
3		an4 832	. 2 |- ( ( ( ph /\ ph ) /\ ( ps /\ ch ) ) <-> ( ( ph /\ ps ) /\ ( ph /\ ch ) ) )
4	2, 3	bitr3i 255	1 |- ( ( ph /\ ( ps /\ ch ) ) <-> ( ( ph /\ ps ) /\ ( ph /\ ch ) ) )

Syntax hints:   <-> wb 188   /\ wa 371

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 189  df-an 373

This theorem is referenced by:  anandi3  998  an3andi  1381  2eu4  2384  inrab  3714  uniin  4217  xpco  5375  fin  5761  fndmin  5987  oaord  7245  nnaord  7317  ixpin  7544  isffth2  15814  fucinv  15871  setcinv  15978  unocv  19236  bldisj  21406  blin  21429  mbfmax  22598  mbfimaopnlem  22604  mbfaddlem  22609  i1faddlem  22644  i1fmullem  22645  lgsquadlem3  24277  2wlkeq  25428  ofpreima  28261  ordtconlem1  28723  dfpo2  30388  fneval  31001  mbfposadd  31981  prtlem70  32419  fz1eqin  35605  fgraphopab  36081  rngcinv  39970  rngcinvALTV  39982  ringcinv  40021  ringcinvALTV  40045