Theorem 3jaoi 1408

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

Syntax hints:   → wi 4   ∨ w3o 1068   ∧ w3a 1069

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 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071

This theorem is referenced by:  3jaoian  1410  tpres  6789  ordzsl  7375  onzsl  7376  tfrlem16  7832  oawordeulem  7980  elfiun  8688  infsupprpr  8762  domtriomlem  9661  axdc3lem2  9670  rankcf  9996  znegcl  11829  xrltnr  12330  xnegcl  12422  xnegneg  12423  xltnegi  12425  xnegid  12447  xaddid1  12450  xmulid1  12487  xrsupsslem  12515  xrinfmsslem  12516  reltxrnmnf  12550  elfznelfzo  12956  addmodlteq  13128  hashle2pr  13645  hashge2el2difr  13649  hashtpg  13653  hash1to3  13659  swrdnd0  13824  prm23lt5  16006  prm23ge5  16007  cshwshashlem1  16284  01eq0ring  19779  ioombl1  23882  2irrexpq  25030  ppiublem1  25496  zabsle1  25590  gausslemma2dlem0f  25655  gausslemma2dlem0i  25658  gausslemma2dlem4  25663  2lgsoddprm  25710  ostth  25933  nb3grprlem1  26881  pthdivtx  27234  frgr3vlem1  27823  frgr3vlem2  27824  frgrwopreg  27873  frgrregorufr  27875  frgrregord13  27969  kur14lem7  32077  3jaodd  32497  dfrdg2  32594  sltval2  32717  sltintdifex  32722  sltres  32723  sltsolem1  32734  nosepnelem  32738  dfrdg4  32966  iooelexlt  34118  relowlssretop  34119  wl-exeq  34249  iccpartiltu  42984  iccpartigtl  42985  icceuelpart  42998  prproropf1olem4  43066  fmtno4prmfac193  43133  fmtnofz04prm  43137  mogoldbblem  43283  exple2lt6  43808