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

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

Proof of Theorem mpjaodan
StepHypRef Expression
1 jaodan.3 . 2
2 jaodan.1 . . 3
3 jaodan.2 . . 3
42, 3jaodan 785 . 2
51, 4mpdan 668 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  \/wo 368  /\wa 369
This theorem is referenced by:  mpjao3dan  1295  weniso  6250  isf32lem2  8755  isf32lem4  8757  fpwwe2lem11  9039  fpwwe2lem12  9040  lecasei  9711  ltlecasei  9713  xaddass  11470  xlesubadd  11484  xmulge0  11505  xadddi2  11518  xrsupss  11529  xrinfmss  11530  fzm1  11787  seqf1olem2  12147  expaddzlem  12209  discr  12303  fzomaxdif  13176  iseralt  13507  sumrb  13535  telfsumo  13616  fsumparts  13620  ntrivcvgtail  13709  prodrb  13739  bitsf1  14096  smupvallem  14133  eucalgf  14212  eucalginv  14213  vdwmc2  14497  mreexmrid  15040  mreexexlem3d  15043  mulgnn0p1  16153  mulgnn0subcl  16155  mulgsubcl  16156  mulgneg  16160  mulgz  16163  mulgnn0dir  16165  mulgdirlem  16166  mulgdir  16167  submmulg  16177  ghmmulg  16279  odid  16562  oddvds  16571  dfod2  16586  gexid  16601  gexdvds  16604  mulgnn0di  16834  mulgdi  16835  gsumzsplit  16944  gsumzsplitOLD  16945  lsppratlem5  17797  prmirred  18525  prmirredOLD  18528  1stckgenlem  20054  qtoprest  20218  tgpmulg  20592  tsmssplit  20654  xblss2ps  20904  xblss2  20905  metustfbasOLD  21068  metustfbas  21069  nmoix  21236  nmoleub  21238  idnghm  21250  blcvx  21303  icccmp  21330  xrge0tsms  21339  metdstri  21355  nmoleub2lem  21597  rrxcph  21824  rrxdstprj1  21836  ivthle  21868  ivthle2  21869  dyadmbl  22009  volivth  22016  itg2const2  22148  itg2mulc  22154  dvlip2  22396  dvfsumlem1  22427  mdegmullem  22478  coemulhi  22651  dgrcolem2  22671  coseq00topi  22895  abssinper  22911  cxplea  23077  cxple2  23078  cxple2a  23080  cxpcn3  23122  cxpaddlelem  23125  cxpaddle  23126  ang180lem3  23143  dcubic2  23175  birthdaylem2  23282  jensen  23318  ppiltx  23451  chtub  23487  bcmono  23552  bcmax  23553  bpos  23568  lgseisenlem1  23624  2sqlem4  23642  pntrlog2bndlem5  23766  pntpbnd1  23771  tgldimor  23893  tgifscgr  23900  tgcgrxfr  23909  tgbtwnconn1  23962  tgbtwnconn2  23963  tgbtwnconn3  23964  tgbtwnconnln3  23965  tgbtwnconn22  23966  tgbtwnconnln1  23967  tgbtwnconnln2  23968  legtrid  23978  legbtwn  23981  legov3  23984  hlln  23991  hltr  23994  btwnhl  23998  ncolncol  24026  mirconn  24058  krippen  24068  midexlem  24069  midex  24111  opphllem2  24120  opphllem5  24123  opphllem6  24124  ex-natded5.7  25132  ex-natded5.13  25136  ex-natded9.20  25138  ex-natded9.20-2  25139  xrge0infss  27580  difioo  27593  iundisjcnt  27603  2sqmod  27636  xrsmulgzz  27666  ressmulgnn0  27672  xrge0addgt0  27681  xrge0adddir  27682  archirngz  27733  archiabllem2a  27738  xrge0tsmsd  27775  locfinref  27844  xrge0mulc1cn  27923  qqhval2lem  27962  nexple  28005  esumpcvgval  28084  esumcvg  28092  sigaclcu3  28122  measiuns  28188  voliune  28201  volfiniune  28202  volmeas  28203  sgncl  28477  sgnmul  28481  gsumnunsn  28493  signsply0  28508  signswch  28518  signslema  28519  signstfvneq0  28529  fdc  30238  orel  30504  pell1qrgaplem  30809  monotoddzzfi  30878  oddcomabszz  30880  zindbi  30882  rmxnn  30889  jm2.24  30901  acongeq  30921  jm2.23  30938  jm2.26lem3  30943  wepwsolem  30987  fnchoice  31404  refsum2cnlem1  31412  wallispilem3  31849  bnj517  33943  bnj1408  34092  bnj1423  34107  bnj1452  34108  lsatcvat  34775  lkrpssN  34888  2at0mat0  35249  atmod1i1m  35582  lhp2at0nle  35759  trlcone  36454  tendoex  36701  dihlspsnssN  37059  dochkrsm  37185  lcfl8  37229  lclkrlem2b  37235  lclkrlem2s  37252  lcfrlem21  37290  mapdval2N  37357  mapdspex  37395
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371
  Copyright terms: Public domain W3C validator