Theorem 3jaoi 1426

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 1338	. 2 ⊢ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓))
5		3jao 1424	. 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 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088

This theorem is referenced by:  3jaoian  1428  tpres  7085  ordzsl  7701  onzsl  7702  tfrlem16  8233  oawordeulem  8394  fsetexb  8661  elfiun  9198  infsupprpr  9272  domtriomlem  10207  axdc3lem2  10216  rankcf  10542  znegcl  12364  xrltnr  12864  xnegcl  12956  xnegneg  12957  xltnegi  12959  xnegid  12981  xaddid1  12984  xmulid1  13022  xrsupsslem  13050  xrinfmsslem  13051  reltxrnmnf  13085  elfznelfzo  13501  addmodlteq  13675  hashle2pr  14200  hashge2el2difr  14204  hashtpg  14208  hash1to3  14214  swrdnd0  14379  prm23lt5  16524  prm23ge5  16525  cshwshashlem1  16806  01eq0ring  20552  ioombl1  24735  2irrexpq  25894  ppiublem1  26359  zabsle1  26453  gausslemma2dlem0f  26518  gausslemma2dlem0i  26521  gausslemma2dlem4  26526  2lgsoddprm  26573  ostth  26796  nb3grprlem1  27756  pthdivtx  28106  frgr3vlem1  28646  frgr3vlem2  28647  frgrwopreg  28696  frgrregorufr  28698  frgrregord13  28769  kur14lem7  33183  3jaodd  33666  dfrdg2  33780  sltval2  33868  sltintdifex  33873  sltres  33874  sltsolem1  33887  nosepnelem  33891  dfrdg4  34262  iooelexlt  35542  relowlssretop  35543  wl-exeq  35702  iccpartiltu  44885  iccpartigtl  44886  icceuelpart  44899  prproropf1olem4  44969  fmtno4prmfac193  45036  fmtnofz04prm  45040  mogoldbblem  45183  exple2lt6  45711