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

Theorem mpjaodan 952
Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule E ( elimination), see natded 28109. (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 951 . 2 ((𝜑 ∧ (𝜓𝜃)) → 𝜒)
51, 4mpdan 683 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wo 841
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 208  df-an 397  df-or 842
This theorem is referenced by:  mpjao3dan  1423  weniso  7096  isf32lem2  9764  isf32lem4  9766  fpwwe2lem11  10050  fpwwe2lem12  10051  lecasei  10734  ltlecasei  10736  xaddass  12630  xlesubadd  12644  xmulge0  12665  xadddi2  12678  xrsupss  12690  xrinfmss  12691  fzm1  12975  seqf1olem2  13398  expaddzlem  13460  discr  13589  fzomaxdif  14691  iseralt  15029  sumrb  15058  telfsumo  15145  fsumparts  15149  ntrivcvgtail  15244  prodrb  15274  bitsf1  15783  smupvallem  15820  eucalgf  15915  eucalginv  15916  vdwmc2  16303  fvprif  16822  mreexmrid  16902  mreexexlem3d  16905  mulgfval  18164  mulgnn0p1  18177  mulgnn0subcl  18179  mulgsubcl  18180  mulgneg  18184  mulgz  18193  mulgnn0dir  18195  mulgdirlem  18196  mulgdir  18197  submmulg  18209  ghmmulg  18308  odid  18595  oddvds  18604  dfod2  18620  gexid  18635  gexdvds  18638  mulgnn0di  18875  mulgdi  18876  gsumzsplit  18976  2nsgsimpgd  19153  prmgrpsimpgd  19165  lsppratlem5  19852  prmirred  20570  1stckgenlem  22089  qtoprest  22253  tgpmulg  22629  tsmssplit  22687  xblss2ps  22938  xblss2  22939  metustfbas  23094  nmoix  23265  nmoleub  23267  idnghm  23279  blcvx  23333  icccmp  23360  xrge0tsms  23369  metdstri  23386  nmoleub2lem  23645  rrxcph  23922  rrxdstprj1  23939  ivthle  23984  ivthle2  23985  dyadmbl  24128  volivth  24135  itg2const2  24269  itg2mulc  24275  dvlip2  24519  dvfsumlem1  24550  mdegmullem  24599  coemulhi  24771  dgrcolem2  24791  coseq00topi  25015  abssinper  25033  cxplea  25206  cxple2  25207  cxple2a  25209  cxpcn3  25256  cxpaddlelem  25259  cxpaddle  25260  ang180lem3  25316  dcubic2  25349  birthdaylem2  25457  jensen  25493  ppiltx  25681  chtub  25715  bcmono  25780  bcmax  25781  bpos  25796  lgseisenlem1  25878  2sqlem4  25924  2sqmod  25939  pntrlog2bndlem5  26084  pntpbnd1  26089  tgldimor  26215  tgifscgr  26221  tgcgrxfr  26231  tgbtwnconn1  26288  tgbtwnconn2  26289  tgbtwnconn3  26290  tgbtwnconnln3  26291  tgbtwnconn22  26292  tgbtwnconnln1  26293  tgbtwnconnln2  26294  legtrid  26304  legbtwn  26307  tgcgrsub2  26308  legov3  26311  hlln  26320  hltr  26323  btwnhl  26327  ncolncol  26359  mirconn  26391  krippen  26404  midexlem  26405  midex  26450  opphllem2  26461  opphllem5  26464  opphllem6  26465  outpasch  26468  hlpasch  26469  trgcopyeulem  26518  cgrahl  26540  cgracol  26541  ex-natded5.7  28117  ex-natded5.13  28121  ex-natded9.20  28123  ex-natded9.20-2  28124  suppovss  30354  xrge0infss  30410  xnn0gt0  30420  nn0xmulclb  30422  difioo  30431  iundisjcnt  30447  f1ocnt  30451  hashxpe  30455  xrsmulgzz  30592  ressmulgnn0  30598  xrge0addgt0  30605  xrge0adddir  30606  xrge0tsmsd  30619  tocyc01  30687  cycpmco2lem4  30698  cycpmco2lem7  30701  cycpmco2  30702  cyc3co2  30709  cycpmrn  30712  archirngz  30745  archiabllem2a  30750  lindsun  30920  lbsdiflsp0  30921  submateq  30973  lmat22lem  30981  locfinref  31004  xrge0mulc1cn  31083  qqhval2lem  31121  nexple  31167  esumpcvgval  31236  esumcvg  31244  sigaclcu3  31280  measiuns  31375  voliune  31387  volfiniune  31388  volmeas  31389  sgncl  31695  sgnmul  31699  gsumnunsn  31710  signsply0  31720  signswch  31730  signslema  31731  signstfvneq0  31741  chtvalz  31799  bnj517  32056  bnj1408  32205  bnj1423  32220  bnj1452  32221  noetalem3  33116  dnibndlem13  33726  dnibnd  33727  poimirlem2  34775  fdc  34901  orel  35261  lsatcvat  36066  lkrpssN  36179  2at0mat0  36541  atmod1i1m  36874  lhp2at0nle  37051  trlcone  37744  tendoex  37991  dihlspsnssN  38348  dochkrsm  38474  lcfl8  38518  lclkrlem2b  38524  lclkrlem2s  38541  lcfrlem21  38579  mapdval2N  38646  mapdspex  38684  pell1qrgaplem  39348  monotoddzzfi  39417  oddcomabszz  39419  zindbi  39421  rmxnn  39426  jm2.24  39438  acongeq  39458  jm2.23  39471  jm2.26lem3  39476  wepwsolem  39520  frege102d  39977  fnchoice  41163  refsum2cnlem1  41171  wallispilem3  42229  wtgoldbnnsum4prm  43844  bgoldbnnsum3prm  43846  nn0sumshdiglem1  44609
  Copyright terms: Public domain W3C validator