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

Theorem 3jaoi 1426
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 1338 . 2 ((𝜑𝜓) ∧ (𝜒𝜓) ∧ (𝜃𝜓))
5 3jao 1424 . 2 (((𝜑𝜓) ∧ (𝜒𝜓) ∧ (𝜃𝜓)) → ((𝜑𝜒𝜃) → 𝜓))
64, 5ax-mp 5 1 ((𝜑𝜒𝜃) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3o 1085  w3a 1086
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 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088
This theorem is referenced by:  3jaoian  1428  tpres  7204  ordzsl  7838  onzsl  7839  tfrlem16  8399  oawordeulem  8560  fsetexb  8864  elfiun  9431  infsupprpr  9505  domtriomlem  10443  axdc3lem2  10452  rankcf  10778  znegcl  12604  xrltnr  13106  xnegcl  13199  xnegneg  13200  xltnegi  13202  xnegid  13224  xaddrid  13227  xmulrid  13265  xrsupsslem  13293  xrinfmsslem  13294  reltxrnmnf  13328  elfznelfzo  13744  addmodlteq  13918  hashle2pr  14445  hashge2el2difr  14449  hashtpg  14453  hash1to3  14459  swrdnd0  14614  prm23lt5  16754  prm23ge5  16755  cshwshashlem1  17036  01eq0ringOLD  20427  ioombl1  25411  2irrexpq  26579  ppiublem1  27048  zabsle1  27142  gausslemma2dlem0f  27207  gausslemma2dlem0i  27210  gausslemma2dlem4  27215  2lgsoddprm  27262  ostth  27485  sltval2  27502  sltintdifex  27507  sltres  27508  sltsolem1  27521  nosepnelem  27525  nb3grprlem1  29070  pthdivtx  29419  frgr3vlem1  29959  frgr3vlem2  29960  frgrwopreg  30009  frgrregorufr  30011  frgrregord13  30082  kur14lem7  34667  3jaodd  35154  dfrdg2  35237  dfrdg4  35393  iooelexlt  36707  relowlssretop  36708  wl-exeq  36867  iccpartiltu  46549  iccpartigtl  46550  icceuelpart  46563  prproropf1olem4  46633  fmtno4prmfac193  46700  fmtnofz04prm  46704  mogoldbblem  46847  exple2lt6  47203
  Copyright terms: Public domain W3C validator