Metamath Proof Explorer


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 )