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

Theorem 3jaoi 1419
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 1331 . 2 ((𝜑𝜓) ∧ (𝜒𝜓) ∧ (𝜃𝜓))
5 3jao 1417 . 2 (((𝜑𝜓) ∧ (𝜒𝜓) ∧ (𝜃𝜓)) → ((𝜑𝜒𝜃) → 𝜓))
64, 5ax-mp 5 1 ((𝜑𝜒𝜃) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1078  w3a 1079
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 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081
This theorem is referenced by:  3jaoian  1421  tpres  6956  ordzsl  7548  onzsl  7549  tfrlem16  8020  oawordeulem  8170  elfiun  8883  infsupprpr  8957  domtriomlem  9853  axdc3lem2  9862  rankcf  10188  znegcl  12006  xrltnr  12504  xnegcl  12596  xnegneg  12597  xltnegi  12599  xnegid  12621  xaddid1  12624  xmulid1  12662  xrsupsslem  12690  xrinfmsslem  12691  reltxrnmnf  12725  elfznelfzo  13132  addmodlteq  13304  hashle2pr  13825  hashge2el2difr  13829  hashtpg  13833  hash1to3  13839  swrdnd0  14009  prm23lt5  16141  prm23ge5  16142  cshwshashlem1  16419  01eq0ring  19975  ioombl1  24092  2irrexpq  25240  ppiublem1  25706  zabsle1  25800  gausslemma2dlem0f  25865  gausslemma2dlem0i  25868  gausslemma2dlem4  25873  2lgsoddprm  25920  ostth  26143  nb3grprlem1  27090  pthdivtx  27438  frgr3vlem1  27980  frgr3vlem2  27981  frgrwopreg  28030  frgrregorufr  28032  frgrregord13  28103  kur14lem7  32357  3jaodd  32842  dfrdg2  32938  sltval2  33061  sltintdifex  33066  sltres  33067  sltsolem1  33078  nosepnelem  33082  dfrdg4  33310  iooelexlt  34526  relowlssretop  34527  wl-exeq  34656  iccpartiltu  43429  iccpartigtl  43430  icceuelpart  43443  prproropf1olem4  43515  fmtno4prmfac193  43582  fmtnofz04prm  43586  mogoldbblem  43732  exple2lt6  44310
  Copyright terms: Public domain W3C validator