Theorem 3jaoi 1427

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 1339	. 2 ⊢ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓))
5		3jao 1425	. 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 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089

This theorem is referenced by:  3jaoian  1429  tpres  7201  ordzsl  7833  onzsl  7834  tfrlem16  8392  oawordeulem  8553  fsetexb  8857  elfiun  9424  infsupprpr  9498  domtriomlem  10436  axdc3lem2  10445  rankcf  10771  znegcl  12596  xrltnr  13098  xnegcl  13191  xnegneg  13192  xltnegi  13194  xnegid  13216  xaddrid  13219  xmulrid  13257  xrsupsslem  13285  xrinfmsslem  13286  reltxrnmnf  13320  elfznelfzo  13736  addmodlteq  13910  hashle2pr  14437  hashge2el2difr  14441  hashtpg  14445  hash1to3  14451  swrdnd0  14606  prm23lt5  16746  prm23ge5  16747  cshwshashlem1  17028  01eq0ringOLD  20305  ioombl1  25078  2irrexpq  26237  ppiublem1  26702  zabsle1  26796  gausslemma2dlem0f  26861  gausslemma2dlem0i  26864  gausslemma2dlem4  26869  2lgsoddprm  26916  ostth  27139  sltval2  27156  sltintdifex  27161  sltres  27162  sltsolem1  27175  nosepnelem  27179  nb3grprlem1  28634  pthdivtx  28983  frgr3vlem1  29523  frgr3vlem2  29524  frgrwopreg  29573  frgrregorufr  29575  frgrregord13  29646  kur14lem7  34198  3jaodd  34679  dfrdg2  34762  dfrdg4  34918  iooelexlt  36238  relowlssretop  36239  wl-exeq  36398  iccpartiltu  46080  iccpartigtl  46081  icceuelpart  46094  prproropf1olem4  46164  fmtno4prmfac193  46231  fmtnofz04prm  46235  mogoldbblem  46378  exple2lt6  47030