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  4260  reldmtpos  6258  dftpos4  6269  sorpssun  6300  sorpssin  6301  oaass  6575  nnawordex  6651  omabs  6661  suplub2  7228  cantnflt  7389  cantnfp1lem3  7398  en3lplem2  7433  tcrank  7570  cardaleph  7732  fpwwe2  8281  gchpwdom  8312  grur1  8458  indpi  8547  nn1suc  9783  nnsub  9800  seqid  11107  seqz  11110  faclbnd  11319  facavg  11330  bcval5  11346  hashfzo  11399  sqrlem6  11749  resqrex  11752  absmod0  11804  absz  11812  iserex  12146  fsumf1o  12212  fsumss  12214  fsumcl2lem  12220  fsumadd  12227  fsummulc2  12262  fsumconst  12268  fsumrelem  12281  isumsplit  12315  absdvdsb  12563  dvdsabsb  12564  gcdabs1  12729  bezoutlem1  12733  bezoutlem2  12734  isprm5  12807  pcabs  12943  pockthg  12969  prmreclem5  12983  vdwlem13  13056  0ram  13083  ram0  13085  prmlem0  13123  mulgnn0ass  14612  mndodcongi  14874  oddvdsnn0  14875  odnncl  14876  efgredlemb  15071  gsumzres  15210  gsumzcl  15211  gsumzf1o  15212  gsumzaddlem  15219  gsumconst  15225  gsumzmhm  15226  gsummulglem  15229  gsumzoppg  15232  pgpfac1lem5  15330  mplsubrglem  16199  gsumfsum  16455  zlpirlem1  16457  ordthaus  17128  icccmplem2  18344  metdstri  18371  ioombl  18938  itgabs  19205  dvlip  19356  dvge0  19369  dvivthlem1  19371  dvcnvrelem1  19380  ply1rem  19565  dgrcolem2  19671  quotcan  19705  sinq12ge0  19892  argregt0  19980  argrege0  19981  scvxcvx  20296  bpos1lem  20537  bposlem3  20541  lgseisenlem2  20605  gxneg  20949  gxsuc  20955  gxadd  20958  gxmul  20961  htthlem  21513  atcvati  22982  sinccvglem  24020  fprodf1o  24172  midofsegid  24799  outsideofeq  24825  ordcmp  24958  itgabsnc  25020  pell1234qrdich  27049  psgnunilem2  27521  wallispilem3  27919  cvrat  30233  4atlem10  30417  4atlem12  30423  cdleme18d  31106  cdleme22b  31152  cdleme32e  31256  lclkrlem2e  32323
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