Theorem 3jaoi 1391

Description: Disjunction of three 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 1239	. 2 |- ( ( ph -> ps ) /\ ( ch -> ps ) /\ ( th -> ps ) )
5		3jao 1389	. 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 1036   /\ w3a 1037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039

This theorem is referenced by:  3jaoian  1393  tpres  6466  ordzsl  7045  onzsl  7046  tfrlem16  7489  oawordeulem  7634  elfiun  8336  domtriomlem  9264  axdc3lem2  9273  rankcf  9599  znegcl  11412  xrltnr  11953  xnegcl  12044  xnegneg  12045  xltnegi  12047  xnegid  12069  xaddid1  12072  xmulid1  12109  xrsupsslem  12137  xrinfmsslem  12138  reltxrnmnf  12172  elfznelfzo  12573  addmodlteq  12745  hashle2pr  13259  hashge2el2difr  13263  hashtpg  13267  hash1to3  13273  prm23lt5  15519  prm23ge5  15520  cshwshashlem1  15802  01eq0ring  19272  ioombl1  23330  ppiublem1  24927  zabsle1  25021  gausslemma2dlem0f  25086  gausslemma2dlem0i  25089  gausslemma2dlem4  25094  2lgsoddprm  25141  ostth  25328  nb3grprlem1  26282  pthdivtx  26625  frgr3vlem1  27137  frgr3vlem2  27138  frgrwopreg  27187  frgrregorufr  27189  frgrregord13  27254  kur14lem7  31194  3jaodd  31595  dfrdg2  31701  sltval2  31809  sltintdifex  31814  sltres  31815  sltsolem1  31826  nosepnelem  31830  dfrdg4  32058  iooelexlt  33210  relowlssretop  33211  wl-exeq  33321  iccpartiltu  41358  iccpartigtl  41359  icceuelpart  41372  fmtno4prmfac193  41485  fmtnofz04prm  41489  mogoldbblem  41629  exple2lt6  42145