Theorem 3jaoian

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

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

Proof

Step	Hyp	Ref	Expression
1		3jaoian.1	|- ( ( ph /\ ps ) -> ch )
2		3jaoian.2	|- ( ( th /\ ps ) -> ch )
3		3jaoian.3	|- ( ( ta /\ ps ) -> ch )
4	1	ex	|- ( ph -> ( ps -> ch ) )
5	2	ex	|- ( th -> ( ps -> ch ) )
6	3	ex	|- ( ta -> ( ps -> ch ) )
7	4 5 6	3jaoi	|- ( ( ph \/ th \/ ta ) -> ( ps -> ch ) )
8	7	imp	|- ( ( ( ph \/ th \/ ta ) /\ ps ) -> ch )