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  6056  nndceq  6747  nndcel  6748  znegcl  9630  xrltnr  10136  nltpnft  10171  ngtmnft  10174  xrrebnd  10176  xnegcl  10189  xnegneg  10190  xltnegi  10192  xrpnfdc  10199  xrmnfdc  10200  xnegid  10216  xaddid1  10219  xposdif  10239  prm23lt5  12992  zabsle1  16003  gausslemma2dlem0f  16058  gausslemma2dlem0i  16061  2lgsoddprm  16117