Theorem 3jaoi 1430

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 1340	. 2 ⊢ ((𝜑 → 𝜓) ∧ (𝜒 → 𝜓) ∧ (𝜃 → 𝜓))
5		3jao 1427	. 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  1432  tpres  7137  ordzsl  7778  onzsl  7779  tfrlem16  8315  oawordeulem  8472  fsetexb  8791  elfiun  9320  infsupprpr  9396  domtriomlem  10336  axdc3lem2  10345  rankcf  10671  znegcl  12510  xrltnr  13021  xnegcl  13115  xnegneg  13116  xltnegi  13118  xnegid  13140  xaddrid  13143  xmulrid  13181  xrsupsslem  13209  xrinfmsslem  13210  reltxrnmnf  13245  elfznelfzo  13675  addmodlteq  13853  hashle2pr  14384  hashge2el2difr  14388  hashtpg  14392  hash1to3  14399  hash3tpde  14400  swrdnd0  14564  prm23lt5  16726  prm23ge5  16727  cshwshashlem1  17007  01eq0ringOLD  20416  ioombl1  25461  2irrexpq  26638  ppiublem1  27111  zabsle1  27205  gausslemma2dlem0f  27270  gausslemma2dlem0i  27273  gausslemma2dlem4  27278  2lgsoddprm  27325  ostth  27548  sltval2  27566  sltintdifex  27571  sltres  27572  sltsolem1  27585  nosepnelem  27589  nb3grprlem1  29325  pthdivtx  29672  frgr3vlem1  30217  frgr3vlem2  30218  frgrwopreg  30267  frgrregorufr  30269  frgrregord13  30340  kur14lem7  35195  3jaodd  35698  dfrdg2  35779  dfrdg4  35935  iooelexlt  37346  relowlssretop  37347  wl-exeq  37518  iccpartiltu  47416  iccpartigtl  47417  icceuelpart  47430  prproropf1olem4  47500  fmtno4prmfac193  47567  fmtnofz04prm  47571  mogoldbblem  47714  grtriproplem  47933  grtrif1o  47936  gpgprismgr4cycllem7  48095  pgnbgreunbgrlem1  48107  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  pgnbgreunbgrlem2lem3  48110  pgnbgreunbgrlem2  48111  pgnbgreunbgrlem4  48113  pgnbgreunbgrlem5  48117  exple2lt6  48358