Description: Distribution of conjunction over conjunction. (Contributed by NM, 14-Aug-1995)
Ref | Expression | ||
---|---|---|---|
Assertion | anandi | |- ( ( ph /\ ( ps /\ ch ) ) <-> ( ( ph /\ ps ) /\ ( ph /\ ch ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anidm | |- ( ( ph /\ ph ) <-> ph ) |
|
2 | 1 | anbi1i | |- ( ( ( ph /\ ph ) /\ ( ps /\ ch ) ) <-> ( ph /\ ( ps /\ ch ) ) ) |
3 | an4 | |- ( ( ( ph /\ ph ) /\ ( ps /\ ch ) ) <-> ( ( ph /\ ps ) /\ ( ph /\ ch ) ) ) |
|
4 | 2 3 | bitr3i | |- ( ( ph /\ ( ps /\ ch ) ) <-> ( ( ph /\ ps ) /\ ( ph /\ ch ) ) ) |