Theorem 3jaoi 1344

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 1206	. 2 |- ( ( ph -> ps ) /\ ( ch -> ps ) /\ ( th -> ps ) )
5		3jao 1342	. 2 |- ( ( ( ph -> ps ) /\ ( ch -> ps ) /\ ( th -> ps ) ) -> ( ( ph \/ ch \/ th ) -> ps ) )
6	4, 5	ax-mp 5	1 |- ( ( ph \/ ch \/ th ) -> ps )

This proof depends on syntax axioms:   -> wi 4   \/ w3o 1008   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011

This theorem is used by:  3jaoian  1346  3ianorr  1350  acexmidlem1  6084  nndceq  6777  nndcel  6778  znegcl  9684  xrltnr  10197  nltpnft  10232  ngtmnft  10235  xrrebnd  10237  xnegcl  10250  xnegneg  10251  xltnegi  10253  xrpnfdc  10260  xrmnfdc  10261  xnegid  10277  xaddid1  10280  xposdif  10300  prm23lt5  13070  ppiublem1  16308  zabsle1  16340  gausslemma2dlem0f  16395  gausslemma2dlem0i  16398  2lgsoddprm  16454