Theorem mpjaodan 956

Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule ∨ E (∨ elimination), see natded 28188. (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 686	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 399   ∨ 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 210  df-an 400  df-or 845

This theorem is referenced by:  mpjao3danOLD  1429  weniso  7086  isf32lem2  9765  isf32lem4  9767  fpwwe2lem11  10051  fpwwe2lem12  10052  lecasei  10735  ltlecasei  10737  xaddass  12630  xlesubadd  12644  xmulge0  12665  xadddi2  12678  xrsupss  12690  xrinfmss  12691  fzm1  12982  seqf1olem2  13406  expaddzlem  13468  discr  13597  fzomaxdif  14695  iseralt  15033  sumrb  15062  telfsumo  15149  fsumparts  15153  ntrivcvgtail  15248  prodrb  15278  bitsf1  15785  smupvallem  15822  eucalgf  15917  eucalginv  15918  vdwmc2  16305  fvprif  16826  mreexmrid  16906  mreexexlem3d  16909  mulgfval  18218  mulgnn0p1  18231  mulgnn0subcl  18233  mulgsubcl  18234  mulgneg  18238  mulgz  18247  mulgnn0dir  18249  mulgdirlem  18250  mulgdir  18251  submmulg  18263  ghmmulg  18362  odid  18658  oddvds  18667  dfod2  18683  gexid  18698  gexdvds  18701  mulgnn0di  18939  mulgdi  18940  gsumzsplit  19040  2nsgsimpgd  19217  prmgrpsimpgd  19229  lsppratlem5  19916  prmirred  20188  1stckgenlem  22158  qtoprest  22322  tgpmulg  22698  tsmssplit  22757  xblss2ps  23008  xblss2  23009  metustfbas  23164  nmoix  23335  nmoleub  23337  idnghm  23349  blcvx  23403  icccmp  23430  xrge0tsms  23439  metdstri  23456  nmoleub2lem  23719  rrxcph  23996  rrxdstprj1  24013  ivthle  24060  ivthle2  24061  dyadmbl  24204  volivth  24211  itg2const2  24345  itg2mulc  24351  dvlip2  24598  dvfsumlem1  24629  mdegmullem  24679  coemulhi  24851  dgrcolem2  24871  coseq00topi  25095  abssinper  25113  cxplea  25287  cxple2  25288  cxple2a  25290  cxpcn3  25337  cxpaddlelem  25340  cxpaddle  25341  ang180lem3  25397  dcubic2  25430  birthdaylem2  25538  jensen  25574  ppiltx  25762  chtub  25796  bcmono  25861  bcmax  25862  bpos  25877  lgseisenlem1  25959  2sqlem4  26005  2sqmod  26020  pntrlog2bndlem5  26165  pntpbnd1  26170  tgldimor  26296  tgifscgr  26302  tgcgrxfr  26312  tgbtwnconn1  26369  tgbtwnconn2  26370  tgbtwnconn3  26371  tgbtwnconnln3  26372  tgbtwnconn22  26373  tgbtwnconnln1  26374  tgbtwnconnln2  26375  legtrid  26385  legbtwn  26388  tgcgrsub2  26389  legov3  26392  hlln  26401  hltr  26404  btwnhl  26408  ncolncol  26440  mirconn  26472  krippen  26485  midexlem  26486  midex  26531  opphllem2  26542  opphllem5  26545  opphllem6  26546  outpasch  26549  hlpasch  26550  trgcopyeulem  26599  cgrahl  26621  cgracol  26622  ex-natded5.7  28196  ex-natded5.13  28200  ex-natded9.20  28202  ex-natded9.20-2  28203  suppovss  30443  xrge0infss  30510  xnn0gt0  30520  nn0xmulclb  30522  difioo  30531  iundisjcnt  30547  f1ocnt  30551  hashxpe  30555  xrsmulgzz  30712  ressmulgnn0  30718  xrge0addgt0  30725  xrge0adddir  30726  xrge0tsmsd  30742  tocyc01  30810  cycpmco2lem4  30821  cycpmco2lem7  30824  cycpmco2  30825  cyc3co2  30832  cycpmrn  30835  archirngz  30868  archiabllem2a  30873  ssmxidllem  31049  lindsun  31109  lbsdiflsp0  31110  submateq  31162  lmat22lem  31170  locfinref  31194  xrge0mulc1cn  31294  qqhval2lem  31332  nexple  31378  esumpcvgval  31447  esumcvg  31455  sigaclcu3  31491  measiuns  31586  voliune  31598  volfiniune  31599  volmeas  31600  sgncl  31906  sgnmul  31910  gsumnunsn  31921  signsply0  31931  signswch  31941  signslema  31942  signstfvneq0  31952  chtvalz  32010  bnj517  32267  bnj1408  32418  bnj1423  32433  bnj1452  32434  noetalem3  33332  dnibndlem13  33942  dnibnd  33943  irrdifflemf  34739  poimirlem2  35059  fdc  35183  orel  35540  lsatcvat  36346  lkrpssN  36459  2at0mat0  36821  atmod1i1m  37154  lhp2at0nle  37331  trlcone  38024  tendoex  38271  dihlspsnssN  38628  dochkrsm  38754  lcfl8  38798  lclkrlem2b  38804  lclkrlem2s  38821  lcfrlem21  38859  mapdval2N  38926  mapdspex  38964  fsuppind  39456  pell1qrgaplem  39814  monotoddzzfi  39883  oddcomabszz  39885  zindbi  39887  rmxnn  39892  jm2.24  39904  acongeq  39924  jm2.23  39937  jm2.26lem3  39942  wepwsolem  39986  frege102d  40455  fnchoice  41658  refsum2cnlem1  41666  wallispilem3  42709  wtgoldbnnsum4prm  44320  bgoldbnnsum3prm  44322  nn0sumshdiglem1  45035