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