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  7198  ordzsl  7845  onzsl  7846  tfrlem16  8412  oawordeulem  8571  fsetexb  8883  elfiun  9447  infsupprpr  9523  domtriomlem  10461  axdc3lem2  10470  rankcf  10796  znegcl  12632  xrltnr  13140  xnegcl  13234  xnegneg  13235  xltnegi  13237  xnegid  13259  xaddrid  13262  xmulrid  13300  xrsupsslem  13328  xrinfmsslem  13329  reltxrnmnf  13364  elfznelfzo  13793  addmodlteq  13969  hashle2pr  14500  hashge2el2difr  14504  hashtpg  14508  hash1to3  14515  hash3tpde  14516  swrdnd0  14680  prm23lt5  16839  prm23ge5  16840  cshwshashlem1  17120  01eq0ringOLD  20496  ioombl1  25520  2irrexpq  26697  ppiublem1  27170  zabsle1  27264  gausslemma2dlem0f  27329  gausslemma2dlem0i  27332  gausslemma2dlem4  27337  2lgsoddprm  27384  ostth  27607  sltval2  27625  sltintdifex  27630  sltres  27631  sltsolem1  27644  nosepnelem  27648  nb3grprlem1  29364  pthdivtx  29714  frgr3vlem1  30259  frgr3vlem2  30260  frgrwopreg  30309  frgrregorufr  30311  frgrregord13  30382  kur14lem7  35239  3jaodd  35737  dfrdg2  35818  dfrdg4  35974  iooelexlt  37385  relowlssretop  37386  wl-exeq  37557  iccpartiltu  47403  iccpartigtl  47404  icceuelpart  47417  prproropf1olem4  47487  fmtno4prmfac193  47554  fmtnofz04prm  47558  mogoldbblem  47701  grtriproplem  47918  grtrif1o  47921  gpgprismgr4cycllem7  48067  exple2lt6  48306