Theorem 3jaoi 1337

Description: Disjunction of 3 antecedents (inference). (Contributed by NM, 12-Sep-1995.)

Hypotheses

Ref	Expression
3jaoi.1	|- ( ph -> ps )
3jaoi.2	|- ( ch -> ps )
3jaoi.3	|- ( th -> ps )

Assertion

Ref	Expression
3jaoi	|- ( ( ph \/ ch \/ th ) -> ps )

Proof of Theorem 3jaoi

Step	Hyp	Ref	Expression
1		3jaoi.1	. . 3 |- ( ph -> ps )
2		3jaoi.2	. . 3 |- ( ch -> ps )
3		3jaoi.3	. . 3 |- ( th -> ps )
4	1, 2, 3	3pm3.2i 1199	. 2 |- ( ( ph -> ps ) /\ ( ch -> ps ) /\ ( th -> ps ) )
5		3jao 1335	. 2 |- ( ( ( ph -> ps ) /\ ( ch -> ps ) /\ ( th -> ps ) ) -> ( ( ph \/ ch \/ th ) -> ps ) )
6	4, 5	ax-mp 5	1 |- ( ( ph \/ ch \/ th ) -> ps )

Syntax hints:   -> wi 4   \/ w3o 1001   /\ w3a 1002

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004

This theorem is referenced by:  3jaoian  1339  3ianorr  1343  acexmidlem1  5997  nndceq  6645  nndcel  6646  znegcl  9477  xrltnr  9975  nltpnft  10010  ngtmnft  10013  xrrebnd  10015  xnegcl  10028  xnegneg  10029  xltnegi  10031  xrpnfdc  10038  xrmnfdc  10039  xnegid  10055  xaddid1  10058  xposdif  10078  prm23lt5  12786  zabsle1  15678  gausslemma2dlem0f  15733  gausslemma2dlem0i  15736  2lgsoddprm  15792