Theorem mpjaodan 956

Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule ∨ E (∨ elimination), see natded 28776. (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 396   ∨ 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 397  df-or 845

This theorem is referenced by:  mpjao3danOLD  1431  weniso  7234  isf32lem2  10119  isf32lem4  10121  fpwwe2lem10  10405  fpwwe2lem11  10406  lecasei  11090  ltlecasei  11092  xaddass  12992  xlesubadd  13006  xmulge0  13027  xadddi2  13040  xrsupss  13052  xrinfmss  13053  fzm1  13345  seqf1olem2  13772  expaddzlem  13835  discr  13964  fzomaxdif  15064  iseralt  15405  sumrb  15434  telfsumo  15523  fsumparts  15527  ntrivcvgtail  15621  prodrb  15651  bitsf1  16162  smupvallem  16199  eucalgf  16297  eucalginv  16298  vdwmc2  16689  fvprif  17281  mreexmrid  17361  mreexexlem3d  17364  mulgfval  18711  mulgnn0p1  18724  mulgnn0subcl  18726  mulgsubcl  18727  mulgneg  18731  mulgz  18740  mulgnn0dir  18742  mulgdirlem  18743  mulgdir  18744  submmulg  18756  ghmmulg  18855  odid  19155  oddvds  19164  dfod2  19180  gexid  19195  gexdvds  19198  mulgnn0di  19436  mulgdi  19437  gsumzsplit  19537  2nsgsimpgd  19714  prmgrpsimpgd  19726  lsppratlem5  20422  prmirred  20705  mhpmulcl  21348  1stckgenlem  22713  qtoprest  22877  tgpmulg  23253  tsmssplit  23312  xblss2ps  23563  xblss2  23564  metustfbas  23722  nmoix  23902  nmoleub  23904  idnghm  23916  blcvx  23970  icccmp  23997  xrge0tsms  24006  metdstri  24023  nmoleub2lem  24286  rrxcph  24565  rrxdstprj1  24582  ivthle  24629  ivthle2  24630  dyadmbl  24773  volivth  24780  itg2const2  24915  itg2mulc  24921  dvlip2  25168  dvfsumlem1  25199  mdegmullem  25252  coemulhi  25424  dgrcolem2  25444  coseq00topi  25668  abssinper  25686  cxplea  25860  cxple2  25861  cxple2a  25863  cxpcn3  25910  cxpaddlelem  25913  cxpaddle  25914  ang180lem3  25970  dcubic2  26003  birthdaylem2  26111  jensen  26147  ppiltx  26335  chtub  26369  bcmono  26434  bcmax  26435  bpos  26450  lgseisenlem1  26532  2sqlem4  26578  2sqmod  26593  pntrlog2bndlem5  26738  pntpbnd1  26743  tgldimor  26872  tgifscgr  26878  tgcgrxfr  26888  tgbtwnconn1  26945  tgbtwnconn2  26946  tgbtwnconn3  26947  tgbtwnconnln3  26948  tgbtwnconn22  26949  tgbtwnconnln1  26950  tgbtwnconnln2  26951  legtrid  26961  legbtwn  26964  tgcgrsub2  26965  legov3  26968  hlln  26977  hltr  26980  btwnhl  26984  ncolncol  27016  mirconn  27048  krippen  27061  midexlem  27062  midex  27107  opphllem2  27118  opphllem5  27121  opphllem6  27122  outpasch  27125  hlpasch  27126  trgcopyeulem  27175  cgrahl  27197  cgracol  27198  ex-natded5.7  28784  ex-natded5.13  28788  ex-natded9.20  28790  ex-natded9.20-2  28791  suppovss  31026  xrge0infss  31092  xnn0gt0  31101  nn0xmulclb  31103  difioo  31112  iundisjcnt  31128  f1ocnt  31132  hashxpe  31136  xrsmulgzz  31296  ressmulgnn0  31302  xrge0addgt0  31309  xrge0adddir  31310  xrge0tsmsd  31326  tocyc01  31394  cycpmco2lem4  31405  cycpmco2lem7  31408  cycpmco2  31409  cyc3co2  31416  cycpmrn  31419  archirngz  31452  archiabllem2a  31457  ssmxidllem  31650  lindsun  31715  lbsdiflsp0  31716  submateq  31768  lmat22lem  31776  locfinref  31800  xrge0mulc1cn  31900  qqhval2lem  31940  nexple  31986  esumpcvgval  32055  esumcvg  32063  sigaclcu3  32099  measiuns  32194  voliune  32206  volfiniune  32207  volmeas  32208  sgncl  32514  sgnmul  32518  gsumnunsn  32529  signsply0  32539  signswch  32549  signslema  32550  signstfvneq0  32560  chtvalz  32618  bnj517  32874  bnj1408  33025  bnj1423  33040  bnj1452  33041  onunel  33698  noinfbnd2lem1  33942  noetasuplem4  33948  noetainflem4  33952  dnibndlem13  34679  dnibnd  34680  irrdifflemf  35505  poimirlem2  35788  fdc  35912  orel  36269  lsatcvat  37071  lkrpssN  37184  2at0mat0  37546  atmod1i1m  37879  lhp2at0nle  38056  trlcone  38749  tendoex  38996  dihlspsnssN  39353  dochkrsm  39479  lcfl8  39523  lclkrlem2b  39529  lclkrlem2s  39546  lcfrlem21  39584  mapdval2N  39651  mapdspex  39689  aks4d1p5  40095  sticksstones12a  40120  sticksstones13  40122  fsuppind  40286  flt4lem7  40503  nna4b4nsq  40504  pell1qrgaplem  40702  monotoddzzfi  40771  oddcomabszz  40773  zindbi  40775  rmxnn  40780  jm2.24  40792  acongeq  40812  jm2.23  40825  jm2.26lem3  40830  wepwsolem  40874  fzuntgd  41072  frege102d  41369  fnchoice  42579  refsum2cnlem1  42587  wallispilem3  43615  wtgoldbnnsum4prm  45265  bgoldbnnsum3prm  45267  nn0sumshdiglem1  45978  mofeu  46186  toslat  46279