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

Theorem mpjaod 394
Description: Eliminate a disjunction in a deduction. (Contributed by Mario Carneiro, 29-May-2016.)
Hypotheses
Ref Expression
jaod.1 (𝜑 → (𝜓𝜒))
jaod.2 (𝜑 → (𝜃𝜒))
jaod.3 (𝜑 → (𝜓𝜃))
Assertion
Ref Expression
mpjaod (𝜑𝜒)

Proof of Theorem mpjaod
StepHypRef Expression
1 jaod.3 . 2 (𝜑 → (𝜓𝜃))
2 jaod.1 . . 3 (𝜑 → (𝜓𝜒))
3 jaod.2 . . 3 (𝜑 → (𝜃𝜒))
42, 3jaod 393 . 2 (𝜑 → ((𝜓𝜃) → 𝜒))
51, 4mpd 15 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 381
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 195  df-or 383
This theorem is referenced by:  ecase2d  977  opth1  4864  sorpssun  6820  sorpssin  6821  reldmtpos  7225  dftpos4  7236  oaass  7506  nnawordex  7582  omabs  7592  suplub2  8228  en3lplem2  8373  cantnflt  8430  cantnfp1lem3  8438  tcrank  8608  cardaleph  8773  fpwwe2  9322  gchpwdom  9349  grur1  9499  indpi  9586  nn1suc  10891  nnsub  10909  seqid  12666  seqz  12669  faclbnd  12897  facavg  12908  bcval5  12925  hashnnn0genn0  12948  hashfzo  13031  sqrlem6  13785  resqrex  13788  absmod0  13840  absz  13848  iserex  14184  fsumf1o  14250  fsumss  14252  fsumcl2lem  14258  fsumadd  14266  fsummulc2  14307  fsumconst  14313  fsumrelem  14329  isumsplit  14360  fprodf1o  14464  fprodss  14466  fprodcl2lem  14468  fprodmul  14478  fproddiv  14479  fprodconst  14496  fprodn0  14497  absdvdsb  14787  dvdsabsb  14788  gcdabs1  15038  bezoutlem1  15043  bezoutlem2  15044  isprm5  15206  pcabs  15366  pockthg  15397  prmreclem5  15411  vdwlem13  15484  0ram  15511  ram0  15513  prmlem0  15599  mulgnn0ass  17350  psgnunilem2  17687  mndodcongi  17734  oddvdsnn0  17735  odnncl  17736  efgredlemb  17931  gsumzres  18082  gsumzcl2  18083  gsumzf1o  18085  gsumzaddlem  18093  gsumconst  18106  gsumzmhm  18109  gsummulglem  18113  gsumzoppg  18116  pgpfac1lem5  18250  mplsubrglem  19209  gsumfsum  19581  zringlpirlem1  19600  ordthaus  20946  icccmplem2  22382  metdstri  22410  ioombl  23085  itgabs  23352  dvlip  23505  dvge0  23518  dvivthlem1  23520  dvcnvrelem1  23529  ply1rem  23672  dgrcolem2  23779  quotcan  23813  sinq12ge0  24009  argregt0  24105  argrege0  24106  scvxcvx  24457  bpos1lem  24752  bposlem3  24756  lgseisenlem2  24846  frgraregord013  26439  htthlem  26992  atcvati  28463  sinccvglem  30654  midofsegid  31215  outsideofeq  31241  hfun  31289  ordcmp  31450  icoreclin  32205  itgabsnc  32473  dvasin  32490  cvrat  33550  4atlem10  33734  4atlem12  33740  cdleme18d  34424  cdleme22b  34471  cdleme32e  34575  lclkrlem2e  35642  pell1234qrdich  36267  clsk1indlem3  37185  suctrALT  37907  wallispilem3  38784  bgoldbtbnd  40050  av-frgraregord013  41571
  Copyright terms: Public domain W3C validator