Theorem 3jaod

Description: Disjunction of three antecedents (deduction). (Contributed by NM, 14-Oct-2005)

	Ref	Expression
Hypotheses	3jaod.1	|- ( ph -> ( ps -> ch ) )
	3jaod.2	|- ( ph -> ( th -> ch ) )
	3jaod.3	|- ( ph -> ( ta -> ch ) )
Assertion	3jaod	|- ( ph -> ( ( ps \/ th \/ ta ) -> ch ) )

Proof

Step	Hyp	Ref	Expression
1		3jaod.1	|- ( ph -> ( ps -> ch ) )
2		3jaod.2	|- ( ph -> ( th -> ch ) )
3		3jaod.3	|- ( ph -> ( ta -> ch ) )
4		3jao	|- ( ( ( ps -> ch ) /\ ( th -> ch ) /\ ( ta -> ch ) ) -> ( ( ps \/ th \/ ta ) -> ch ) )
5	1 2 3 4	syl3anc	|- ( ph -> ( ( ps \/ th \/ ta ) -> ch ) )