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

Theorem mpjaod 859
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 858 . 2 (𝜑 → ((𝜓𝜃) → 𝜒))
51, 4mpd 15 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 846
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-or 847
This theorem is referenced by:  ecase2dOLD  1030  opth1  5433  onun2  6426  sorpssun  7668  sorpssin  7669  poxp2  8076  poxp3  8083  reldmtpos  8166  dftpos4  8177  oaass  8509  nnawordex  8585  omabs  8598  suplub2  9398  en3lplem2  9550  cantnflt  9609  cantnfp1lem3  9617  ttrclselem2  9663  tcrank  9821  cardaleph  10026  fpwwe2  10580  gchpwdom  10607  grur1  10757  indpi  10844  nn1suc  12176  nnsub  12198  seqid  13954  seqz  13957  faclbnd  14191  facavg  14202  bcval5  14219  hashnnn0genn0  14244  hashfzo  14330  01sqrexlem6  15133  resqrex  15136  absmod0  15189  absz  15197  iserex  15542  fsumf1o  15609  fsumss  15611  fsumcl2lem  15617  fsumadd  15626  fsummulc2  15670  fsumconst  15676  fsumrelem  15693  isumsplit  15726  fprodf1o  15830  fprodss  15832  fprodcl2lem  15834  fprodmul  15844  fproddiv  15845  fprodconst  15862  fprodn0  15863  absdvdsb  16158  dvdsabsb  16159  gcdabs1  16410  bezoutlem1  16421  bezoutlem2  16422  2mulprm  16570  isprm5  16584  pcabs  16748  pockthg  16779  prmreclem5  16793  vdwlem13  16866  0ram  16893  ram0  16895  prmlem0  16979  mulgnn0ass  18913  psgnunilem2  19278  mndodcongi  19326  oddvdsnn0  19327  odnncl  19328  efgredlemb  19529  gsumzres  19687  gsumzcl2  19688  gsumzf1o  19690  gsumzaddlem  19699  gsumconst  19712  gsumzmhm  19715  gsummulglem  19719  gsumzoppg  19722  pgpfac1lem5  19859  ablsimpnosubgd  19884  gsumfsum  20867  zringlpirlem1  20886  mplsubrglem  21413  ordthaus  22738  icccmplem2  24189  metdstri  24217  ioombl  24932  itgabs  25202  dvlip  25360  dvge0  25373  dvivthlem1  25375  dvcnvrelem1  25384  ply1rem  25531  dgrcolem2  25638  quotcan  25672  sinq12ge0  25868  argregt0  25968  argrege0  25969  scvxcvx  26338  bpos1lem  26633  bposlem3  26637  lgseisenlem2  26727  noextendseq  27018  nogt01o  27047  nosupprefixmo  27051  noinfprefixmo  27052  noinfbnd1lem5  27078  noetasuplem4  27087  noetainflem4  27091  frgrregord013  29342  htthlem  29862  atcvati  31331  ccatf1  31808  sinccvglem  34263  midofsegid  34692  outsideofeq  34718  hfun  34766  ordcmp  34922  icoreclin  35831  itgabsnc  36150  dvasin  36165  cvrat  37888  4atlem10  38072  4atlem12  38078  cdleme18d  38761  cdleme22b  38807  cdleme32e  38911  lclkrlem2e  39977  aks4d1p1  40536  pell1234qrdich  41187  onsupnmax  41565  omlimcl2  41579  onexlimgt  41580  onexoegt  41581  onsucf1olem  41608  oege1  41643  cantnfresb  41661  omabs2  41668  clsk1indlem3  42322  suctrALT  43115  wallispilem3  44315  bgoldbtbnd  46008  reorelicc  46803
  Copyright terms: Public domain W3C validator