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

Theorem mpjaodan 762
Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule  \/ E ( \/ elimination), see natded 21711. (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  6075  isf32lem2  8234  isf32lem4  8236  fpwwe2lem11  8515  fpwwe2lem12  8516  lecasei  9179  ltlecasei  9181  xaddass  10828  xlesubadd  10842  xmulge0  10863  xadddi2  10876  xrsupss  10887  xrinfmss  10888  seqf1olem2  11363  expaddzlem  11423  discr  11516  fzomaxdif  12147  iseralt  12478  sumrb  12507  fsumtscopo  12581  fsumparts  12585  bitsf1  12958  smupvallem  12995  eucalgf  13074  eucalginv  13075  vdwmc2  13347  mreexmrid  13868  mreexexlem3d  13871  mulgnn0p1  14901  mulgnn0subcl  14903  mulgsubcl  14904  mulgneg  14908  mulgz  14911  mulgnn0dir  14913  mulgdirlem  14914  mulgdir  14915  submmulg  14925  ghmmulg  15018  odid  15176  oddvds  15185  dfod2  15200  gexid  15215  gexdvds  15218  mulgnn0di  15448  mulgdi  15449  gsumzsplit  15529  lsppratlem5  16223  prmirred  16775  1stckgenlem  17585  qtoprest  17749  tgpmulg  18123  tsmssplit  18181  xblss2ps  18431  xblss2  18432  metustfbasOLD  18595  metustfbas  18596  nmoix  18763  nmoleub  18765  idnghm  18777  blcvx  18829  icccmp  18856  xrge0tsms  18865  metdstri  18881  nmoleub2lem  19122  ivthle  19353  ivthle2  19354  dyadmbl  19492  volivth  19499  itg2const2  19633  itg2mulc  19639  dvlip2  19879  dvfsumlem1  19910  mdegmullem  20001  coemulhi  20172  dgrcolem2  20192  coseq00topi  20410  abssinper  20426  cxplea  20587  cxple2  20588  cxple2a  20590  cxpcn3  20632  cxpaddlelem  20635  cxpaddle  20636  ang180lem3  20653  dcubic2  20684  birthdaylem2  20791  jensen  20827  ppiltx  20960  chtub  20996  bcmono  21061  bcmax  21062  bpos  21077  lgseisenlem1  21133  2sqlem4  21151  pntrlog2bndlem5  21275  pntpbnd1  21280  ex-natded5.7  21719  ex-natded5.13  21723  ex-natded9.20  21725  ex-natded9.20-2  21726  difioo  24145  iundisjcnt  24154  xrsmulgzz  24200  ressmulgnn0  24206  xrge0addgt0  24214  xrge0adddir  24215  xrge0tsmsd  24223  xrge0mulc1cn  24327  qqhval2lem  24365  esumpcvgval  24468  esumcvg  24476  sigaclcu3  24505  measiuns  24571  voliune  24585  volfiniune  24586  volmeas  24587  ntrivcvgtail  25228  prodrb  25258  fdc  26449  pell1qrgaplem  26936  monotoddzzfi  27005  oddcomabszz  27007  zindbi  27009  rmxnn  27016  jm2.24  27028  acongeq  27048  jm2.23  27067  jm2.26lem3  27072  wepwsolem  27116  fnchoice  27676  refsum2cnlem1  27684  wallispilem3  27792  bnj517  29256  bnj1408  29405  bnj1423  29420  bnj1452  29421  lsatcvat  29848  lkrpssN  29961  2at0mat0  30322  atmod1i1m  30655  lhp2at0nle  30832  trlcone  31525  tendoex  31772  dihlspsnssN  32130  dochkrsm  32256  lcfl8  32300  lclkrlem2b  32306  lclkrlem2s  32323  lcfrlem21  32361  mapdval2N  32428  mapdspex  32466
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