Theorem 3jaoi 1430

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

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

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 848  df-3or 1087  df-3an 1088

This theorem is referenced by:  3jaoian  1432  tpres  7157  ordzsl  7801  onzsl  7802  tfrlem16  8338  oawordeulem  8495  fsetexb  8814  elfiun  9357  infsupprpr  9433  domtriomlem  10371  axdc3lem2  10380  rankcf  10706  znegcl  12544  xrltnr  13055  xnegcl  13149  xnegneg  13150  xltnegi  13152  xnegid  13174  xaddrid  13177  xmulrid  13215  xrsupsslem  13243  xrinfmsslem  13244  reltxrnmnf  13279  elfznelfzo  13709  addmodlteq  13887  hashle2pr  14418  hashge2el2difr  14422  hashtpg  14426  hash1to3  14433  hash3tpde  14434  swrdnd0  14598  prm23lt5  16761  prm23ge5  16762  cshwshashlem1  17042  01eq0ringOLD  20451  ioombl1  25496  2irrexpq  26673  ppiublem1  27146  zabsle1  27240  gausslemma2dlem0f  27305  gausslemma2dlem0i  27308  gausslemma2dlem4  27313  2lgsoddprm  27360  ostth  27583  sltval2  27601  sltintdifex  27606  sltres  27607  sltsolem1  27620  nosepnelem  27624  nb3grprlem1  29360  pthdivtx  29707  frgr3vlem1  30252  frgr3vlem2  30253  frgrwopreg  30302  frgrregorufr  30304  frgrregord13  30375  kur14lem7  35192  3jaodd  35695  dfrdg2  35776  dfrdg4  35932  iooelexlt  37343  relowlssretop  37344  wl-exeq  37515  iccpartiltu  47416  iccpartigtl  47417  icceuelpart  47430  prproropf1olem4  47500  fmtno4prmfac193  47567  fmtnofz04prm  47571  mogoldbblem  47714  grtriproplem  47931  grtrif1o  47934  gpgprismgr4cycllem7  48084  pgnbgreunbgrlem1  48096  pgnbgreunbgrlem2lem1  48097  pgnbgreunbgrlem2lem2  48098  pgnbgreunbgrlem2lem3  48099  pgnbgreunbgrlem2  48100  pgnbgreunbgrlem4  48102  pgnbgreunbgrlem5  48106  exple2lt6  48345