Theorem mpjaodan 956

Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule ∨ E (∨ elimination), see natded 29924. (Contributed by Mario Carneiro, 29-May-2016.)

Hypotheses

Ref	Expression
jaodan.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)
jaodan.2	⊢ ((𝜑 ∧ 𝜃) → 𝜒)
jaodan.3	⊢ (𝜑 → (𝜓 ∨ 𝜃))

Assertion

Ref	Expression
mpjaodan	⊢ (𝜑 → 𝜒)

Proof of Theorem mpjaodan

Step	Hyp	Ref	Expression
1		jaodan.3	. 2 ⊢ (𝜑 → (𝜓 ∨ 𝜃))
2		jaodan.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3		jaodan.2	. . 3 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)
4	2, 3	jaodan 955	. 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)
5	1, 4	mpdan 684	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∨ 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 206  df-an 396  df-or 845

This theorem is referenced by:  mpjao3danOLD  1431  onunel  6469  weniso  7354  isf32lem2  10353  isf32lem4  10355  fpwwe2lem10  10639  fpwwe2lem11  10640  lecasei  11325  ltlecasei  11327  xaddass  13233  xlesubadd  13247  xmulge0  13268  xadddi2  13281  xrsupss  13293  xrinfmss  13294  fzm1  13586  seqf1olem2  14013  expaddzlem  14076  discr  14208  fzomaxdif  15295  iseralt  15636  sumrb  15664  telfsumo  15753  fsumparts  15757  ntrivcvgtail  15851  prodrb  15881  bitsf1  16392  smupvallem  16429  eucalgf  16525  eucalginv  16526  vdwmc2  16917  fvprif  17512  mreexmrid  17592  mreexexlem3d  17595  mulgfval  18989  mulgnn0p1  19002  mulgnn0subcl  19004  mulgsubcl  19005  mulgneg  19009  mulgz  19019  mulgnn0dir  19021  mulgdirlem  19022  mulgdir  19023  submmulg  19035  ghmmulg  19143  odid  19448  oddvds  19457  dfod2  19474  gexid  19491  gexdvds  19494  mulgnn0di  19735  mulgdi  19736  gsumzsplit  19837  2nsgsimpgd  20014  prmgrpsimpgd  20026  lringuplu  20433  lsppratlem5  20910  prmirred  21246  mhpmulcl  21912  1stckgenlem  23278  qtoprest  23442  tgpmulg  23818  tsmssplit  23877  xblss2ps  24128  xblss2  24129  metustfbas  24287  nmoix  24467  nmoleub  24469  idnghm  24481  blcvx  24535  icccmp  24562  xrge0tsms  24571  metdstri  24588  nmoleub2lem  24862  rrxcph  25141  rrxdstprj1  25158  ivthle  25206  ivthle2  25207  dyadmbl  25350  volivth  25357  itg2const2  25492  itg2mulc  25498  dvlip2  25748  dvfsumlem1  25779  mdegmullem  25832  coemulhi  26004  dgrcolem2  26025  coseq00topi  26249  abssinper  26267  cxplea  26441  cxple2  26442  cxple2a  26444  cxpcn3  26493  cxpaddlelem  26496  cxpaddle  26497  ang180lem3  26553  dcubic2  26586  birthdaylem2  26694  jensen  26730  ppiltx  26918  chtub  26952  bcmono  27017  bcmax  27018  bpos  27033  lgseisenlem1  27115  2sqlem4  27161  2sqmod  27176  pntrlog2bndlem5  27321  pntpbnd1  27326  noinfbnd2lem1  27470  noetasuplem4  27476  noetainflem4  27480  mulsproplem12  27823  mulsproplem13  27824  mulsproplem14  27825  slemuld  27834  mulscan2d  27871  tgldimor  28021  tgifscgr  28027  tgcgrxfr  28037  tgbtwnconn1  28094  tgbtwnconn2  28095  tgbtwnconn3  28096  tgbtwnconnln3  28097  tgbtwnconn22  28098  tgbtwnconnln1  28099  tgbtwnconnln2  28100  legtrid  28110  legbtwn  28113  tgcgrsub2  28114  legov3  28117  hlln  28126  hltr  28129  btwnhl  28133  ncolncol  28165  mirconn  28197  krippen  28210  midexlem  28211  midex  28256  opphllem2  28267  opphllem5  28270  opphllem6  28271  outpasch  28274  hlpasch  28275  trgcopyeulem  28324  cgrahl  28346  cgracol  28347  ex-natded5.7  29932  ex-natded5.13  29936  ex-natded9.20  29938  ex-natded9.20-2  29939  suppovss  32174  xrge0infss  32241  xnn0gt0  32250  nn0xmulclb  32252  difioo  32261  iundisjcnt  32277  f1ocnt  32281  hashxpe  32287  xrsmulgzz  32447  ressmulgnn0  32453  xrge0addgt0  32460  xrge0adddir  32461  xrge0tsmsd  32480  tocyc01  32548  cycpmco2lem4  32559  cycpmco2lem7  32562  cycpmco2  32563  cyc3co2  32570  cycpmrn  32573  archirngz  32606  archiabllem2a  32611  ssmxidllem  32864  lindsun  32999  lbsdiflsp0  33000  submateq  33088  lmat22lem  33096  locfinref  33120  xrge0mulc1cn  33220  qqhval2lem  33260  nexple  33306  esumpcvgval  33375  esumcvg  33383  sigaclcu3  33419  measiuns  33514  voliune  33526  volfiniune  33527  volmeas  33528  sgncl  33836  sgnmul  33840  gsumnunsn  33851  signsply0  33861  signswch  33871  signslema  33872  signstfvneq0  33882  chtvalz  33940  bnj517  34195  bnj1408  34346  bnj1423  34361  bnj1452  34362  dnibndlem13  35670  dnibnd  35671  irrdifflemf  36510  poimirlem2  36794  fdc  36917  orel  37274  lsatcvat  38224  lkrpssN  38337  2at0mat0  38700  atmod1i1m  39033  lhp2at0nle  39210  trlcone  39903  tendoex  40150  dihlspsnssN  40507  dochkrsm  40633  lcfl8  40677  lclkrlem2b  40683  lclkrlem2s  40700  lcfrlem21  40738  mapdval2N  40805  mapdspex  40843  aks4d1p5  41252  sticksstones12a  41280  sticksstones13  41282  fsuppind  41465  flt4lem7  41704  nna4b4nsq  41705  pell1qrgaplem  41914  monotoddzzfi  41984  oddcomabszz  41986  zindbi  41988  rmxnn  41993  jm2.24  42005  acongeq  42025  jm2.23  42038  jm2.26lem3  42043  wepwsolem  42087  oe0rif  42338  onmcl  42384  omabs2  42385  omcl2  42386  onsucunipr  42425  oaun3lem1  42427  fzuntgd  42512  frege102d  42808  fnchoice  44016  refsum2cnlem1  44024  wallispilem3  45082  wtgoldbnnsum4prm  46769  bgoldbnnsum3prm  46771  nn0sumshdiglem1  47395  mofeu  47602  toslat  47695