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

Theorem mpjaod 878
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 877 . 2 (𝜑 → ((𝜓𝜃) → 𝜒))
51, 4mpd 15 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 865
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 198  df-or 866
This theorem is referenced by:  ecase2d  1045  opth1  5146  sorpssun  7183  sorpssin  7184  reldmtpos  7604  dftpos4  7615  oaass  7887  nnawordex  7963  omabs  7973  suplub2  8615  en3lplem2  8764  cantnflt  8825  cantnfp1lem3  8833  tcrank  9003  cardaleph  9204  fpwwe2  9759  gchpwdom  9786  grur1  9936  indpi  10023  nn1suc  11337  nnsub  11356  seqid  13088  seqz  13091  faclbnd  13316  facavg  13327  bcval5  13344  hashnnn0genn0  13370  hashfzo  13452  sqrlem6  14230  resqrex  14233  absmod0  14285  absz  14293  iserex  14629  fsumf1o  14696  fsumss  14698  fsumcl2lem  14704  fsumadd  14712  fsummulc2  14757  fsumconst  14763  fsumrelem  14780  isumsplit  14813  fprodf1o  14916  fprodss  14918  fprodcl2lem  14920  fprodmul  14930  fproddiv  14931  fprodconst  14948  fprodn0  14949  absdvdsb  15242  dvdsabsb  15243  gcdabs1  15489  bezoutlem1  15494  bezoutlem2  15495  isprm5  15655  pcabs  15815  pockthg  15846  prmreclem5  15860  vdwlem13  15933  0ram  15960  ram0  15962  prmlem0  16043  mulgnn0ass  17799  psgnunilem2  18135  mndodcongi  18182  oddvdsnn0  18183  odnncl  18184  efgredlemb  18379  gsumzres  18530  gsumzcl2  18531  gsumzf1o  18533  gsumzaddlem  18541  gsumconst  18554  gsumzmhm  18557  gsummulglem  18561  gsumzoppg  18564  pgpfac1lem5  18699  mplsubrglem  19667  gsumfsum  20040  zringlpirlem1  20059  ordthaus  21422  icccmplem2  22859  metdstri  22887  ioombl  23568  itgabs  23837  dvlip  23992  dvge0  24005  dvivthlem1  24007  dvcnvrelem1  24016  ply1rem  24159  dgrcolem2  24266  quotcan  24300  sinq12ge0  24497  argregt0  24592  argrege0  24593  scvxcvx  24948  bpos1lem  25243  bposlem3  25247  lgseisenlem2  25337  frgrregord013  27605  htthlem  28124  atcvati  29595  sinccvglem  31909  noextendseq  32162  noetalem3  32207  midofsegid  32553  outsideofeq  32579  hfun  32627  ordcmp  32784  icoreclin  33539  itgabsnc  33809  dvasin  33826  cvrat  35220  4atlem10  35404  4atlem12  35410  cdleme18d  36093  cdleme22b  36139  cdleme32e  36243  lclkrlem2e  37309  pell1234qrdich  37944  clsk1indlem3  38858  suctrALT  39572  wallispilem3  40780  bgoldbtbnd  42289
  Copyright terms: Public domain W3C validator