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

Theorem mpjaodan 822
Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule E ( elimination), see natded 26418. (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 821 . 2 ((𝜑 ∧ (𝜓𝜃)) → 𝜒)
51, 4mpdan 698 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 381  wa 382
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 195  df-or 383  df-an 384
This theorem is referenced by:  mpjao3dan  1386  weniso  6482  isf32lem2  9036  isf32lem4  9038  fpwwe2lem11  9318  fpwwe2lem12  9319  lecasei  9994  ltlecasei  9996  xaddass  11908  xlesubadd  11922  xmulge0  11943  xadddi2  11956  xrsupss  11967  xrinfmss  11968  fzm1  12244  seqf1olem2  12658  expaddzlem  12720  discr  12818  fzomaxdif  13877  iseralt  14209  sumrb  14237  telfsumo  14321  fsumparts  14325  ntrivcvgtail  14417  prodrb  14447  bitsf1  14952  smupvallem  14989  eucalgf  15080  eucalginv  15081  vdwmc2  15467  mreexmrid  16072  mreexexlem3d  16075  mulgnn0p1  17321  mulgnn0subcl  17323  mulgsubcl  17324  mulgneg  17329  mulgz  17337  mulgnn0dir  17340  mulgdirlem  17341  mulgdir  17342  submmulg  17355  ghmmulg  17441  odid  17726  oddvds  17735  dfod2  17750  gexid  17765  gexdvds  17768  mulgnn0di  18000  mulgdi  18001  gsumzsplit  18096  lsppratlem5  18918  prmirred  19607  1stckgenlem  21108  qtoprest  21272  tgpmulg  21649  tsmssplit  21707  xblss2ps  21957  xblss2  21958  metustfbas  22113  nmoix  22275  nmoleub  22277  idnghm  22289  blcvx  22341  icccmp  22368  xrge0tsms  22377  metdstri  22393  nmoleub2lem  22653  rrxcph  22905  rrxdstprj1  22917  ivthle  22949  ivthle2  22950  dyadmbl  23091  volivth  23098  itg2const2  23231  itg2mulc  23237  dvlip2  23479  dvfsumlem1  23510  mdegmullem  23559  coemulhi  23731  dgrcolem2  23751  coseq00topi  23975  abssinper  23991  cxplea  24159  cxple2  24160  cxple2a  24162  cxpcn3  24206  cxpaddlelem  24209  cxpaddle  24210  ang180lem3  24258  dcubic2  24288  birthdaylem2  24396  jensen  24432  ppiltx  24620  chtub  24654  bcmono  24719  bcmax  24720  bpos  24735  lgseisenlem1  24817  2sqlem4  24863  pntrlog2bndlem5  24987  pntpbnd1  24992  tgldimor  25114  tgifscgr  25121  tgcgrxfr  25131  tgbtwnconn1  25188  tgbtwnconn2  25189  tgbtwnconn3  25190  tgbtwnconnln3  25191  tgbtwnconn22  25192  tgbtwnconnln1  25193  tgbtwnconnln2  25194  legtrid  25204  legbtwn  25207  tgcgrsub2  25208  legov3  25211  hlln  25220  hltr  25223  btwnhl  25227  ncolncol  25259  mirconn  25291  krippen  25304  midexlem  25305  midex  25347  opphllem2  25358  opphllem5  25361  opphllem6  25362  outpasch  25365  hlpasch  25366  trgcopyeulem  25415  cgrahl  25436  cgracol  25437  ex-natded5.7  26426  ex-natded5.13  26430  ex-natded9.20  26432  ex-natded9.20-2  26433  xrge0infss  28721  difioo  28740  iundisjcnt  28750  f1ocnt  28752  2sqmod  28785  xrsmulgzz  28815  ressmulgnn0  28821  xrge0addgt0  28828  xrge0adddir  28829  archirngz  28880  archiabllem2a  28885  xrge0tsmsd  28922  submateq  29009  lmat22lem  29017  locfinref  29042  xrge0mulc1cn  29121  qqhval2lem  29159  nexple  29205  esumpcvgval  29273  esumcvg  29281  sigaclcu3  29318  measiuns  29413  voliune  29425  volfiniune  29426  volmeas  29427  sgncl  29733  sgnmul  29737  gsumnunsn  29748  signsply0  29760  signswch  29770  signslema  29771  signstfvneq0  29781  bnj517  30015  bnj1408  30164  bnj1423  30179  bnj1452  30180  dnibndlem13  31456  dnibnd  31457  poimirlem2  32384  fdc  32514  orel  32877  lsatcvat  33158  lkrpssN  33271  2at0mat0  33632  atmod1i1m  33965  lhp2at0nle  34142  trlcone  34837  tendoex  35084  dihlspsnssN  35442  dochkrsm  35568  lcfl8  35612  lclkrlem2b  35618  lclkrlem2s  35635  lcfrlem21  35673  mapdval2N  35740  mapdspex  35778  pell1qrgaplem  36258  monotoddzzfi  36328  oddcomabszz  36330  zindbi  36332  rmxnn  36339  jm2.24  36351  acongeq  36371  jm2.23  36384  jm2.26lem3  36389  wepwsolem  36433  frege102d  36868  fnchoice  38014  refsum2cnlem1  38022  wallispilem3  38764  wtgoldbnnsum4prm  40023  bgoldbnnsum3prm  40025  nn0sumshdiglem1  42215
  Copyright terms: Public domain W3C validator