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

Theorem mpjaodan 958
Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule E ( elimination), see natded 29350. (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 957 . 2 ((𝜑 ∧ (𝜓𝜃)) → 𝜒)
51, 4mpdan 686 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wo 846
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 206  df-an 398  df-or 847
This theorem is referenced by:  mpjao3danOLD  1433  onunel  6423  weniso  7300  isf32lem2  10291  isf32lem4  10293  fpwwe2lem10  10577  fpwwe2lem11  10578  lecasei  11262  ltlecasei  11264  xaddass  13169  xlesubadd  13183  xmulge0  13204  xadddi2  13217  xrsupss  13229  xrinfmss  13230  fzm1  13522  seqf1olem2  13949  expaddzlem  14012  discr  14144  fzomaxdif  15229  iseralt  15570  sumrb  15599  telfsumo  15688  fsumparts  15692  ntrivcvgtail  15786  prodrb  15816  bitsf1  16327  smupvallem  16364  eucalgf  16460  eucalginv  16461  vdwmc2  16852  fvprif  17444  mreexmrid  17524  mreexexlem3d  17527  mulgfval  18875  mulgnn0p1  18888  mulgnn0subcl  18890  mulgsubcl  18891  mulgneg  18895  mulgz  18905  mulgnn0dir  18907  mulgdirlem  18908  mulgdir  18909  submmulg  18921  ghmmulg  19021  odid  19321  oddvds  19330  dfod2  19347  gexid  19364  gexdvds  19367  mulgnn0di  19605  mulgdi  19606  gsumzsplit  19705  2nsgsimpgd  19882  prmgrpsimpgd  19894  lsppratlem5  20615  prmirred  20898  mhpmulcl  21542  1stckgenlem  22907  qtoprest  23071  tgpmulg  23447  tsmssplit  23506  xblss2ps  23757  xblss2  23758  metustfbas  23916  nmoix  24096  nmoleub  24098  idnghm  24110  blcvx  24164  icccmp  24191  xrge0tsms  24200  metdstri  24217  nmoleub2lem  24480  rrxcph  24759  rrxdstprj1  24776  ivthle  24823  ivthle2  24824  dyadmbl  24967  volivth  24974  itg2const2  25109  itg2mulc  25115  dvlip2  25362  dvfsumlem1  25393  mdegmullem  25446  coemulhi  25618  dgrcolem2  25638  coseq00topi  25862  abssinper  25880  cxplea  26054  cxple2  26055  cxple2a  26057  cxpcn3  26104  cxpaddlelem  26107  cxpaddle  26108  ang180lem3  26164  dcubic2  26197  birthdaylem2  26305  jensen  26341  ppiltx  26529  chtub  26563  bcmono  26628  bcmax  26629  bpos  26644  lgseisenlem1  26726  2sqlem4  26772  2sqmod  26787  pntrlog2bndlem5  26932  pntpbnd1  26937  noinfbnd2lem1  27081  noetasuplem4  27087  noetainflem4  27091  tgldimor  27447  tgifscgr  27453  tgcgrxfr  27463  tgbtwnconn1  27520  tgbtwnconn2  27521  tgbtwnconn3  27522  tgbtwnconnln3  27523  tgbtwnconn22  27524  tgbtwnconnln1  27525  tgbtwnconnln2  27526  legtrid  27536  legbtwn  27539  tgcgrsub2  27540  legov3  27543  hlln  27552  hltr  27555  btwnhl  27559  ncolncol  27591  mirconn  27623  krippen  27636  midexlem  27637  midex  27682  opphllem2  27693  opphllem5  27696  opphllem6  27697  outpasch  27700  hlpasch  27701  trgcopyeulem  27750  cgrahl  27772  cgracol  27773  ex-natded5.7  29358  ex-natded5.13  29362  ex-natded9.20  29364  ex-natded9.20-2  29365  suppovss  31601  xrge0infss  31668  xnn0gt0  31677  nn0xmulclb  31679  difioo  31688  iundisjcnt  31704  f1ocnt  31708  hashxpe  31712  xrsmulgzz  31872  ressmulgnn0  31878  xrge0addgt0  31885  xrge0adddir  31886  xrge0tsmsd  31902  tocyc01  31970  cycpmco2lem4  31981  cycpmco2lem7  31984  cycpmco2  31985  cyc3co2  31992  cycpmrn  31995  archirngz  32028  archiabllem2a  32033  ssmxidllem  32241  lindsun  32323  lbsdiflsp0  32324  submateq  32393  lmat22lem  32401  locfinref  32425  xrge0mulc1cn  32525  qqhval2lem  32565  nexple  32611  esumpcvgval  32680  esumcvg  32688  sigaclcu3  32724  measiuns  32819  voliune  32831  volfiniune  32832  volmeas  32833  sgncl  33141  sgnmul  33145  gsumnunsn  33156  signsply0  33166  signswch  33176  signslema  33177  signstfvneq0  33187  chtvalz  33245  bnj517  33500  bnj1408  33651  bnj1423  33666  bnj1452  33667  dnibndlem13  34956  dnibnd  34957  irrdifflemf  35799  poimirlem2  36083  fdc  36207  orel  36564  lsatcvat  37515  lkrpssN  37628  2at0mat0  37991  atmod1i1m  38324  lhp2at0nle  38501  trlcone  39194  tendoex  39441  dihlspsnssN  39798  dochkrsm  39924  lcfl8  39968  lclkrlem2b  39974  lclkrlem2s  39991  lcfrlem21  40029  mapdval2N  40096  mapdspex  40134  aks4d1p5  40540  sticksstones12a  40568  sticksstones13  40570  fsuppind  40768  flt4lem7  41000  nna4b4nsq  41001  pell1qrgaplem  41199  monotoddzzfi  41269  oddcomabszz  41271  zindbi  41273  rmxnn  41278  jm2.24  41290  acongeq  41310  jm2.23  41323  jm2.26lem3  41328  wepwsolem  41372  oe0rif  41623  omabs2  41668  omcl2  41669  fzuntgd  41737  frege102d  42033  fnchoice  43241  refsum2cnlem1  43249  wallispilem3  44315  wtgoldbnnsum4prm  46001  bgoldbnnsum3prm  46003  nn0sumshdiglem1  46714  mofeu  46921  toslat  47014
  Copyright terms: Public domain W3C validator