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 ) ) )

This proof depends on syntax axioms:   /\ wa 104   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  anandi3  1022  moanim  2161  difundi  3483  inrab  3505  uniin  3955  xpcom  5337  fin  5581  fndmin  5819  nnaord  6787  ixpin  7011  ltexprlemdisj  7979  gsumvalfi  14241  bldisj  15644  blininf  15667  lgsquadlem3  16420  wlkeq  16817