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

Theorem mpjaodan 823
Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule E ( elimination), see natded 26652. (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 822 . 2 ((𝜑 ∧ (𝜓𝜃)) → 𝜒)
51, 4mpdan 699 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 382  wa 383
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 196  df-or 384  df-an 385
This theorem is referenced by:  mpjao3dan  1387  weniso  6504  isf32lem2  9059  isf32lem4  9061  fpwwe2lem11  9341  fpwwe2lem12  9342  lecasei  10022  ltlecasei  10024  xaddass  11951  xlesubadd  11965  xmulge0  11986  xadddi2  11999  xrsupss  12011  xrinfmss  12012  fzm1  12289  seqf1olem2  12703  expaddzlem  12765  discr  12863  fzomaxdif  13931  iseralt  14263  sumrb  14291  telfsumo  14375  fsumparts  14379  ntrivcvgtail  14471  prodrb  14501  bitsf1  15006  smupvallem  15043  eucalgf  15134  eucalginv  15135  vdwmc2  15521  mreexmrid  16126  mreexexlem3d  16129  mulgnn0p1  17375  mulgnn0subcl  17377  mulgsubcl  17378  mulgneg  17383  mulgz  17391  mulgnn0dir  17394  mulgdirlem  17395  mulgdir  17396  submmulg  17409  ghmmulg  17495  odid  17780  oddvds  17789  dfod2  17804  gexid  17819  gexdvds  17822  mulgnn0di  18054  mulgdi  18055  gsumzsplit  18150  lsppratlem5  18972  prmirred  19662  1stckgenlem  21166  qtoprest  21330  tgpmulg  21707  tsmssplit  21765  xblss2ps  22016  xblss2  22017  metustfbas  22172  nmoix  22343  nmoleub  22345  idnghm  22357  blcvx  22409  icccmp  22436  xrge0tsms  22445  metdstri  22462  nmoleub2lem  22722  rrxcph  22988  rrxdstprj1  23000  ivthle  23032  ivthle2  23033  dyadmbl  23174  volivth  23181  itg2const2  23314  itg2mulc  23320  dvlip2  23562  dvfsumlem1  23593  mdegmullem  23642  coemulhi  23814  dgrcolem2  23834  coseq00topi  24058  abssinper  24074  cxplea  24242  cxple2  24243  cxple2a  24245  cxpcn3  24289  cxpaddlelem  24292  cxpaddle  24293  ang180lem3  24341  dcubic2  24371  birthdaylem2  24479  jensen  24515  ppiltx  24703  chtub  24737  bcmono  24802  bcmax  24803  bpos  24818  lgseisenlem1  24900  2sqlem4  24946  pntrlog2bndlem5  25070  pntpbnd1  25075  tgldimor  25197  tgifscgr  25203  tgcgrxfr  25213  tgbtwnconn1  25270  tgbtwnconn2  25271  tgbtwnconn3  25272  tgbtwnconnln3  25273  tgbtwnconn22  25274  tgbtwnconnln1  25275  tgbtwnconnln2  25276  legtrid  25286  legbtwn  25289  tgcgrsub2  25290  legov3  25293  hlln  25302  hltr  25305  btwnhl  25309  ncolncol  25341  mirconn  25373  krippen  25386  midexlem  25387  midex  25429  opphllem2  25440  opphllem5  25443  opphllem6  25444  outpasch  25447  hlpasch  25448  trgcopyeulem  25497  cgrahl  25518  cgracol  25519  ex-natded5.7  26660  ex-natded5.13  26664  ex-natded9.20  26666  ex-natded9.20-2  26667  xrge0infss  28915  difioo  28934  iundisjcnt  28944  f1ocnt  28946  2sqmod  28979  xrsmulgzz  29009  ressmulgnn0  29015  xrge0addgt0  29022  xrge0adddir  29023  archirngz  29074  archiabllem2a  29079  xrge0tsmsd  29116  submateq  29203  lmat22lem  29211  locfinref  29236  xrge0mulc1cn  29315  qqhval2lem  29353  nexple  29399  esumpcvgval  29467  esumcvg  29475  sigaclcu3  29512  measiuns  29607  voliune  29619  volfiniune  29620  volmeas  29621  sgncl  29927  sgnmul  29931  gsumnunsn  29942  signsply0  29954  signswch  29964  signslema  29965  signstfvneq0  29975  bnj517  30209  bnj1408  30358  bnj1423  30373  bnj1452  30374  dnibndlem13  31650  dnibnd  31651  poimirlem2  32581  fdc  32711  orel  33074  lsatcvat  33355  lkrpssN  33468  2at0mat0  33829  atmod1i1m  34162  lhp2at0nle  34339  trlcone  35034  tendoex  35281  dihlspsnssN  35639  dochkrsm  35765  lcfl8  35809  lclkrlem2b  35815  lclkrlem2s  35832  lcfrlem21  35870  mapdval2N  35937  mapdspex  35975  pell1qrgaplem  36455  monotoddzzfi  36525  oddcomabszz  36527  zindbi  36529  rmxnn  36536  jm2.24  36548  acongeq  36568  jm2.23  36581  jm2.26lem3  36586  wepwsolem  36630  frege102d  37065  fnchoice  38211  refsum2cnlem1  38219  wallispilem3  38960  wtgoldbnnsum4prm  40218  bgoldbnnsum3prm  40220  nn0sumshdiglem1  42213
  Copyright terms: Public domain W3C validator