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

Theorem mpjaod 395
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 394 . 2 (𝜑 → ((𝜓𝜃) → 𝜒))
51, 4mpd 15 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 382
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 384
This theorem is referenced by:  ecase2d  1018  opth1  5092  sorpssun  7110  sorpssin  7111  reldmtpos  7530  dftpos4  7541  oaass  7812  nnawordex  7888  omabs  7898  suplub2  8534  en3lplem2  8683  cantnflt  8744  cantnfp1lem3  8752  tcrank  8922  cardaleph  9122  fpwwe2  9677  gchpwdom  9704  grur1  9854  indpi  9941  nn1suc  11253  nnsub  11271  seqid  13060  seqz  13063  faclbnd  13291  facavg  13302  bcval5  13319  hashnnn0genn0  13345  hashfzo  13428  sqrlem6  14207  resqrex  14210  absmod0  14262  absz  14270  iserex  14606  fsumf1o  14673  fsumss  14675  fsumcl2lem  14681  fsumadd  14689  fsummulc2  14735  fsumconst  14741  fsumrelem  14758  isumsplit  14791  fprodf1o  14895  fprodss  14897  fprodcl2lem  14899  fprodmul  14909  fproddiv  14910  fprodconst  14927  fprodn0  14928  absdvdsb  15222  dvdsabsb  15223  gcdabs1  15473  bezoutlem1  15478  bezoutlem2  15479  isprm5  15641  pcabs  15801  pockthg  15832  prmreclem5  15846  vdwlem13  15919  0ram  15946  ram0  15948  prmlem0  16034  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  18698  mplsubrglem  19661  gsumfsum  20035  zringlpirlem1  20054  ordthaus  21410  icccmplem2  22847  metdstri  22875  ioombl  23553  itgabs  23820  dvlip  23975  dvge0  23988  dvivthlem1  23990  dvcnvrelem1  23999  ply1rem  24142  dgrcolem2  24249  quotcan  24283  sinq12ge0  24480  argregt0  24576  argrege0  24577  scvxcvx  24932  bpos1lem  25227  bposlem3  25231  lgseisenlem2  25321  frgrregord013  27584  htthlem  28104  atcvati  29575  sinccvglem  31894  noextendseq  32147  noetalem3  32192  midofsegid  32538  outsideofeq  32564  hfun  32612  ordcmp  32773  icoreclin  33534  itgabsnc  33810  dvasin  33827  cvrat  35229  4atlem10  35413  4atlem12  35419  cdleme18d  36103  cdleme22b  36149  cdleme32e  36253  lclkrlem2e  37320  pell1234qrdich  37945  clsk1indlem3  38861  suctrALT  39578  wallispilem3  40805  bgoldbtbnd  42225
  Copyright terms: Public domain W3C validator