Theorem 3jaoi 1314

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 1177	. 2 |- ( ( ph -> ps ) /\ ( ch -> ps ) /\ ( th -> ps ) )
5		3jao 1312	. 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 979   /\ w3a 980

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 710

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

This theorem is referenced by:  3jaoian  1316  3ianorr  1320  acexmidlem1  5918  nndceq  6557  nndcel  6558  znegcl  9357  xrltnr  9854  nltpnft  9889  ngtmnft  9892  xrrebnd  9894  xnegcl  9907  xnegneg  9908  xltnegi  9910  xrpnfdc  9917  xrmnfdc  9918  xnegid  9934  xaddid1  9937  xposdif  9957  prm23lt5  12432  zabsle1  15240  gausslemma2dlem0f  15295  gausslemma2dlem0i  15298  2lgsoddprm  15354