Theorem mpjaodan 960

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 847

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 207  df-an 396  df-or 848

This theorem is referenced by:  onunel  6442  weniso  7332  isf32lem2  10314  isf32lem4  10316  fpwwe2lem10  10600  fpwwe2lem11  10601  lecasei  11287  ltlecasei  11289  xaddass  13216  xlesubadd  13230  xmulge0  13251  xadddi2  13264  xrsupss  13276  xrinfmss  13277  fzm1  13575  seqf1olem2  14014  expaddzlem  14077  discr  14212  fzomaxdif  15317  iseralt  15658  sumrb  15686  telfsumo  15775  fsumparts  15779  ntrivcvgtail  15873  prodrb  15905  bitsf1  16423  smupvallem  16460  eucalgf  16560  eucalginv  16561  vdwmc2  16957  fvprif  17531  mreexmrid  17611  mreexexlem3d  17614  mulgfval  19008  ressmulgnn0  19016  mulgnn0p1  19024  mulgnn0subcl  19026  mulgsubcl  19027  mulgneg  19031  mulgz  19041  mulgnn0dir  19043  mulgdirlem  19044  mulgdir  19045  submmulg  19057  ghmmulg  19167  odid  19475  oddvds  19484  dfod2  19501  gexid  19518  gexdvds  19521  mulgnn0di  19762  mulgdi  19763  gsumzsplit  19864  2nsgsimpgd  20041  prmgrpsimpgd  20053  lringuplu  20460  lsppratlem5  21068  prmirred  21391  mhpmulcl  22043  1stckgenlem  23447  qtoprest  23611  tgpmulg  23987  tsmssplit  24046  xblss2ps  24296  xblss2  24297  metustfbas  24452  nmoix  24624  nmoleub  24626  idnghm  24638  blcvx  24693  icccmp  24721  xrge0tsms  24730  metdstri  24747  nmoleub2lem  25021  rrxcph  25299  rrxdstprj1  25316  ivthle  25364  ivthle2  25365  dyadmbl  25508  volivth  25515  itg2const2  25649  itg2mulc  25655  dvlip2  25907  dvfsumlem1  25939  mdegmullem  25990  coemulhi  26166  dgrcolem2  26187  coseq00topi  26418  abssinper  26437  cxplea  26612  cxple2  26613  cxple2a  26615  cxpcn3  26665  cxpaddlelem  26668  cxpaddle  26669  ang180lem3  26728  dcubic2  26761  birthdaylem2  26869  jensen  26906  ppiltx  27094  chtub  27130  bcmono  27195  bcmax  27196  bpos  27211  lgseisenlem1  27293  2sqlem4  27339  2sqmod  27354  pntrlog2bndlem5  27499  pntpbnd1  27504  noinfbnd2lem1  27649  noetasuplem4  27655  noetainflem4  27659  mulsproplem12  28037  mulsproplem13  28038  mulsproplem14  28039  slemuld  28048  mulsge0d  28056  mulscan2d  28089  slemul1ad  28092  absmuls  28153  abssneg  28156  sleabs  28157  tgldimor  28436  tgifscgr  28442  tgcgrxfr  28452  tgbtwnconn1  28509  tgbtwnconn2  28510  tgbtwnconn3  28511  tgbtwnconnln3  28512  tgbtwnconn22  28513  tgbtwnconnln1  28514  tgbtwnconnln2  28515  legtrid  28525  legbtwn  28528  tgcgrsub2  28529  legov3  28532  hlln  28541  hltr  28544  btwnhl  28548  ncolncol  28580  mirconn  28612  krippen  28625  midexlem  28626  midex  28671  opphllem2  28682  opphllem5  28685  opphllem6  28686  outpasch  28689  hlpasch  28690  trgcopyeulem  28739  cgrahl  28761  cgracol  28762  ex-natded5.7  30347  ex-natded5.13  30351  ex-natded9.20  30353  ex-natded9.20-2  30354  suppovss  32611  xrge0infss  32690  xnn0gt0  32699  nn0xmulclb  32701  difioo  32712  iundisjcnt  32728  f1ocnt  32732  fzo0opth  32735  hashxpe  32739  sgncl  32763  sgnmul  32767  nexple  32776  2exple2exp  32777  ccatws1f1o  32880  chnub  32945  chnccats1  32948  xrsmulgzz  32954  xrge0addgt0  32965  xrge0adddir  32966  ressmulgnn0d  32992  xrge0tsmsd  33009  gsumwun  33012  tocyc01  33082  cycpmco2lem4  33093  cycpmco2lem7  33096  cycpmco2  33097  cyc3co2  33104  cycpmrn  33107  archirngz  33150  archiabllem2a  33155  elrgspnlem2  33201  ssdifidllem  33434  ssmxidllem  33451  rprmirred  33509  rprmdvdspow  33511  1arithufdlem3  33524  dfufd2lem  33527  ply1dg3rt0irred  33558  lindsun  33628  lbsdiflsp0  33629  fldextrspunlsplem  33675  constrmon  33741  constrconj  33742  constrfin  33743  constrelextdg2  33744  constrextdg2lem  33745  zconstr  33761  submateq  33806  lmat22lem  33814  locfinref  33838  xrge0mulc1cn  33938  zrhcntr  33976  qqhval2lem  33978  esumpcvgval  34075  esumcvg  34083  sigaclcu3  34119  measiuns  34214  voliune  34226  volfiniune  34227  volmeas  34228  gsumnunsn  34539  signsply0  34549  signswch  34559  signslema  34560  signstfvneq0  34570  chtvalz  34627  bnj517  34882  bnj1408  35033  bnj1423  35048  bnj1452  35049  weiunse  36463  dnibndlem13  36485  dnibnd  36486  irrdifflemf  37320  poimirlem2  37623  fdc  37746  orel  38103  lsatcvat  39050  lkrpssN  39163  2at0mat0  39526  atmod1i1m  39859  lhp2at0nle  40036  trlcone  40729  tendoex  40976  dihlspsnssN  41333  dochkrsm  41459  lcfl8  41503  lclkrlem2b  41509  lclkrlem2s  41526  lcfrlem21  41564  mapdval2N  41631  mapdspex  41669  aks4d1p5  42075  hashnexinjle  42124  sticksstones12a  42152  sticksstones13  42154  sn-msqgt0d  42481  fimgmcyclem  42528  fsuppind  42585  flt4lem7  42654  nna4b4nsq  42655  pell1qrgaplem  42868  monotoddzzfi  42938  oddcomabszz  42940  zindbi  42942  rmxnn  42947  jm2.24  42959  acongeq  42979  jm2.23  42992  jm2.26lem3  42997  wepwsolem  43038  oe0rif  43281  onmcl  43327  omabs2  43328  omcl2  43329  onsucunipr  43368  oaun3lem1  43370  fzuntgd  43454  frege102d  43750  fnchoice  45030  refsum2cnlem1  45038  wallispilem3  46072  squeezedltsq  46894  wtgoldbnnsum4prm  47807  bgoldbnnsum3prm  47809  nn0sumshdiglem1  48614  mofeu  48840  toslat  48974  2arwcatlem2  49589  2arwcatlem3  49590  2arwcatlem4  49591  2arwcatlem5  49592  2arwcat  49593