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 27230. (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  1393  weniso  6589  isf32lem2  9161  isf32lem4  9163  fpwwe2lem11  9447  fpwwe2lem12  9448  lecasei  10128  ltlecasei  10130  xaddass  12064  xlesubadd  12078  xmulge0  12099  xadddi2  12112  xrsupss  12124  xrinfmss  12125  fzm1  12404  seqf1olem2  12824  expaddzlem  12886  discr  12984  fzomaxdif  14064  iseralt  14396  sumrb  14425  telfsumo  14515  fsumparts  14519  ntrivcvgtail  14613  prodrb  14643  bitsf1  15149  smupvallem  15186  eucalgf  15277  eucalginv  15278  vdwmc2  15664  mreexmrid  16284  mreexexlem3d  16287  mulgnn0p1  17533  mulgnn0subcl  17535  mulgsubcl  17536  mulgneg  17541  mulgz  17549  mulgnn0dir  17552  mulgdirlem  17553  mulgdir  17554  submmulg  17567  ghmmulg  17653  odid  17938  oddvds  17947  dfod2  17962  gexid  17977  gexdvds  17980  mulgnn0di  18212  mulgdi  18213  gsumzsplit  18308  lsppratlem5  19132  prmirred  19824  1stckgenlem  21337  qtoprest  21501  tgpmulg  21878  tsmssplit  21936  xblss2ps  22187  xblss2  22188  metustfbas  22343  nmoix  22514  nmoleub  22516  idnghm  22528  blcvx  22582  icccmp  22609  xrge0tsms  22618  metdstri  22635  nmoleub2lem  22895  rrxcph  23161  rrxdstprj1  23173  ivthle  23206  ivthle2  23207  dyadmbl  23349  volivth  23356  itg2const2  23489  itg2mulc  23495  dvlip2  23739  dvfsumlem1  23770  mdegmullem  23819  coemulhi  23991  dgrcolem2  24011  coseq00topi  24235  abssinper  24251  cxplea  24423  cxple2  24424  cxple2a  24426  cxpcn3  24470  cxpaddlelem  24473  cxpaddle  24474  ang180lem3  24522  dcubic2  24552  birthdaylem2  24660  jensen  24696  ppiltx  24884  chtub  24918  bcmono  24983  bcmax  24984  bpos  24999  lgseisenlem1  25081  2sqlem4  25127  pntrlog2bndlem5  25251  pntpbnd1  25256  tgldimor  25378  tgifscgr  25384  tgcgrxfr  25394  tgbtwnconn1  25451  tgbtwnconn2  25452  tgbtwnconn3  25453  tgbtwnconnln3  25454  tgbtwnconn22  25455  tgbtwnconnln1  25456  tgbtwnconnln2  25457  legtrid  25467  legbtwn  25470  tgcgrsub2  25471  legov3  25474  hlln  25483  hltr  25486  btwnhl  25490  ncolncol  25522  mirconn  25554  krippen  25567  midexlem  25568  midex  25610  opphllem2  25621  opphllem5  25624  opphllem6  25625  outpasch  25628  hlpasch  25629  trgcopyeulem  25678  cgrahl  25699  cgracol  25700  ex-natded5.7  27238  ex-natded5.13  27242  ex-natded9.20  27244  ex-natded9.20-2  27245  xrge0infss  29499  difioo  29518  iundisjcnt  29531  f1ocnt  29533  2sqmod  29622  xrsmulgzz  29652  ressmulgnn0  29658  xrge0addgt0  29665  xrge0adddir  29666  archirngz  29717  archiabllem2a  29722  xrge0tsmsd  29759  submateq  29849  lmat22lem  29857  locfinref  29882  xrge0mulc1cn  29961  qqhval2lem  29999  nexple  30045  esumpcvgval  30114  esumcvg  30122  sigaclcu3  30159  measiuns  30254  voliune  30266  volfiniune  30267  volmeas  30268  sgncl  30574  sgnmul  30578  gsumnunsn  30589  signsply0  30602  signswch  30612  signslema  30613  signstfvneq0  30623  chtvalz  30681  bnj517  30929  bnj1408  31078  bnj1423  31093  bnj1452  31094  noetalem3  31839  dnibndlem13  32455  dnibnd  32456  poimirlem2  33382  fdc  33512  orel  33875  lsatcvat  34156  lkrpssN  34269  2at0mat0  34630  atmod1i1m  34963  lhp2at0nle  35140  trlcone  35835  tendoex  36082  dihlspsnssN  36440  dochkrsm  36566  lcfl8  36610  lclkrlem2b  36616  lclkrlem2s  36633  lcfrlem21  36671  mapdval2N  36738  mapdspex  36776  pell1qrgaplem  37256  monotoddzzfi  37326  oddcomabszz  37328  zindbi  37330  rmxnn  37337  jm2.24  37349  acongeq  37369  jm2.23  37382  jm2.26lem3  37387  wepwsolem  37431  frege102d  37865  fnchoice  39008  refsum2cnlem1  39016  wallispilem3  40047  wtgoldbnnsum4prm  41455  bgoldbnnsum3prm  41457  nn0sumshdiglem1  42180
  Copyright terms: Public domain W3C validator