Theorem 3jaoi 1340

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 1202	. 2 |- ( ( ph -> ps ) /\ ( ch -> ps ) /\ ( th -> ps ) )
5		3jao 1338	. 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 1004   /\ w3a 1005

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 717

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007

This theorem is referenced by:  3jaoian  1342  3ianorr  1346  acexmidlem1  6048  nndceq  6734  nndcel  6735  znegcl  9610  xrltnr  10115  nltpnft  10150  ngtmnft  10153  xrrebnd  10155  xnegcl  10168  xnegneg  10169  xltnegi  10171  xrpnfdc  10178  xrmnfdc  10179  xnegid  10195  xaddid1  10198  xposdif  10218  prm23lt5  12965  zabsle1  15889  gausslemma2dlem0f  15944  gausslemma2dlem0i  15947  2lgsoddprm  16003