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

Theorem 3jaoi 1424
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 1336 . 2 ((𝜑𝜓) ∧ (𝜒𝜓) ∧ (𝜃𝜓))
5 3jao 1422 . 2 (((𝜑𝜓) ∧ (𝜒𝜓) ∧ (𝜃𝜓)) → ((𝜑𝜒𝜃) → 𝜓))
64, 5ax-mp 5 1 ((𝜑𝜒𝜃) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1083  w3a 1084
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 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086
This theorem is referenced by:  3jaoian  1426  tpres  6955  ordzsl  7555  onzsl  7556  tfrlem16  8026  oawordeulem  8177  elfiun  8892  infsupprpr  8966  domtriomlem  9863  axdc3lem2  9872  rankcf  10198  znegcl  12017  xrltnr  12514  xnegcl  12606  xnegneg  12607  xltnegi  12609  xnegid  12631  xaddid1  12634  xmulid1  12672  xrsupsslem  12700  xrinfmsslem  12701  reltxrnmnf  12735  elfznelfzo  13149  addmodlteq  13321  hashle2pr  13843  hashge2el2difr  13847  hashtpg  13851  hash1to3  13857  swrdnd0  14022  prm23lt5  16152  prm23ge5  16153  cshwshashlem1  16432  01eq0ring  20048  ioombl1  24172  2irrexpq  25327  ppiublem1  25792  zabsle1  25886  gausslemma2dlem0f  25951  gausslemma2dlem0i  25954  gausslemma2dlem4  25959  2lgsoddprm  26006  ostth  26229  nb3grprlem1  27176  pthdivtx  27524  frgr3vlem1  28064  frgr3vlem2  28065  frgrwopreg  28114  frgrregorufr  28116  frgrregord13  28187  kur14lem7  32519  3jaodd  33004  dfrdg2  33100  sltval2  33223  sltintdifex  33228  sltres  33229  sltsolem1  33240  nosepnelem  33244  dfrdg4  33472  iooelexlt  34727  relowlssretop  34728  wl-exeq  34885  iccpartiltu  43866  iccpartigtl  43867  icceuelpart  43880  prproropf1olem4  43950  fmtno4prmfac193  44017  fmtnofz04prm  44021  mogoldbblem  44165  exple2lt6  44693
  Copyright terms: Public domain W3C validator