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  9675  xrltnr  10181  nltpnft  10216  ngtmnft  10219  xrrebnd  10221  xnegcl  10234  xnegneg  10235  xltnegi  10237  xrpnfdc  10244  xrmnfdc  10245  xnegid  10261  xaddid1  10264  xposdif  10284  prm23lt5  13042  zabsle1  16118  gausslemma2dlem0f  16173  gausslemma2dlem0i  16176  2lgsoddprm  16232