Theorem jaoi3

Description: Inference separating a disjunct of an antecedent. (Contributed by Alexander van der Vekens, 25-May-2018)

	Ref	Expression
Hypotheses	jaoi3.1	|- ( ph -> ps )
	jaoi3.2	|- ( ( -. ph /\ ch ) -> ps )
Assertion	jaoi3	|- ( ( ph \/ ch ) -> ps )

Proof

Step	Hyp	Ref	Expression
1		jaoi3.1	|- ( ph -> ps )
2		jaoi3.2	|- ( ( -. ph /\ ch ) -> ps )
3	1 2	jaoi	|- ( ( ph \/ ( -. ph /\ ch ) ) -> ps )
4	3	jaoi2	|- ( ( ph \/ ch ) -> ps )