Theorem 3jaoi 1428

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

Syntax hints:   → wi 4   ∨ w3o 1086   ∧ w3a 1087

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 847  df-3or 1088  df-3an 1089

This theorem is referenced by:  3jaoian  1430  tpres  7238  ordzsl  7882  onzsl  7883  tfrlem16  8449  oawordeulem  8610  fsetexb  8922  elfiun  9499  infsupprpr  9573  domtriomlem  10511  axdc3lem2  10520  rankcf  10846  znegcl  12678  xrltnr  13182  xnegcl  13275  xnegneg  13276  xltnegi  13278  xnegid  13300  xaddrid  13303  xmulrid  13341  xrsupsslem  13369  xrinfmsslem  13370  reltxrnmnf  13404  elfznelfzo  13822  addmodlteq  13997  hashle2pr  14526  hashge2el2difr  14530  hashtpg  14534  hash1to3  14541  hash3tpde  14542  swrdnd0  14705  prm23lt5  16861  prm23ge5  16862  cshwshashlem1  17143  01eq0ringOLD  20557  ioombl1  25616  2irrexpq  26791  ppiublem1  27264  zabsle1  27358  gausslemma2dlem0f  27423  gausslemma2dlem0i  27426  gausslemma2dlem4  27431  2lgsoddprm  27478  ostth  27701  sltval2  27719  sltintdifex  27724  sltres  27725  sltsolem1  27738  nosepnelem  27742  nb3grprlem1  29415  pthdivtx  29765  frgr3vlem1  30305  frgr3vlem2  30306  frgrwopreg  30355  frgrregorufr  30357  frgrregord13  30428  kur14lem7  35180  3jaodd  35677  dfrdg2  35759  dfrdg4  35915  iooelexlt  37328  relowlssretop  37329  wl-exeq  37488  iccpartiltu  47296  iccpartigtl  47297  icceuelpart  47310  prproropf1olem4  47380  fmtno4prmfac193  47447  fmtnofz04prm  47451  mogoldbblem  47594  grtriproplem  47790  grtrif1o  47793  exple2lt6  48089