Theorem mpjaodan 957

Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule ∨ E (∨ elimination), see natded 29410. (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  6427  weniso  7304  isf32lem2  10299  isf32lem4  10301  fpwwe2lem10  10585  fpwwe2lem11  10586  lecasei  11270  ltlecasei  11272  xaddass  13178  xlesubadd  13192  xmulge0  13213  xadddi2  13226  xrsupss  13238  xrinfmss  13239  fzm1  13531  seqf1olem2  13958  expaddzlem  14021  discr  14153  fzomaxdif  15240  iseralt  15581  sumrb  15609  telfsumo  15698  fsumparts  15702  ntrivcvgtail  15796  prodrb  15826  bitsf1  16337  smupvallem  16374  eucalgf  16470  eucalginv  16471  vdwmc2  16862  fvprif  17457  mreexmrid  17537  mreexexlem3d  17540  mulgfval  18888  mulgnn0p1  18901  mulgnn0subcl  18903  mulgsubcl  18904  mulgneg  18908  mulgz  18918  mulgnn0dir  18920  mulgdirlem  18921  mulgdir  18922  submmulg  18934  ghmmulg  19034  odid  19334  oddvds  19343  dfod2  19360  gexid  19377  gexdvds  19380  mulgnn0di  19618  mulgdi  19619  gsumzsplit  19718  2nsgsimpgd  19895  prmgrpsimpgd  19907  lringuplu  20224  lsppratlem5  20671  prmirred  20932  mhpmulcl  21576  1stckgenlem  22941  qtoprest  23105  tgpmulg  23481  tsmssplit  23540  xblss2ps  23791  xblss2  23792  metustfbas  23950  nmoix  24130  nmoleub  24132  idnghm  24144  blcvx  24198  icccmp  24225  xrge0tsms  24234  metdstri  24251  nmoleub2lem  24514  rrxcph  24793  rrxdstprj1  24810  ivthle  24857  ivthle2  24858  dyadmbl  25001  volivth  25008  itg2const2  25143  itg2mulc  25149  dvlip2  25396  dvfsumlem1  25427  mdegmullem  25480  coemulhi  25652  dgrcolem2  25672  coseq00topi  25896  abssinper  25914  cxplea  26088  cxple2  26089  cxple2a  26091  cxpcn3  26138  cxpaddlelem  26141  cxpaddle  26142  ang180lem3  26198  dcubic2  26231  birthdaylem2  26339  jensen  26375  ppiltx  26563  chtub  26597  bcmono  26662  bcmax  26663  bpos  26678  lgseisenlem1  26760  2sqlem4  26806  2sqmod  26821  pntrlog2bndlem5  26966  pntpbnd1  26971  noinfbnd2lem1  27115  noetasuplem4  27121  noetainflem4  27125  tgldimor  27507  tgifscgr  27513  tgcgrxfr  27523  tgbtwnconn1  27580  tgbtwnconn2  27581  tgbtwnconn3  27582  tgbtwnconnln3  27583  tgbtwnconn22  27584  tgbtwnconnln1  27585  tgbtwnconnln2  27586  legtrid  27596  legbtwn  27599  tgcgrsub2  27600  legov3  27603  hlln  27612  hltr  27615  btwnhl  27619  ncolncol  27651  mirconn  27683  krippen  27696  midexlem  27697  midex  27742  opphllem2  27753  opphllem5  27756  opphllem6  27757  outpasch  27760  hlpasch  27761  trgcopyeulem  27810  cgrahl  27832  cgracol  27833  ex-natded5.7  29418  ex-natded5.13  29422  ex-natded9.20  29424  ex-natded9.20-2  29425  suppovss  31665  xrge0infss  31733  xnn0gt0  31742  nn0xmulclb  31744  difioo  31753  iundisjcnt  31769  f1ocnt  31773  hashxpe  31779  xrsmulgzz  31939  ressmulgnn0  31945  xrge0addgt0  31952  xrge0adddir  31953  xrge0tsmsd  31969  tocyc01  32037  cycpmco2lem4  32048  cycpmco2lem7  32051  cycpmco2  32052  cyc3co2  32059  cycpmrn  32062  archirngz  32095  archiabllem2a  32100  ssmxidllem  32314  lindsun  32407  lbsdiflsp0  32408  submateq  32479  lmat22lem  32487  locfinref  32511  xrge0mulc1cn  32611  qqhval2lem  32651  nexple  32697  esumpcvgval  32766  esumcvg  32774  sigaclcu3  32810  measiuns  32905  voliune  32917  volfiniune  32918  volmeas  32919  sgncl  33227  sgnmul  33231  gsumnunsn  33242  signsply0  33252  signswch  33262  signslema  33263  signstfvneq0  33273  chtvalz  33331  bnj517  33586  bnj1408  33737  bnj1423  33752  bnj1452  33753  dnibndlem13  35029  dnibnd  35030  irrdifflemf  35869  poimirlem2  36153  fdc  36277  orel  36634  lsatcvat  37585  lkrpssN  37698  2at0mat0  38061  atmod1i1m  38394  lhp2at0nle  38571  trlcone  39264  tendoex  39511  dihlspsnssN  39868  dochkrsm  39994  lcfl8  40038  lclkrlem2b  40044  lclkrlem2s  40061  lcfrlem21  40099  mapdval2N  40166  mapdspex  40204  aks4d1p5  40610  sticksstones12a  40638  sticksstones13  40640  fsuppind  40823  flt4lem7  41055  nna4b4nsq  41056  pell1qrgaplem  41254  monotoddzzfi  41324  oddcomabszz  41326  zindbi  41328  rmxnn  41333  jm2.24  41345  acongeq  41365  jm2.23  41378  jm2.26lem3  41383  wepwsolem  41427  oe0rif  41678  onmcl  41724  omabs2  41725  omcl2  41726  onsucunipr  41765  oaun3lem1  41767  fzuntgd  41852  frege102d  42148  fnchoice  43356  refsum2cnlem1  43364  wallispilem3  44428  wtgoldbnnsum4prm  46114  bgoldbnnsum3prm  46116  nn0sumshdiglem1  46827  mofeu  47034  toslat  47127