Theorem 3jaoi 1425

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

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

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 396  df-or 844  df-3or 1086  df-3an 1087

This theorem is referenced by:  3jaoian  1427  tpres  7058  ordzsl  7667  onzsl  7668  tfrlem16  8195  oawordeulem  8347  fsetexb  8610  elfiun  9119  infsupprpr  9193  domtriomlem  10129  axdc3lem2  10138  rankcf  10464  znegcl  12285  xrltnr  12784  xnegcl  12876  xnegneg  12877  xltnegi  12879  xnegid  12901  xaddid1  12904  xmulid1  12942  xrsupsslem  12970  xrinfmsslem  12971  reltxrnmnf  13005  elfznelfzo  13420  addmodlteq  13594  hashle2pr  14119  hashge2el2difr  14123  hashtpg  14127  hash1to3  14133  swrdnd0  14298  prm23lt5  16443  prm23ge5  16444  cshwshashlem1  16725  01eq0ring  20456  ioombl1  24631  2irrexpq  25790  ppiublem1  26255  zabsle1  26349  gausslemma2dlem0f  26414  gausslemma2dlem0i  26417  gausslemma2dlem4  26422  2lgsoddprm  26469  ostth  26692  nb3grprlem1  27650  pthdivtx  27998  frgr3vlem1  28538  frgr3vlem2  28539  frgrwopreg  28588  frgrregorufr  28590  frgrregord13  28661  kur14lem7  33074  3jaodd  33559  dfrdg2  33677  sltval2  33786  sltintdifex  33791  sltres  33792  sltsolem1  33805  nosepnelem  33809  dfrdg4  34180  iooelexlt  35460  relowlssretop  35461  wl-exeq  35620  iccpartiltu  44762  iccpartigtl  44763  icceuelpart  44776  prproropf1olem4  44846  fmtno4prmfac193  44913  fmtnofz04prm  44917  mogoldbblem  45060  exple2lt6  45588