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

Theorem 3jaoi 1388
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 1237 . 2 ((𝜑𝜓) ∧ (𝜒𝜓) ∧ (𝜃𝜓))
5 3jao 1386 . 2 (((𝜑𝜓) ∧ (𝜒𝜓) ∧ (𝜃𝜓)) → ((𝜑𝜒𝜃) → 𝜓))
64, 5ax-mp 5 1 ((𝜑𝜒𝜃) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1035  w3a 1036
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 385  df-an 386  df-3or 1037  df-3an 1038
This theorem is referenced by:  3jaoian  1390  tpres  6420  ordzsl  6992  onzsl  6993  tfrlem16  7434  oawordeulem  7579  elfiun  8280  domtriomlem  9208  axdc3lem2  9217  rankcf  9543  znegcl  11356  xrltnr  11897  xnegcl  11987  xnegneg  11988  xltnegi  11990  xnegid  12012  xaddid1  12015  xmulid1  12052  xrsupsslem  12080  xrinfmsslem  12081  reltxrnmnf  12114  elfznelfzo  12514  addmodlteq  12685  hashle2pr  13197  hashge2el2difr  13201  hashtpg  13205  hash1to3  13212  prm23lt5  15443  prm23ge5  15444  cshwshashlem1  15726  01eq0ring  19191  ioombl1  23237  ppiublem1  24827  zabsle1  24921  gausslemma2dlem0f  24986  gausslemma2dlem0i  24989  gausslemma2dlem4  24994  2lgsoddprm  25041  ostth  25228  nb3grprlem1  26169  pthdivtx  26494  frgr3vlem1  27001  frgr3vlem2  27002  frgrwopreg  27044  frgrregorufr  27048  frgrregord13  27108  kur14lem7  30899  3jaodd  31301  dfrdg2  31399  sltval2  31507  sltsgn1  31512  sltsgn2  31513  sltintdifex  31514  sltres  31515  sltsolem1  31525  nosepnelem  31562  dfrdg4  31697  iooelexlt  32839  relowlssretop  32840  wl-exeq  32950  iccpartiltu  40653  iccpartigtl  40654  icceuelpart  40667  fmtno4prmfac193  40781  fmtnofz04prm  40785  exple2lt6  41430
  Copyright terms: Public domain W3C validator