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

Theorem mpjaodan 826
Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule E ( elimination), see natded 27148. (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 825 . 2 ((𝜑 ∧ (𝜓𝜃)) → 𝜒)
51, 4mpdan 701 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 383  wa 384
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 197  df-or 385  df-an 386
This theorem is referenced by:  mpjao3dan  1392  weniso  6569  isf32lem2  9136  isf32lem4  9138  fpwwe2lem11  9422  fpwwe2lem12  9423  lecasei  10103  ltlecasei  10105  xaddass  12038  xlesubadd  12052  xmulge0  12073  xadddi2  12086  xrsupss  12098  xrinfmss  12099  fzm1  12377  seqf1olem2  12797  expaddzlem  12859  discr  12957  fzomaxdif  14033  iseralt  14365  sumrb  14393  telfsumo  14480  fsumparts  14484  ntrivcvgtail  14576  prodrb  14606  bitsf1  15111  smupvallem  15148  eucalgf  15239  eucalginv  15240  vdwmc2  15626  mreexmrid  16243  mreexexlem3d  16246  mulgnn0p1  17492  mulgnn0subcl  17494  mulgsubcl  17495  mulgneg  17500  mulgz  17508  mulgnn0dir  17511  mulgdirlem  17512  mulgdir  17513  submmulg  17526  ghmmulg  17612  odid  17897  oddvds  17906  dfod2  17921  gexid  17936  gexdvds  17939  mulgnn0di  18171  mulgdi  18172  gsumzsplit  18267  lsppratlem5  19091  prmirred  19783  1stckgenlem  21296  qtoprest  21460  tgpmulg  21837  tsmssplit  21895  xblss2ps  22146  xblss2  22147  metustfbas  22302  nmoix  22473  nmoleub  22475  idnghm  22487  blcvx  22541  icccmp  22568  xrge0tsms  22577  metdstri  22594  nmoleub2lem  22854  rrxcph  23120  rrxdstprj1  23132  ivthle  23165  ivthle2  23166  dyadmbl  23308  volivth  23315  itg2const2  23448  itg2mulc  23454  dvlip2  23696  dvfsumlem1  23727  mdegmullem  23776  coemulhi  23948  dgrcolem2  23968  coseq00topi  24192  abssinper  24208  cxplea  24376  cxple2  24377  cxple2a  24379  cxpcn3  24423  cxpaddlelem  24426  cxpaddle  24427  ang180lem3  24475  dcubic2  24505  birthdaylem2  24613  jensen  24649  ppiltx  24837  chtub  24871  bcmono  24936  bcmax  24937  bpos  24952  lgseisenlem1  25034  2sqlem4  25080  pntrlog2bndlem5  25204  pntpbnd1  25209  tgldimor  25331  tgifscgr  25337  tgcgrxfr  25347  tgbtwnconn1  25404  tgbtwnconn2  25405  tgbtwnconn3  25406  tgbtwnconnln3  25407  tgbtwnconn22  25408  tgbtwnconnln1  25409  tgbtwnconnln2  25410  legtrid  25420  legbtwn  25423  tgcgrsub2  25424  legov3  25427  hlln  25436  hltr  25439  btwnhl  25443  ncolncol  25475  mirconn  25507  krippen  25520  midexlem  25521  midex  25563  opphllem2  25574  opphllem5  25577  opphllem6  25578  outpasch  25581  hlpasch  25582  trgcopyeulem  25631  cgrahl  25652  cgracol  25653  ex-natded5.7  27156  ex-natded5.13  27160  ex-natded9.20  27162  ex-natded9.20-2  27163  xrge0infss  29410  difioo  29429  iundisjcnt  29440  f1ocnt  29442  2sqmod  29475  xrsmulgzz  29505  ressmulgnn0  29511  xrge0addgt0  29518  xrge0adddir  29519  archirngz  29570  archiabllem2a  29575  xrge0tsmsd  29612  submateq  29699  lmat22lem  29707  locfinref  29732  xrge0mulc1cn  29811  qqhval2lem  29849  nexple  29895  esumpcvgval  29963  esumcvg  29971  sigaclcu3  30008  measiuns  30103  voliune  30115  volfiniune  30116  volmeas  30117  sgncl  30423  sgnmul  30427  gsumnunsn  30438  signsply0  30450  signswch  30460  signslema  30461  signstfvneq0  30471  bnj517  30716  bnj1408  30865  bnj1423  30880  bnj1452  30881  dnibndlem13  32175  dnibnd  32176  poimirlem2  33082  fdc  33212  orel  33575  lsatcvat  33856  lkrpssN  33969  2at0mat0  34330  atmod1i1m  34663  lhp2at0nle  34840  trlcone  35535  tendoex  35782  dihlspsnssN  36140  dochkrsm  36266  lcfl8  36310  lclkrlem2b  36316  lclkrlem2s  36333  lcfrlem21  36371  mapdval2N  36438  mapdspex  36476  pell1qrgaplem  36956  monotoddzzfi  37026  oddcomabszz  37028  zindbi  37030  rmxnn  37037  jm2.24  37049  acongeq  37069  jm2.23  37082  jm2.26lem3  37087  wepwsolem  37131  frege102d  37566  fnchoice  38710  refsum2cnlem1  38718  wallispilem3  39621  wtgoldbnnsum4prm  41009  bgoldbnnsum3prm  41011  nn0sumshdiglem1  41737
  Copyright terms: Public domain W3C validator