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 )

Syntax hints:   -> wi 4   \/ w3o 1008   /\ w3a 1009

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 721

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

This theorem is referenced by:  3jaoian  1346  3ianorr  1350  acexmidlem1  6071  nndceq  6762  nndcel  6763  znegcl  9654  xrltnr  10160  nltpnft  10195  ngtmnft  10198  xrrebnd  10200  xnegcl  10213  xnegneg  10214  xltnegi  10216  xrpnfdc  10223  xrmnfdc  10224  xnegid  10240  xaddid1  10243  xposdif  10263  prm23lt5  13020  zabsle1  16032  gausslemma2dlem0f  16087  gausslemma2dlem0i  16090  2lgsoddprm  16146