Metamath Proof Explorer


Theorem pm5.71

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

Proof

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