Theorem anandi 598

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 400	. . 3 |- ( ( ph /\ ph ) <-> ph )
2	1	anbi1i 462	. 2 |- ( ( ( ph /\ ph ) /\ ( ps /\ ch ) ) <-> ( ph /\ ( ps /\ ch ) ) )
3		an4 592	. 2 |- ( ( ( ph /\ ph ) /\ ( ps /\ ch ) ) <-> ( ( ph /\ ps ) /\ ( ph /\ ch ) ) )
4	2, 3	bitr3i 186	1 |- ( ( ph /\ ( ps /\ ch ) ) <-> ( ( ph /\ ps ) /\ ( ph /\ ch ) ) )

Syntax hints:   /\ wa 104   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  anandi3  1022  moanim  2161  difundi  3483  inrab  3505  uniin  3953  xpcom  5332  fin  5576  fndmin  5810  nnaord  6775  ixpin  6998  ltexprlemdisj  7966  gsumvalfi  14132  bldisj  15428  blininf  15451  lgsquadlem3  16115  wlkeq  16512