Theorem anandi 512

Description: Distribution of conjunction over conjunction.

Assertion

Ref	Expression
anandi	|- ((ph /\ (ps /\ ch)) <-> ((ph /\ ps) /\ (ph /\ ch)))

Proof of Theorem anandi

Step	Hyp	Ref	Expression
1		anidm 434	. . 3 |- ((ph /\ ph) <-> ph)
2	1	anbi1i 483	. 2 |- (((ph /\ ph) /\ (ps /\ ch)) <-> (ph /\ (ps /\ ch)))
3		an4 508	. 2 |- (((ph /\ ph) /\ (ps /\ ch)) <-> ((ph /\ ps) /\ (ph /\ ch)))
4	2, 3	bitr3 175	1 |- ((ph /\ (ps /\ ch)) <-> ((ph /\ ps) /\ (ph /\ ch)))

Syntax hints:   <-> wb 146   /\ wa 223

This theorem is referenced by:  rnlem 775  mopick2 1439  r19.29 1759  inrab 2274  uniin 2524  ndmoprdistr 4055  oaord 4187  isfinite1 4539  isfinite1OLD 4540  distrlem1pr 5139  cau5i 6917  cau5 6919  climunii 7098  lmuni 7948

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain