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

Theorem 3jaoi 1540
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 1424 . 2 ((𝜑𝜓) ∧ (𝜒𝜓) ∧ (𝜃𝜓))
5 3jao 1537 . 2 (((𝜑𝜓) ∧ (𝜒𝜓) ∧ (𝜃𝜓)) → ((𝜑𝜒𝜃) → 𝜓))
64, 5ax-mp 5 1 ((𝜑𝜒𝜃) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1071  w3a 1072
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 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074
This theorem is referenced by:  3jaoian  1542  tpres  6630  ordzsl  7210  onzsl  7211  tfrlem16  7658  oawordeulem  7803  elfiun  8501  domtriomlem  9456  axdc3lem2  9465  rankcf  9791  znegcl  11604  xrltnr  12146  xnegcl  12237  xnegneg  12238  xltnegi  12240  xnegid  12262  xaddid1  12265  xmulid1  12302  xrsupsslem  12330  xrinfmsslem  12331  reltxrnmnf  12365  elfznelfzo  12767  addmodlteq  12939  hashle2pr  13451  hashge2el2difr  13455  hashtpg  13459  hash1to3  13465  prm23lt5  15721  prm23ge5  15722  cshwshashlem1  16004  01eq0ring  19474  ioombl1  23530  ppiublem1  25126  zabsle1  25220  gausslemma2dlem0f  25285  gausslemma2dlem0i  25288  gausslemma2dlem4  25293  2lgsoddprm  25340  ostth  25527  nb3grprlem1  26480  pthdivtx  26835  frgr3vlem1  27427  frgr3vlem2  27428  frgrwopreg  27477  frgrregorufr  27479  frgrregord13  27564  kur14lem7  31501  3jaodd  31902  dfrdg2  32006  sltval2  32115  sltintdifex  32120  sltres  32121  sltsolem1  32132  nosepnelem  32136  dfrdg4  32364  iooelexlt  33521  relowlssretop  33522  wl-exeq  33634  iccpartiltu  41868  iccpartigtl  41869  icceuelpart  41882  fmtno4prmfac193  41995  fmtnofz04prm  41999  mogoldbblem  42139  exple2lt6  42655
  Copyright terms: Public domain W3C validator