Description: Theorem *5.71 of WhiteheadRussell p. 125. (Contributed by Roy F. Longton, 23-Jun-2005)
Ref | Expression | ||
---|---|---|---|
Assertion | pm5.71 | |- ( ( ps -> -. ch ) -> ( ( ( ph \/ ps ) /\ ch ) <-> ( ph /\ ch ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orel2 | |- ( -. ps -> ( ( ph \/ ps ) -> ph ) ) |
|
2 | orc | |- ( ph -> ( ph \/ ps ) ) |
|
3 | 1 2 | impbid1 | |- ( -. ps -> ( ( ph \/ ps ) <-> ph ) ) |
4 | 3 | anbi1d | |- ( -. ps -> ( ( ( ph \/ ps ) /\ ch ) <-> ( ph /\ ch ) ) ) |
5 | pm2.21 | |- ( -. ch -> ( ch -> ( ( ph \/ ps ) <-> ph ) ) ) |
|
6 | 5 | pm5.32rd | |- ( -. ch -> ( ( ( ph \/ ps ) /\ ch ) <-> ( ph /\ ch ) ) ) |
7 | 4 6 | ja | |- ( ( ps -> -. ch ) -> ( ( ( ph \/ ps ) /\ ch ) <-> ( ph /\ ch ) ) ) |