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

Theorem mpjaodan 762
Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule  \/ E ( \/ elimination), see natded 21664. (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 761 . 2  |-  ( (
ph  /\  ( ps  \/  th ) )  ->  ch )
51, 4mpdan 650 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 358    /\ wa 359
This theorem is referenced by:  weniso  6034  isf32lem2  8190  isf32lem4  8192  fpwwe2lem11  8471  fpwwe2lem12  8472  lecasei  9135  ltlecasei  9137  xaddass  10784  xlesubadd  10798  xmulge0  10819  xadddi2  10832  xrsupss  10843  xrinfmss  10844  seqf1olem2  11318  expaddzlem  11378  discr  11471  fzomaxdif  12102  iseralt  12433  sumrb  12462  fsumtscopo  12536  fsumparts  12540  bitsf1  12913  smupvallem  12950  eucalgf  13029  eucalginv  13030  vdwmc2  13302  mreexmrid  13823  mreexexlem3d  13826  mulgnn0p1  14856  mulgnn0subcl  14858  mulgsubcl  14859  mulgneg  14863  mulgz  14866  mulgnn0dir  14868  mulgdirlem  14869  mulgdir  14870  submmulg  14880  ghmmulg  14973  odid  15131  oddvds  15140  dfod2  15155  gexid  15170  gexdvds  15173  mulgnn0di  15403  mulgdi  15404  gsumzsplit  15484  lsppratlem5  16178  prmirred  16730  1stckgenlem  17538  qtoprest  17702  tgpmulg  18076  tsmssplit  18134  xblss2ps  18384  xblss2  18385  metustfbasOLD  18548  metustfbas  18549  nmoix  18716  nmoleub  18718  idnghm  18730  blcvx  18782  icccmp  18809  xrge0tsms  18818  metdstri  18834  nmoleub2lem  19075  ivthle  19306  ivthle2  19307  dyadmbl  19445  volivth  19452  itg2const2  19586  itg2mulc  19592  dvlip2  19832  dvfsumlem1  19863  mdegmullem  19954  coemulhi  20125  dgrcolem2  20145  coseq00topi  20363  abssinper  20379  cxplea  20540  cxple2  20541  cxple2a  20543  cxpcn3  20585  cxpaddlelem  20588  cxpaddle  20589  ang180lem3  20606  dcubic2  20637  birthdaylem2  20744  jensen  20780  ppiltx  20913  chtub  20949  bcmono  21014  bcmax  21015  bpos  21030  lgseisenlem1  21086  2sqlem4  21104  pntrlog2bndlem5  21228  pntpbnd1  21233  ex-natded5.7  21672  ex-natded5.13  21676  ex-natded9.20  21678  ex-natded9.20-2  21679  difioo  24098  iundisjcnt  24107  xrsmulgzz  24153  ressmulgnn0  24159  xrge0addgt0  24167  xrge0adddir  24168  xrge0tsmsd  24176  xrge0mulc1cn  24280  qqhval2lem  24318  esumpcvgval  24421  esumcvg  24429  sigaclcu3  24458  measiuns  24524  voliune  24538  volfiniune  24539  volmeas  24540  ntrivcvgtail  25181  prodrb  25211  fdc  26339  pell1qrgaplem  26826  monotoddzzfi  26895  oddcomabszz  26897  zindbi  26899  rmxnn  26906  jm2.24  26918  acongeq  26938  jm2.23  26957  jm2.26lem3  26962  wepwsolem  27006  fnchoice  27567  refsum2cnlem1  27575  wallispilem3  27683  bnj517  28962  bnj1408  29111  bnj1423  29126  bnj1452  29127  lsatcvat  29533  lkrpssN  29646  2at0mat0  30007  atmod1i1m  30340  lhp2at0nle  30517  trlcone  31210  tendoex  31457  dihlspsnssN  31815  dochkrsm  31941  lcfl8  31985  lclkrlem2b  31991  lclkrlem2s  32008  lcfrlem21  32046  mapdval2N  32113  mapdspex  32151
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  df-an 361
  Copyright terms: Public domain W3C validator