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  6081  nndceq  6772  nndcel  6773  znegcl  9679  xrltnr  10191  nltpnft  10226  ngtmnft  10229  xrrebnd  10231  xnegcl  10244  xnegneg  10245  xltnegi  10247  xrpnfdc  10254  xrmnfdc  10255  xnegid  10271  xaddid1  10274  xposdif  10294  prm23lt5  13062  ppiublem1  16192  zabsle1  16216  gausslemma2dlem0f  16271  gausslemma2dlem0i  16274  2lgsoddprm  16330