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  7149  ordzsl  7789  onzsl  7790  tfrlem16  8326  oawordeulem  8483  fsetexb  8805  elfiun  9337  infsupprpr  9413  domtriomlem  10356  axdc3lem2  10365  rankcf  10692  znegcl  12530  xrltnr  13037  xnegcl  13132  xnegneg  13133  xltnegi  13135  xnegid  13157  xaddrid  13160  xmulrid  13198  xrsupsslem  13226  xrinfmsslem  13227  reltxrnmnf  13262  elfznelfzo  13693  addmodlteq  13873  hashle2pr  14404  hashge2el2difr  14408  hashtpg  14412  hash1to3  14419  hash3tpde  14420  swrdnd0  14585  prm23lt5  16746  prm23ge5  16747  cshwshashlem1  17027  01eq0ringOLD  20468  ioombl1  25523  2irrexpq  26700  ppiublem1  27173  zabsle1  27267  gausslemma2dlem0f  27332  gausslemma2dlem0i  27335  gausslemma2dlem4  27340  2lgsoddprm  27387  ostth  27610  ltsval2  27628  ltsintdifex  27633  ltsres  27634  ltssolem1  27647  nosepnelem  27651  nb3grprlem1  29457  pthdivtx  29804  frgr3vlem1  30352  frgr3vlem2  30353  frgrwopreg  30402  frgrregorufr  30404  frgrregord13  30475  kur14lem7  35408  3jaodd  35911  dfrdg2  35989  dfrdg4  36147  iooelexlt  37569  relowlssretop  37570  wl-exeq  37741  iccpartiltu  47735  iccpartigtl  47736  icceuelpart  47749  prproropf1olem4  47819  fmtno4prmfac193  47886  fmtnofz04prm  47890  mogoldbblem  48033  grtriproplem  48252  grtrif1o  48255  gpgprismgr4cycllem7  48414  pgnbgreunbgrlem1  48426  pgnbgreunbgrlem2lem1  48427  pgnbgreunbgrlem2lem2  48428  pgnbgreunbgrlem2lem3  48429  pgnbgreunbgrlem2  48430  pgnbgreunbgrlem4  48432  pgnbgreunbgrlem5  48436  exple2lt6  48677