Theorem 3jaoi 1316

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 1178	. 2 |- ( ( ph -> ps ) /\ ( ch -> ps ) /\ ( th -> ps ) )
5		3jao 1314	. 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 980   /\ w3a 981

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 711

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983

This theorem is referenced by:  3jaoian  1318  3ianorr  1322  acexmidlem1  5942  nndceq  6587  nndcel  6588  znegcl  9405  xrltnr  9903  nltpnft  9938  ngtmnft  9941  xrrebnd  9943  xnegcl  9956  xnegneg  9957  xltnegi  9959  xrpnfdc  9966  xrmnfdc  9967  xnegid  9983  xaddid1  9986  xposdif  10006  prm23lt5  12619  zabsle1  15509  gausslemma2dlem0f  15564  gausslemma2dlem0i  15567  2lgsoddprm  15623