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

Theorem 3jaoi 1545
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 1431 . 2 ((𝜑𝜓) ∧ (𝜒𝜓) ∧ (𝜃𝜓))
5 3jao 1542 . 2 (((𝜑𝜓) ∧ (𝜒𝜓) ∧ (𝜃𝜓)) → ((𝜑𝜒𝜃) → 𝜓))
64, 5ax-mp 5 1 ((𝜑𝜒𝜃) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1099  w3a 1100
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 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102
This theorem is referenced by:  3jaoian  1547  tpres  6691  ordzsl  7275  onzsl  7276  tfrlem16  7725  oawordeulem  7871  elfiun  8575  domtriomlem  9549  axdc3lem2  9558  rankcf  9884  znegcl  11678  xrltnr  12169  xnegcl  12262  xnegneg  12263  xltnegi  12265  xnegid  12287  xaddid1  12290  xmulid1  12327  xrsupsslem  12355  xrinfmsslem  12356  reltxrnmnf  12390  elfznelfzo  12797  addmodlteq  12969  hashle2pr  13476  hashge2el2difr  13480  hashtpg  13484  hash1to3  13490  prm23lt5  15736  prm23ge5  15737  cshwshashlem1  16014  01eq0ring  19481  ioombl1  23543  ppiublem1  25141  zabsle1  25235  gausslemma2dlem0f  25300  gausslemma2dlem0i  25303  gausslemma2dlem4  25308  2lgsoddprm  25355  ostth  25542  nb3grprlem1  26498  pthdivtx  26853  frgr3vlem1  27448  frgr3vlem2  27449  frgrwopreg  27498  frgrregorufr  27500  frgrregord13  27584  kur14lem7  31517  3jaodd  31917  dfrdg2  32021  sltval2  32130  sltintdifex  32135  sltres  32136  sltsolem1  32147  nosepnelem  32151  dfrdg4  32379  iooelexlt  33526  relowlssretop  33527  wl-exeq  33635  iccpartiltu  41933  iccpartigtl  41934  icceuelpart  41947  fmtno4prmfac193  42060  fmtnofz04prm  42064  mogoldbblem  42204  exple2lt6  42713
  Copyright terms: Public domain W3C validator