Theorem 3jaoi 1428

Description: Disjunction of three antecedents (inference). (Contributed by NM, 12-Sep-1995.)

Hypotheses

Ref	Expression
3jaoi.1	⊢ (𝜑 → 𝜓)
3jaoi.2	⊢ (𝜒 → 𝜓)
3jaoi.3	⊢ (𝜃 → 𝜓)

Assertion

Ref	Expression
3jaoi	⊢ ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓)

Proof of Theorem 3jaoi

Step	Hyp	Ref	Expression
1		3jaoi.1	. . 3 ⊢ (𝜑 → 𝜓)
2		3jaoi.2	. . 3 ⊢ (𝜒 → 𝜓)
3		3jaoi.3	. . 3 ⊢ (𝜃 → 𝜓)
4	1, 2, 3	3pm3.2i 1340	. 2 ⊢ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓))
5		3jao 1426	. 2 ⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓)) → ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓))
6	4, 5	ax-mp 5	1 ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∨ w3o 1087   ∧ w3a 1088

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 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090

This theorem is referenced by:  3jaoian  1430  tpres  7202  ordzsl  7834  onzsl  7835  tfrlem16  8393  oawordeulem  8554  fsetexb  8858  elfiun  9425  infsupprpr  9499  domtriomlem  10437  axdc3lem2  10446  rankcf  10772  znegcl  12597  xrltnr  13099  xnegcl  13192  xnegneg  13193  xltnegi  13195  xnegid  13217  xaddrid  13220  xmulrid  13258  xrsupsslem  13286  xrinfmsslem  13287  reltxrnmnf  13321  elfznelfzo  13737  addmodlteq  13911  hashle2pr  14438  hashge2el2difr  14442  hashtpg  14446  hash1to3  14452  swrdnd0  14607  prm23lt5  16747  prm23ge5  16748  cshwshashlem1  17029  01eq0ringOLD  20306  ioombl1  25079  2irrexpq  26239  ppiublem1  26705  zabsle1  26799  gausslemma2dlem0f  26864  gausslemma2dlem0i  26867  gausslemma2dlem4  26872  2lgsoddprm  26919  ostth  27142  sltval2  27159  sltintdifex  27164  sltres  27165  sltsolem1  27178  nosepnelem  27182  nb3grprlem1  28637  pthdivtx  28986  frgr3vlem1  29526  frgr3vlem2  29527  frgrwopreg  29576  frgrregorufr  29578  frgrregord13  29649  kur14lem7  34203  3jaodd  34684  dfrdg2  34767  dfrdg4  34923  iooelexlt  36243  relowlssretop  36244  wl-exeq  36403  iccpartiltu  46090  iccpartigtl  46091  icceuelpart  46104  prproropf1olem4  46174  fmtno4prmfac193  46241  fmtnofz04prm  46245  mogoldbblem  46388  exple2lt6  47040