MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3jaoi Structured version   Visualization version   GIF version

Theorem 3jaoi 1408
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
StepHypRef Expression
1 3jaoi.1 . . 3 (𝜑𝜓)
2 3jaoi.2 . . 3 (𝜒𝜓)
3 3jaoi.3 . . 3 (𝜃𝜓)
41, 2, 33pm3.2i 1320 . 2 ((𝜑𝜓) ∧ (𝜒𝜓) ∧ (𝜃𝜓))
5 3jao 1406 . 2 (((𝜑𝜓) ∧ (𝜒𝜓) ∧ (𝜃𝜓)) → ((𝜑𝜒𝜃) → 𝜓))
64, 5ax-mp 5 1 ((𝜑𝜒𝜃) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1068  w3a 1069
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 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071
This theorem is referenced by:  3jaoian  1410  tpres  6789  ordzsl  7375  onzsl  7376  tfrlem16  7832  oawordeulem  7980  elfiun  8688  infsupprpr  8762  domtriomlem  9661  axdc3lem2  9670  rankcf  9996  znegcl  11829  xrltnr  12330  xnegcl  12422  xnegneg  12423  xltnegi  12425  xnegid  12447  xaddid1  12450  xmulid1  12487  xrsupsslem  12515  xrinfmsslem  12516  reltxrnmnf  12550  elfznelfzo  12956  addmodlteq  13128  hashle2pr  13645  hashge2el2difr  13649  hashtpg  13653  hash1to3  13659  swrdnd0  13824  prm23lt5  16006  prm23ge5  16007  cshwshashlem1  16284  01eq0ring  19779  ioombl1  23882  2irrexpq  25030  ppiublem1  25496  zabsle1  25590  gausslemma2dlem0f  25655  gausslemma2dlem0i  25658  gausslemma2dlem4  25663  2lgsoddprm  25710  ostth  25933  nb3grprlem1  26881  pthdivtx  27234  frgr3vlem1  27823  frgr3vlem2  27824  frgrwopreg  27873  frgrregorufr  27875  frgrregord13  27969  kur14lem7  32077  3jaodd  32497  dfrdg2  32594  sltval2  32717  sltintdifex  32722  sltres  32723  sltsolem1  32734  nosepnelem  32738  dfrdg4  32966  iooelexlt  34118  relowlssretop  34119  wl-exeq  34249  iccpartiltu  42984  iccpartigtl  42985  icceuelpart  42998  prproropf1olem4  43066  fmtno4prmfac193  43133  fmtnofz04prm  43137  mogoldbblem  43283  exple2lt6  43808
  Copyright terms: Public domain W3C validator