Theorem 3jaoi 1431

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 1341	. 2 ⊢ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓))
5		3jao 1428	. 2 ⊢ (((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓)) → ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓))
6	4, 5	ax-mp 5	1 ⊢ ((𝜑 ∨ 𝜒 ∨ 𝜃) → 𝜓)

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

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 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089

This theorem is referenced by:  3jaoian  1433  tpres  7151  ordzsl  7791  onzsl  7792  tfrlem16  8327  oawordeulem  8484  fsetexb  8806  elfiun  9338  infsupprpr  9414  domtriomlem  10359  axdc3lem2  10368  rankcf  10695  znegcl  12557  xrltnr  13065  xnegcl  13160  xnegneg  13161  xltnegi  13163  xnegid  13185  xaddrid  13188  xmulrid  13226  xrsupsslem  13254  xrinfmsslem  13255  reltxrnmnf  13290  elfznelfzo  13723  addmodlteq  13903  hashle2pr  14434  hashge2el2difr  14438  hashtpg  14442  hash1to3  14449  hash3tpde  14450  swrdnd0  14615  prm23lt5  16780  prm23ge5  16781  cshwshashlem1  17061  01eq0ringOLD  20503  ioombl1  25543  2irrexpq  26712  ppiublem1  27183  zabsle1  27277  gausslemma2dlem0f  27342  gausslemma2dlem0i  27345  gausslemma2dlem4  27350  2lgsoddprm  27397  ostth  27620  ltsval2  27638  ltsintdifex  27643  ltsres  27644  ltssolem1  27657  nosepnelem  27661  nb3grprlem1  29467  pthdivtx  29814  frgr3vlem1  30362  frgr3vlem2  30363  frgrwopreg  30412  frgrregorufr  30414  frgrregord13  30485  kur14lem7  35414  3jaodd  35917  dfrdg2  35995  dfrdg4  36153  iooelexlt  37696  relowlssretop  37697  wl-exeq  37877  iccpartiltu  47898  iccpartigtl  47899  icceuelpart  47912  prproropf1olem4  47982  fmtno4prmfac193  48052  fmtnofz04prm  48056  mogoldbblem  48212  grtriproplem  48431  grtrif1o  48434  gpgprismgr4cycllem7  48593  pgnbgreunbgrlem1  48605  pgnbgreunbgrlem2lem1  48606  pgnbgreunbgrlem2lem2  48607  pgnbgreunbgrlem2lem3  48608  pgnbgreunbgrlem2  48609  pgnbgreunbgrlem4  48611  pgnbgreunbgrlem5  48615  exple2lt6  48856