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

Theorem mpjaodan 956
Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule E ( elimination), see natded 28179. (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 955 . 2 ((𝜑 ∧ (𝜓𝜃)) → 𝜒)
51, 4mpdan 686 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wo 844
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 210  df-an 400  df-or 845
This theorem is referenced by:  mpjao3danOLD  1429  weniso  7091  isf32lem2  9763  isf32lem4  9765  fpwwe2lem11  10049  fpwwe2lem12  10050  lecasei  10733  ltlecasei  10735  xaddass  12630  xlesubadd  12644  xmulge0  12665  xadddi2  12678  xrsupss  12690  xrinfmss  12691  fzm1  12982  seqf1olem2  13406  expaddzlem  13468  discr  13597  fzomaxdif  14694  iseralt  15032  sumrb  15061  telfsumo  15148  fsumparts  15152  ntrivcvgtail  15247  prodrb  15277  bitsf1  15784  smupvallem  15821  eucalgf  15916  eucalginv  15917  vdwmc2  16304  fvprif  16825  mreexmrid  16905  mreexexlem3d  16908  mulgfval  18217  mulgnn0p1  18230  mulgnn0subcl  18232  mulgsubcl  18233  mulgneg  18237  mulgz  18246  mulgnn0dir  18248  mulgdirlem  18249  mulgdir  18250  submmulg  18262  ghmmulg  18361  odid  18657  oddvds  18666  dfod2  18682  gexid  18697  gexdvds  18700  mulgnn0di  18937  mulgdi  18938  gsumzsplit  19038  2nsgsimpgd  19215  prmgrpsimpgd  19227  lsppratlem5  19911  prmirred  20630  1stckgenlem  22149  qtoprest  22313  tgpmulg  22689  tsmssplit  22748  xblss2ps  22999  xblss2  23000  metustfbas  23155  nmoix  23326  nmoleub  23328  idnghm  23340  blcvx  23394  icccmp  23421  xrge0tsms  23430  metdstri  23447  nmoleub2lem  23710  rrxcph  23987  rrxdstprj1  24004  ivthle  24051  ivthle2  24052  dyadmbl  24195  volivth  24202  itg2const2  24336  itg2mulc  24342  dvlip2  24589  dvfsumlem1  24620  mdegmullem  24670  coemulhi  24842  dgrcolem2  24862  coseq00topi  25086  abssinper  25104  cxplea  25278  cxple2  25279  cxple2a  25281  cxpcn3  25328  cxpaddlelem  25331  cxpaddle  25332  ang180lem3  25388  dcubic2  25421  birthdaylem2  25529  jensen  25565  ppiltx  25753  chtub  25787  bcmono  25852  bcmax  25853  bpos  25868  lgseisenlem1  25950  2sqlem4  25996  2sqmod  26011  pntrlog2bndlem5  26156  pntpbnd1  26161  tgldimor  26287  tgifscgr  26293  tgcgrxfr  26303  tgbtwnconn1  26360  tgbtwnconn2  26361  tgbtwnconn3  26362  tgbtwnconnln3  26363  tgbtwnconn22  26364  tgbtwnconnln1  26365  tgbtwnconnln2  26366  legtrid  26376  legbtwn  26379  tgcgrsub2  26380  legov3  26383  hlln  26392  hltr  26395  btwnhl  26399  ncolncol  26431  mirconn  26463  krippen  26476  midexlem  26477  midex  26522  opphllem2  26533  opphllem5  26536  opphllem6  26537  outpasch  26540  hlpasch  26541  trgcopyeulem  26590  cgrahl  26612  cgracol  26613  ex-natded5.7  28187  ex-natded5.13  28191  ex-natded9.20  28193  ex-natded9.20-2  28194  suppovss  30425  xrge0infss  30483  xnn0gt0  30493  nn0xmulclb  30495  difioo  30504  iundisjcnt  30520  f1ocnt  30524  hashxpe  30528  xrsmulgzz  30685  ressmulgnn0  30691  xrge0addgt0  30698  xrge0adddir  30699  xrge0tsmsd  30712  tocyc01  30780  cycpmco2lem4  30791  cycpmco2lem7  30794  cycpmco2  30795  cyc3co2  30802  cycpmrn  30805  archirngz  30838  archiabllem2a  30843  ssmxidllem  31001  lindsun  31044  lbsdiflsp0  31045  submateq  31097  lmat22lem  31105  locfinref  31128  xrge0mulc1cn  31204  qqhval2lem  31242  nexple  31288  esumpcvgval  31357  esumcvg  31365  sigaclcu3  31401  measiuns  31496  voliune  31508  volfiniune  31509  volmeas  31510  sgncl  31816  sgnmul  31820  gsumnunsn  31831  signsply0  31841  signswch  31851  signslema  31852  signstfvneq0  31862  chtvalz  31920  bnj517  32177  bnj1408  32328  bnj1423  32343  bnj1452  32344  noetalem3  33239  dnibndlem13  33849  dnibnd  33850  irrdifflemf  34647  poimirlem2  34964  fdc  35088  orel  35445  lsatcvat  36251  lkrpssN  36364  2at0mat0  36726  atmod1i1m  37059  lhp2at0nle  37236  trlcone  37929  tendoex  38176  dihlspsnssN  38533  dochkrsm  38659  lcfl8  38703  lclkrlem2b  38709  lclkrlem2s  38726  lcfrlem21  38764  mapdval2N  38831  mapdspex  38869  pell1qrgaplem  39661  monotoddzzfi  39730  oddcomabszz  39732  zindbi  39734  rmxnn  39739  jm2.24  39751  acongeq  39771  jm2.23  39784  jm2.26lem3  39789  wepwsolem  39833  frege102d  40302  fnchoice  41509  refsum2cnlem1  41517  wallispilem3  42566  wtgoldbnnsum4prm  44177  bgoldbnnsum3prm  44179  nn0sumshdiglem1  44891
  Copyright terms: Public domain W3C validator