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  5915  nndceq  6554  nndcel  6555  znegcl  9351  xrltnr  9848  nltpnft  9883  ngtmnft  9886  xrrebnd  9888  xnegcl  9901  xnegneg  9902  xltnegi  9904  xrpnfdc  9911  xrmnfdc  9912  xnegid  9928  xaddid1  9931  xposdif  9951  prm23lt5  12404  zabsle1  15156  gausslemma2dlem0f  15211  gausslemma2dlem0i  15214  2lgsoddprm  15270