Theorem 3jaoi 1429

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 1426	. 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 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088

This theorem is referenced by:  3jaoian  1431  tpres  7222  ordzsl  7867  onzsl  7868  tfrlem16  8434  oawordeulem  8593  fsetexb  8905  elfiun  9471  infsupprpr  9545  domtriomlem  10483  axdc3lem2  10492  rankcf  10818  znegcl  12654  xrltnr  13162  xnegcl  13256  xnegneg  13257  xltnegi  13259  xnegid  13281  xaddrid  13284  xmulrid  13322  xrsupsslem  13350  xrinfmsslem  13351  reltxrnmnf  13385  elfznelfzo  13812  addmodlteq  13988  hashle2pr  14517  hashge2el2difr  14521  hashtpg  14525  hash1to3  14532  hash3tpde  14533  swrdnd0  14696  prm23lt5  16853  prm23ge5  16854  cshwshashlem1  17134  01eq0ringOLD  20532  ioombl1  25598  2irrexpq  26774  ppiublem1  27247  zabsle1  27341  gausslemma2dlem0f  27406  gausslemma2dlem0i  27409  gausslemma2dlem4  27414  2lgsoddprm  27461  ostth  27684  sltval2  27702  sltintdifex  27707  sltres  27708  sltsolem1  27721  nosepnelem  27725  nb3grprlem1  29398  pthdivtx  29748  frgr3vlem1  30293  frgr3vlem2  30294  frgrwopreg  30343  frgrregorufr  30345  frgrregord13  30416  kur14lem7  35218  3jaodd  35716  dfrdg2  35797  dfrdg4  35953  iooelexlt  37364  relowlssretop  37365  wl-exeq  37536  iccpartiltu  47414  iccpartigtl  47415  icceuelpart  47428  prproropf1olem4  47498  fmtno4prmfac193  47565  fmtnofz04prm  47569  mogoldbblem  47712  grtriproplem  47911  grtrif1o  47914  exple2lt6  48285