Theorem mpjaodan 957

Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule ∨ E (∨ elimination), see natded 29694. (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 956	. 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)
5	1, 4	mpdan 685	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 396   ∨ wo 845

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 397  df-or 846

This theorem is referenced by:  mpjao3danOLD  1432  onunel  6469  weniso  7353  isf32lem2  10351  isf32lem4  10353  fpwwe2lem10  10637  fpwwe2lem11  10638  lecasei  11322  ltlecasei  11324  xaddass  13230  xlesubadd  13244  xmulge0  13265  xadddi2  13278  xrsupss  13290  xrinfmss  13291  fzm1  13583  seqf1olem2  14010  expaddzlem  14073  discr  14205  fzomaxdif  15292  iseralt  15633  sumrb  15661  telfsumo  15750  fsumparts  15754  ntrivcvgtail  15848  prodrb  15878  bitsf1  16389  smupvallem  16426  eucalgf  16522  eucalginv  16523  vdwmc2  16914  fvprif  17509  mreexmrid  17589  mreexexlem3d  17592  mulgfval  18954  mulgnn0p1  18967  mulgnn0subcl  18969  mulgsubcl  18970  mulgneg  18974  mulgz  18984  mulgnn0dir  18986  mulgdirlem  18987  mulgdir  18988  submmulg  19000  ghmmulg  19106  odid  19408  oddvds  19417  dfod2  19434  gexid  19451  gexdvds  19454  mulgnn0di  19695  mulgdi  19696  gsumzsplit  19797  2nsgsimpgd  19974  prmgrpsimpgd  19986  lringuplu  20318  lsppratlem5  20770  prmirred  21050  mhpmulcl  21698  1stckgenlem  23064  qtoprest  23228  tgpmulg  23604  tsmssplit  23663  xblss2ps  23914  xblss2  23915  metustfbas  24073  nmoix  24253  nmoleub  24255  idnghm  24267  blcvx  24321  icccmp  24348  xrge0tsms  24357  metdstri  24374  nmoleub2lem  24637  rrxcph  24916  rrxdstprj1  24933  ivthle  24980  ivthle2  24981  dyadmbl  25124  volivth  25131  itg2const2  25266  itg2mulc  25272  dvlip2  25519  dvfsumlem1  25550  mdegmullem  25603  coemulhi  25775  dgrcolem2  25795  coseq00topi  26019  abssinper  26037  cxplea  26211  cxple2  26212  cxple2a  26214  cxpcn3  26263  cxpaddlelem  26266  cxpaddle  26267  ang180lem3  26323  dcubic2  26356  birthdaylem2  26464  jensen  26500  ppiltx  26688  chtub  26722  bcmono  26787  bcmax  26788  bpos  26803  lgseisenlem1  26885  2sqlem4  26931  2sqmod  26946  pntrlog2bndlem5  27091  pntpbnd1  27096  noinfbnd2lem1  27240  noetasuplem4  27246  noetainflem4  27250  mulsproplem12  27593  mulsproplem13  27594  mulsproplem14  27595  slemuld  27604  mulscan2d  27641  tgldimor  27791  tgifscgr  27797  tgcgrxfr  27807  tgbtwnconn1  27864  tgbtwnconn2  27865  tgbtwnconn3  27866  tgbtwnconnln3  27867  tgbtwnconn22  27868  tgbtwnconnln1  27869  tgbtwnconnln2  27870  legtrid  27880  legbtwn  27883  tgcgrsub2  27884  legov3  27887  hlln  27896  hltr  27899  btwnhl  27903  ncolncol  27935  mirconn  27967  krippen  27980  midexlem  27981  midex  28026  opphllem2  28037  opphllem5  28040  opphllem6  28041  outpasch  28044  hlpasch  28045  trgcopyeulem  28094  cgrahl  28116  cgracol  28117  ex-natded5.7  29702  ex-natded5.13  29706  ex-natded9.20  29708  ex-natded9.20-2  29709  suppovss  31944  xrge0infss  32011  xnn0gt0  32020  nn0xmulclb  32022  difioo  32031  iundisjcnt  32047  f1ocnt  32051  hashxpe  32057  xrsmulgzz  32217  ressmulgnn0  32223  xrge0addgt0  32230  xrge0adddir  32231  xrge0tsmsd  32250  tocyc01  32318  cycpmco2lem4  32329  cycpmco2lem7  32332  cycpmco2  32333  cyc3co2  32340  cycpmrn  32343  archirngz  32376  archiabllem2a  32381  ssmxidllem  32634  lindsun  32769  lbsdiflsp0  32770  submateq  32858  lmat22lem  32866  locfinref  32890  xrge0mulc1cn  32990  qqhval2lem  33030  nexple  33076  esumpcvgval  33145  esumcvg  33153  sigaclcu3  33189  measiuns  33284  voliune  33296  volfiniune  33297  volmeas  33298  sgncl  33606  sgnmul  33610  gsumnunsn  33621  signsply0  33631  signswch  33641  signslema  33642  signstfvneq0  33652  chtvalz  33710  bnj517  33965  bnj1408  34116  bnj1423  34131  bnj1452  34132  dnibndlem13  35452  dnibnd  35453  irrdifflemf  36292  poimirlem2  36576  fdc  36699  orel  37056  lsatcvat  38006  lkrpssN  38119  2at0mat0  38482  atmod1i1m  38815  lhp2at0nle  38992  trlcone  39685  tendoex  39932  dihlspsnssN  40289  dochkrsm  40415  lcfl8  40459  lclkrlem2b  40465  lclkrlem2s  40482  lcfrlem21  40520  mapdval2N  40587  mapdspex  40625  aks4d1p5  41031  sticksstones12a  41059  sticksstones13  41061  fsuppind  41244  flt4lem7  41483  nna4b4nsq  41484  pell1qrgaplem  41693  monotoddzzfi  41763  oddcomabszz  41765  zindbi  41767  rmxnn  41772  jm2.24  41784  acongeq  41804  jm2.23  41817  jm2.26lem3  41822  wepwsolem  41866  oe0rif  42117  onmcl  42163  omabs2  42164  omcl2  42165  onsucunipr  42204  oaun3lem1  42206  fzuntgd  42291  frege102d  42587  fnchoice  43795  refsum2cnlem1  43803  wallispilem3  44862  wtgoldbnnsum4prm  46549  bgoldbnnsum3prm  46551  nn0sumshdiglem1  47385  mofeu  47592  toslat  47685