Theorem 3jaoi 1424

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

Syntax hints:   → wi 4   ∨ w3o 1083   ∧ w3a 1084

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 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086

This theorem is referenced by:  3jaoian  1426  tpres  6940  ordzsl  7540  onzsl  7541  tfrlem16  8012  oawordeulem  8163  elfiun  8878  infsupprpr  8952  domtriomlem  9853  axdc3lem2  9862  rankcf  10188  znegcl  12005  xrltnr  12502  xnegcl  12594  xnegneg  12595  xltnegi  12597  xnegid  12619  xaddid1  12622  xmulid1  12660  xrsupsslem  12688  xrinfmsslem  12689  reltxrnmnf  12723  elfznelfzo  13137  addmodlteq  13309  hashle2pr  13831  hashge2el2difr  13835  hashtpg  13839  hash1to3  13845  swrdnd0  14010  prm23lt5  16141  prm23ge5  16142  cshwshashlem1  16421  01eq0ring  20038  ioombl1  24166  2irrexpq  25321  ppiublem1  25786  zabsle1  25880  gausslemma2dlem0f  25945  gausslemma2dlem0i  25948  gausslemma2dlem4  25953  2lgsoddprm  26000  ostth  26223  nb3grprlem1  27170  pthdivtx  27518  frgr3vlem1  28058  frgr3vlem2  28059  frgrwopreg  28108  frgrregorufr  28110  frgrregord13  28181  kur14lem7  32572  3jaodd  33057  dfrdg2  33153  sltval2  33276  sltintdifex  33281  sltres  33282  sltsolem1  33293  nosepnelem  33297  dfrdg4  33525  iooelexlt  34779  relowlssretop  34780  wl-exeq  34939  iccpartiltu  43939  iccpartigtl  43940  icceuelpart  43953  prproropf1olem4  44023  fmtno4prmfac193  44090  fmtnofz04prm  44094  mogoldbblem  44238  exple2lt6  44766