Theorem pm5.53

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

	Ref	Expression
Assertion	pm5.53	|- ( ( ( ( ph \/ ps ) \/ ch ) -> th ) <-> ( ( ( ph -> th ) /\ ( ps -> th ) ) /\ ( ch -> th ) ) )

Proof

Step	Hyp	Ref	Expression
1		jaob	|- ( ( ( ( ph \/ ps ) \/ ch ) -> th ) <-> ( ( ( ph \/ ps ) -> th ) /\ ( ch -> th ) ) )
2		jaob	|- ( ( ( ph \/ ps ) -> th ) <-> ( ( ph -> th ) /\ ( ps -> th ) ) )
3	2	anbi1i	|- ( ( ( ( ph \/ ps ) -> th ) /\ ( ch -> th ) ) <-> ( ( ( ph -> th ) /\ ( ps -> th ) ) /\ ( ch -> th ) ) )
4	1 3	bitri	|- ( ( ( ( ph \/ ps ) \/ ch ) -> th ) <-> ( ( ( ph -> th ) /\ ( ps -> th ) ) /\ ( ch -> th ) ) )