Theorem pm2.82

Description: Theorem *2.82 of WhiteheadRussell p. 108. (Contributed by NM, 3-Jan-2005)

	Ref	Expression
Assertion	pm2.82	|- ( ( ( ph \/ ps ) \/ ch ) -> ( ( ( ph \/ -. ch ) \/ th ) -> ( ( ph \/ ps ) \/ th ) ) )

Proof

Step	Hyp	Ref	Expression
1		pm2.24	|- ( ch -> ( -. ch -> ps ) )
2	1	orim2d	|- ( ch -> ( ( ph \/ -. ch ) -> ( ph \/ ps ) ) )
3	2	jao1i	|- ( ( ( ph \/ ps ) \/ ch ) -> ( ( ph \/ -. ch ) -> ( ph \/ ps ) ) )
4	3	orim1d	|- ( ( ( ph \/ ps ) \/ ch ) -> ( ( ( ph \/ -. ch ) \/ th ) -> ( ( ph \/ ps ) \/ th ) ) )