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

Theorem mpjaod 370
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 369 . 2  |-  ( ph  ->  ( ( ps  \/  th )  ->  ch )
)
51, 4mpd 14 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 357
This theorem is referenced by:  ecase2d  906  opth1  4244  reldmtpos  6242  dftpos4  6253  sorpssun  6284  sorpssin  6285  oaass  6559  nnawordex  6635  omabs  6645  suplub2  7212  cantnflt  7373  cantnfp1lem3  7382  en3lplem2  7417  tcrank  7554  cardaleph  7716  fpwwe2  8265  gchpwdom  8296  grur1  8442  indpi  8531  nn1suc  9767  nnsub  9784  seqid  11091  seqz  11094  faclbnd  11303  facavg  11314  bcval5  11330  hashfzo  11383  sqrlem6  11733  resqrex  11736  absmod0  11788  absz  11796  iserex  12130  fsumf1o  12196  fsumss  12198  fsumcl2lem  12204  fsumadd  12211  fsummulc2  12246  fsumconst  12252  fsumrelem  12265  isumsplit  12299  absdvdsb  12547  dvdsabsb  12548  gcdabs1  12713  bezoutlem1  12717  bezoutlem2  12718  isprm5  12791  pcabs  12927  pockthg  12953  prmreclem5  12967  vdwlem13  13040  0ram  13067  ram0  13069  prmlem0  13107  mulgnn0ass  14596  mndodcongi  14858  oddvdsnn0  14859  odnncl  14860  efgredlemb  15055  gsumzres  15194  gsumzcl  15195  gsumzf1o  15196  gsumzaddlem  15203  gsumconst  15209  gsumzmhm  15210  gsummulglem  15213  gsumzoppg  15216  pgpfac1lem5  15314  mplsubrglem  16183  gsumfsum  16439  zlpirlem1  16441  ordthaus  17112  icccmplem2  18328  metdstri  18355  ioombl  18922  itgabs  19189  dvlip  19340  dvge0  19353  dvivthlem1  19355  dvcnvrelem1  19364  ply1rem  19549  dgrcolem2  19655  quotcan  19689  sinq12ge0  19876  argregt0  19964  argrege0  19965  scvxcvx  20280  bpos1lem  20521  bposlem3  20525  lgseisenlem2  20589  gxneg  20933  gxsuc  20939  gxadd  20942  gxmul  20945  htthlem  21497  atcvati  22966  sinccvglem  24005  midofsegid  24727  outsideofeq  24753  ordcmp  24886  pell1234qrdich  26946  psgnunilem2  27418  wallispilem3  27816  cvrat  29611  4atlem10  29795  4atlem12  29801  cdleme18d  30484  cdleme22b  30530  cdleme32e  30634  lclkrlem2e  31701
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 177  df-or 359
  Copyright terms: Public domain W3C validator