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

Theorem mpjaod 371
Description: Eliminate a disjunction in a deduction. (Contributed by Mario Carneiro, 29-May-2016.)
Hypotheses
Ref Expression
jaod.1  |-  ( ph  ->  ( ps  ->  ch ) )
jaod.2  |-  ( ph  ->  ( th  ->  ch ) )
jaod.3  |-  ( ph  ->  ( ps  \/  th ) )
Assertion
Ref Expression
mpjaod  |-  ( ph  ->  ch )

Proof of Theorem mpjaod
StepHypRef Expression
1 jaod.3 . 2  |-  ( ph  ->  ( ps  \/  th ) )
2 jaod.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
3 jaod.2 . . 3  |-  ( ph  ->  ( th  ->  ch ) )
42, 3jaod 370 . 2  |-  ( ph  ->  ( ( ps  \/  th )  ->  ch )
)
51, 4mpd 15 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 358
This theorem is referenced by:  ecase2d  907  opth1  4368  reldmtpos  6416  dftpos4  6427  sorpssun  6458  sorpssin  6459  oaass  6733  nnawordex  6809  omabs  6819  suplub2  7392  cantnflt  7553  cantnfp1lem3  7562  en3lplem2  7597  tcrank  7734  cardaleph  7896  fpwwe2  8444  gchpwdom  8475  grur1  8621  indpi  8710  nn1suc  9946  nnsub  9963  seqid  11288  seqz  11291  faclbnd  11501  facavg  11512  bcval5  11529  hashnnn0genn0  11547  hashfzo  11614  sqrlem6  11973  resqrex  11976  absmod0  12028  absz  12036  iserex  12370  fsumf1o  12437  fsumss  12439  fsumcl2lem  12445  fsumadd  12452  fsummulc2  12487  fsumconst  12493  fsumrelem  12506  isumsplit  12540  absdvdsb  12788  dvdsabsb  12789  gcdabs1  12954  bezoutlem1  12958  bezoutlem2  12959  isprm5  13032  pcabs  13168  pockthg  13194  prmreclem5  13208  vdwlem13  13281  0ram  13308  ram0  13310  prmlem0  13348  mulgnn0ass  14839  mndodcongi  15101  oddvdsnn0  15102  odnncl  15103  efgredlemb  15298  gsumzres  15437  gsumzcl  15438  gsumzf1o  15439  gsumzaddlem  15446  gsumconst  15452  gsumzmhm  15453  gsummulglem  15456  gsumzoppg  15459  pgpfac1lem5  15557  mplsubrglem  16422  gsumfsum  16682  zlpirlem1  16684  ordthaus  17363  icccmplem2  18718  metdstri  18745  ioombl  19319  itgabs  19586  dvlip  19737  dvge0  19750  dvivthlem1  19752  dvcnvrelem1  19761  ply1rem  19946  dgrcolem2  20052  quotcan  20086  sinq12ge0  20276  argregt0  20365  argrege0  20366  scvxcvx  20684  bpos1lem  20926  bposlem3  20930  lgseisenlem2  20994  gxneg  21695  gxsuc  21701  gxadd  21704  gxmul  21707  htthlem  22261  atcvati  23730  sinccvglem  24881  fprodf1o  25044  fprodss  25046  fprodcl2lem  25048  fprodmul  25056  fproddiv  25057  fprodconst  25074  fprodn0  25075  midofsegid  25745  outsideofeq  25771  hfun  25826  ordcmp  25904  itgabsnc  25967  pell1234qrdich  26608  psgnunilem2  27080  wallispilem3  27477  cvrat  29587  4atlem10  29771  4atlem12  29777  cdleme18d  30460  cdleme22b  30506  cdleme32e  30610  lclkrlem2e  31677
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-or 360
  Copyright terms: Public domain W3C validator