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  5963  nndceq  6608  nndcel  6609  znegcl  9438  xrltnr  9936  nltpnft  9971  ngtmnft  9974  xrrebnd  9976  xnegcl  9989  xnegneg  9990  xltnegi  9992  xrpnfdc  9999  xrmnfdc  10000  xnegid  10016  xaddid1  10019  xposdif  10039  prm23lt5  12701  zabsle1  15591  gausslemma2dlem0f  15646  gausslemma2dlem0i  15649  2lgsoddprm  15705