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 396  df-or 845  df-3or 1087  df-3an 1088

This theorem is referenced by:  3jaoian  1428  tpres  7204  ordzsl  7838  onzsl  7839  tfrlem16  8399  oawordeulem  8560  fsetexb  8864  elfiun  9431  infsupprpr  9505  domtriomlem  10443  axdc3lem2  10452  rankcf  10778  znegcl  12604  xrltnr  13106  xnegcl  13199  xnegneg  13200  xltnegi  13202  xnegid  13224  xaddrid  13227  xmulrid  13265  xrsupsslem  13293  xrinfmsslem  13294  reltxrnmnf  13328  elfznelfzo  13744  addmodlteq  13918  hashle2pr  14445  hashge2el2difr  14449  hashtpg  14453  hash1to3  14459  swrdnd0  14614  prm23lt5  16754  prm23ge5  16755  cshwshashlem1  17036  01eq0ringOLD  20427  ioombl1  25411  2irrexpq  26579  ppiublem1  27048  zabsle1  27142  gausslemma2dlem0f  27207  gausslemma2dlem0i  27210  gausslemma2dlem4  27215  2lgsoddprm  27262  ostth  27485  sltval2  27502  sltintdifex  27507  sltres  27508  sltsolem1  27521  nosepnelem  27525  nb3grprlem1  29070  pthdivtx  29419  frgr3vlem1  29959  frgr3vlem2  29960  frgrwopreg  30009  frgrregorufr  30011  frgrregord13  30082  kur14lem7  34667  3jaodd  35154  dfrdg2  35237  dfrdg4  35393  iooelexlt  36707  relowlssretop  36708  wl-exeq  36867  iccpartiltu  46549  iccpartigtl  46550  icceuelpart  46563  prproropf1olem4  46633  fmtno4prmfac193  46700  fmtnofz04prm  46704  mogoldbblem  46847  exple2lt6  47203