Theorem anandi 826

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 822	. 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  987  an3andi  1341  2eu4  2390  inrab  3775  uniin  4271  xpco  5553  fin  5771  fndmin  5995  oaord  7208  nnaord  7280  ixpin  7506  isffth2  15160  fucinv  15217  setcinv  15292  unocv  18580  bldisj  20769  blin  20792  mbfmax  21924  mbfimaopnlem  21930  mbfaddlem  21935  i1faddlem  21968  i1fmullem  21969  lgsquadlem3  23497  2wlkeq  24530  ofpreima  27330  ordtconlem1  27731  dfpo2  29111  mbfposadd  29989  fneval  30097  prtlem70  30520  fz1eqin  30630  fgraphopab  31099  ringcinv  32372