Theorem 3jaoi 1437

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

Syntax hints:   → wi 4   ∨ w3o 1092   ∧ w3a 1093

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 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095

This theorem is referenced by:  3jaoian  1439  tpres  7149  ordzsl  7789  onzsl  7790  tfrlem16  8326  oawordeulem  8483  fsetexb  8805  elfiun  9337  infsupprpr  9413  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  20507  ioombl1  25551  2irrexpq  26717  ppiublem1  27187  zabsle1  27281  gausslemma2dlem0f  27346  gausslemma2dlem0i  27349  gausslemma2dlem4  27354  2lgsoddprm  27401  ostth  27624  ltsval2  27642  ltsintdifex  27647  ltsres  27648  ltssolem1  27661  nosepnelem  27665  nb3grprlem1  29471  pthdivtx  29817  frgr3vlem1  30365  frgr3vlem2  30366  frgrwopreg  30415  frgrregorufr  30417  frgrregord13  30488  kur14lem7  35455  3jaodd  35958  dfrdg2  36036  dfrdg4  36194  iooelexlt  37739  relowlssretop  37740  wl-exeq  37920  iccpartiltu  47911  iccpartigtl  47912  icceuelpart  47925  prproropf1olem4  47995  fmtno4prmfac193  48065  fmtnofz04prm  48069  mogoldbblem  48225  grtriproplem  48444  grtrif1o  48447  gpgprismgr4cycllem7  48606  pgnbgreunbgrlem1  48618  pgnbgreunbgrlem2lem1  48619  pgnbgreunbgrlem2lem2  48620  pgnbgreunbgrlem2lem3  48621  pgnbgreunbgrlem2  48622  pgnbgreunbgrlem4  48624  pgnbgreunbgrlem5  48628  exple2lt6  48869