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

Theorem 3jaoi 1429
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 1341 . 2 ((𝜑𝜓) ∧ (𝜒𝜓) ∧ (𝜃𝜓))
5 3jao 1427 . 2 (((𝜑𝜓) ∧ (𝜒𝜓) ∧ (𝜃𝜓)) → ((𝜑𝜒𝜃) → 𝜓))
64, 5ax-mp 5 1 ((𝜑𝜒𝜃) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1088  w3a 1089
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 848  df-3or 1090  df-3an 1091
This theorem is referenced by:  3jaoian  1431  tpres  7038  ordzsl  7646  onzsl  7647  tfrlem16  8153  oawordeulem  8306  fsetexb  8569  elfiun  9076  infsupprpr  9150  domtriomlem  10086  axdc3lem2  10095  rankcf  10421  znegcl  12242  xrltnr  12741  xnegcl  12833  xnegneg  12834  xltnegi  12836  xnegid  12858  xaddid1  12861  xmulid1  12899  xrsupsslem  12927  xrinfmsslem  12928  reltxrnmnf  12962  elfznelfzo  13377  addmodlteq  13551  hashle2pr  14076  hashge2el2difr  14080  hashtpg  14084  hash1to3  14090  swrdnd0  14255  prm23lt5  16400  prm23ge5  16401  cshwshashlem1  16682  01eq0ring  20343  ioombl1  24491  2irrexpq  25650  ppiublem1  26115  zabsle1  26209  gausslemma2dlem0f  26274  gausslemma2dlem0i  26277  gausslemma2dlem4  26282  2lgsoddprm  26329  ostth  26552  nb3grprlem1  27500  pthdivtx  27848  frgr3vlem1  28388  frgr3vlem2  28389  frgrwopreg  28438  frgrregorufr  28440  frgrregord13  28511  kur14lem7  32918  3jaodd  33403  dfrdg2  33521  sltval2  33630  sltintdifex  33635  sltres  33636  sltsolem1  33649  nosepnelem  33653  dfrdg4  34024  iooelexlt  35307  relowlssretop  35308  wl-exeq  35467  iccpartiltu  44593  iccpartigtl  44594  icceuelpart  44607  prproropf1olem4  44677  fmtno4prmfac193  44744  fmtnofz04prm  44748  mogoldbblem  44891  exple2lt6  45419
  Copyright terms: Public domain W3C validator