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

Theorem mpjaodan 761
Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule  \/ E ( \/ elimination), see natded 20896. (Contributed by Mario Carneiro, 29-May-2016.)
Hypotheses
Ref Expression
jaodan.1  |-  ( (
ph  /\  ps )  ->  ch )
jaodan.2  |-  ( (
ph  /\  th )  ->  ch )
jaodan.3  |-  ( ph  ->  ( ps  \/  th ) )
Assertion
Ref Expression
mpjaodan  |-  ( ph  ->  ch )

Proof of Theorem mpjaodan
StepHypRef Expression
1 jaodan.3 . 2  |-  ( ph  ->  ( ps  \/  th ) )
2 jaodan.1 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
3 jaodan.2 . . 3  |-  ( (
ph  /\  th )  ->  ch )
42, 3jaodan 760 . 2  |-  ( (
ph  /\  ( ps  \/  th ) )  ->  ch )
51, 4mpdan 649 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 357    /\ wa 358
This theorem is referenced by:  weniso  5936  isf32lem2  8067  isf32lem4  8069  fpwwe2lem11  8349  fpwwe2lem12  8350  lecasei  9013  ltlecasei  9015  xaddass  10658  xlesubadd  10672  xmulge0  10693  xadddi2  10706  xrsupss  10716  xrinfmss  10717  seqf1olem2  11175  expaddzlem  11235  discr  11328  fzomaxdif  11917  iseralt  12248  sumrb  12277  fsumtscopo  12351  fsumparts  12355  bitsf1  12728  smupvallem  12765  eucalgf  12844  eucalginv  12845  vdwmc2  13117  mreexmrid  13638  mreexexlem3d  13641  mulgnn0p1  14671  mulgnn0subcl  14673  mulgsubcl  14674  mulgneg  14678  mulgz  14681  mulgnn0dir  14683  mulgdirlem  14684  mulgdir  14685  submmulg  14695  ghmmulg  14788  odid  14946  oddvds  14955  dfod2  14970  gexid  14985  gexdvds  14988  mulgnn0di  15218  mulgdi  15219  gsumzsplit  15299  lsppratlem5  15997  prmirred  16548  1stckgenlem  17348  qtoprest  17508  tgpmulg  17872  tsmssplit  17930  xblss2  18054  nmoix  18334  nmoleub  18336  idnghm  18348  blcvx  18400  icccmp  18427  xrge0tsms  18436  metdstri  18452  nmoleub2lem  18693  ivthle  18914  ivthle2  18915  dyadmbl  19053  volivth  19060  itg2const2  19194  itg2mulc  19200  dvlip2  19440  dvfsumlem1  19471  mdegmullem  19562  coemulhi  19733  dgrcolem2  19753  coseq00topi  19971  abssinper  19987  cxplea  20148  cxple2  20149  cxple2a  20151  cxpcn3  20193  cxpaddlelem  20196  cxpaddle  20197  ang180lem3  20214  dcubic2  20245  birthdaylem2  20352  jensen  20388  ppiltx  20521  chtub  20557  bcmono  20622  bcmax  20623  bpos  20638  lgseisenlem1  20694  2sqlem4  20712  pntrlog2bndlem5  20836  pntpbnd1  20841  ex-natded5.7  20904  ex-natded5.13  20908  ex-natded9.20  20910  ex-natded9.20-2  20911  elpreq  23195  difioo  23344  ssnnssfz  23347  iundisjcnt  23355  hashge1  23362  xrsmulgzz  23396  ressmulgnn0  23398  xrge0addgt0  23406  xrge0adddir  23407  xrge0tsmsd  23415  xrge0mulc1cn  23483  qqhval2lem  23638  nnlogbexp  23670  esumcst  23721  esumpcvgval  23734  esumcvg  23742  sigaclcu3  23771  voliune  23849  volfiniune  23850  volmeas  23851  ntrivcvgtail  24529  prodrb  24559  fdc  25779  pell1qrgaplem  26281  monotoddzzfi  26350  oddcomabszz  26352  zindbi  26354  rmxnn  26361  jm2.24  26373  acongeq  26393  jm2.23  26412  jm2.26lem3  26417  wepwsolem  26461  fnchoice  27023  refsum2cnlem1  27031  bnj517  28662  bnj1408  28811  bnj1423  28826  bnj1452  28827  lsatcvat  29292  lkrpssN  29405  2at0mat0  29766  atmod1i1m  30099  lhp2at0nle  30276  trlcone  30969  tendoex  31216  dihlspsnssN  31574  dochkrsm  31700  lcfl8  31744  lclkrlem2b  31750  lclkrlem2s  31767  lcfrlem21  31805  mapdval2N  31872  mapdspex  31910
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  df-an 360
  Copyright terms: Public domain W3C validator