Theorem 3jaoi 1422

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

Syntax hints:   → wi 4   ∨ w3o 1081   ∧ w3a 1082

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 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084

This theorem is referenced by:  3jaoian  1424  tpres  6956  ordzsl  7552  onzsl  7553  tfrlem16  8021  oawordeulem  8172  elfiun  8886  infsupprpr  8960  domtriomlem  9856  axdc3lem2  9865  rankcf  10191  znegcl  12009  xrltnr  12506  xnegcl  12598  xnegneg  12599  xltnegi  12601  xnegid  12623  xaddid1  12626  xmulid1  12664  xrsupsslem  12692  xrinfmsslem  12693  reltxrnmnf  12727  elfznelfzo  13134  addmodlteq  13306  hashle2pr  13827  hashge2el2difr  13831  hashtpg  13835  hash1to3  13841  swrdnd0  14011  prm23lt5  16143  prm23ge5  16144  cshwshashlem1  16421  01eq0ring  20037  ioombl1  24155  2irrexpq  25305  ppiublem1  25770  zabsle1  25864  gausslemma2dlem0f  25929  gausslemma2dlem0i  25932  gausslemma2dlem4  25937  2lgsoddprm  25984  ostth  26207  nb3grprlem1  27154  pthdivtx  27502  frgr3vlem1  28044  frgr3vlem2  28045  frgrwopreg  28094  frgrregorufr  28096  frgrregord13  28167  kur14lem7  32452  3jaodd  32937  dfrdg2  33033  sltval2  33156  sltintdifex  33161  sltres  33162  sltsolem1  33173  nosepnelem  33177  dfrdg4  33405  iooelexlt  34635  relowlssretop  34636  wl-exeq  34766  iccpartiltu  43572  iccpartigtl  43573  icceuelpart  43586  prproropf1olem4  43658  fmtno4prmfac193  43725  fmtnofz04prm  43729  mogoldbblem  43875  exple2lt6  44402