Theorem mpjaodan 960

Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule ∨ E (∨ elimination), see natded 30384. (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  6459  weniso  7347  isf32lem2  10368  isf32lem4  10370  fpwwe2lem10  10654  fpwwe2lem11  10655  lecasei  11341  ltlecasei  11343  xaddass  13265  xlesubadd  13279  xmulge0  13300  xadddi2  13313  xrsupss  13325  xrinfmss  13326  fzm1  13624  seqf1olem2  14060  expaddzlem  14123  discr  14258  fzomaxdif  15362  iseralt  15701  sumrb  15729  telfsumo  15818  fsumparts  15822  ntrivcvgtail  15916  prodrb  15948  bitsf1  16465  smupvallem  16502  eucalgf  16602  eucalginv  16603  vdwmc2  16999  fvprif  17575  mreexmrid  17655  mreexexlem3d  17658  mulgfval  19052  ressmulgnn0  19060  mulgnn0p1  19068  mulgnn0subcl  19070  mulgsubcl  19071  mulgneg  19075  mulgz  19085  mulgnn0dir  19087  mulgdirlem  19088  mulgdir  19089  submmulg  19101  ghmmulg  19211  odid  19519  oddvds  19528  dfod2  19545  gexid  19562  gexdvds  19565  mulgnn0di  19806  mulgdi  19807  gsumzsplit  19908  2nsgsimpgd  20085  prmgrpsimpgd  20097  lringuplu  20504  lsppratlem5  21112  prmirred  21435  mhpmulcl  22087  1stckgenlem  23491  qtoprest  23655  tgpmulg  24031  tsmssplit  24090  xblss2ps  24340  xblss2  24341  metustfbas  24496  nmoix  24668  nmoleub  24670  idnghm  24682  blcvx  24737  icccmp  24765  xrge0tsms  24774  metdstri  24791  nmoleub2lem  25065  rrxcph  25344  rrxdstprj1  25361  ivthle  25409  ivthle2  25410  dyadmbl  25553  volivth  25560  itg2const2  25694  itg2mulc  25700  dvlip2  25952  dvfsumlem1  25984  mdegmullem  26035  coemulhi  26211  dgrcolem2  26232  coseq00topi  26463  abssinper  26482  cxplea  26657  cxple2  26658  cxple2a  26660  cxpcn3  26710  cxpaddlelem  26713  cxpaddle  26714  ang180lem3  26773  dcubic2  26806  birthdaylem2  26914  jensen  26951  ppiltx  27139  chtub  27175  bcmono  27240  bcmax  27241  bpos  27256  lgseisenlem1  27338  2sqlem4  27384  2sqmod  27399  pntrlog2bndlem5  27544  pntpbnd1  27549  noinfbnd2lem1  27694  noetasuplem4  27700  noetainflem4  27704  mulsproplem12  28082  mulsproplem13  28083  mulsproplem14  28084  slemuld  28093  mulsge0d  28101  mulscan2d  28134  slemul1ad  28137  absmuls  28198  abssneg  28201  sleabs  28202  tgldimor  28481  tgifscgr  28487  tgcgrxfr  28497  tgbtwnconn1  28554  tgbtwnconn2  28555  tgbtwnconn3  28556  tgbtwnconnln3  28557  tgbtwnconn22  28558  tgbtwnconnln1  28559  tgbtwnconnln2  28560  legtrid  28570  legbtwn  28573  tgcgrsub2  28574  legov3  28577  hlln  28586  hltr  28589  btwnhl  28593  ncolncol  28625  mirconn  28657  krippen  28670  midexlem  28671  midex  28716  opphllem2  28727  opphllem5  28730  opphllem6  28731  outpasch  28734  hlpasch  28735  trgcopyeulem  28784  cgrahl  28806  cgracol  28807  ex-natded5.7  30392  ex-natded5.13  30396  ex-natded9.20  30398  ex-natded9.20-2  30399  suppovss  32658  xrge0infss  32737  xnn0gt0  32746  nn0xmulclb  32748  difioo  32759  iundisjcnt  32775  f1ocnt  32779  fzo0opth  32782  hashxpe  32786  sgncl  32810  sgnmul  32814  nexple  32823  2exple2exp  32824  ccatws1f1o  32927  chnub  32992  chnccats1  32995  xrsmulgzz  33001  xrge0addgt0  33012  xrge0adddir  33013  ressmulgnn0d  33039  xrge0tsmsd  33056  gsumwun  33059  tocyc01  33129  cycpmco2lem4  33140  cycpmco2lem7  33143  cycpmco2  33144  cyc3co2  33151  cycpmrn  33154  archirngz  33187  archiabllem2a  33192  elrgspnlem2  33238  ssdifidllem  33471  ssmxidllem  33488  rprmirred  33546  rprmdvdspow  33548  1arithufdlem3  33561  dfufd2lem  33564  ply1dg3rt0irred  33595  lindsun  33665  lbsdiflsp0  33666  fldextrspunlsplem  33714  constrmon  33778  constrconj  33779  constrfin  33780  constrelextdg2  33781  constrextdg2lem  33782  zconstr  33798  submateq  33840  lmat22lem  33848  locfinref  33872  xrge0mulc1cn  33972  zrhcntr  34010  qqhval2lem  34012  esumpcvgval  34109  esumcvg  34117  sigaclcu3  34153  measiuns  34248  voliune  34260  volfiniune  34261  volmeas  34262  gsumnunsn  34573  signsply0  34583  signswch  34593  signslema  34594  signstfvneq0  34604  chtvalz  34661  bnj517  34916  bnj1408  35067  bnj1423  35082  bnj1452  35083  weiunse  36486  dnibndlem13  36508  dnibnd  36509  irrdifflemf  37343  poimirlem2  37646  fdc  37769  orel  38126  lsatcvat  39068  lkrpssN  39181  2at0mat0  39544  atmod1i1m  39877  lhp2at0nle  40054  trlcone  40747  tendoex  40994  dihlspsnssN  41351  dochkrsm  41477  lcfl8  41521  lclkrlem2b  41527  lclkrlem2s  41544  lcfrlem21  41582  mapdval2N  41649  mapdspex  41687  aks4d1p5  42093  hashnexinjle  42142  sticksstones12a  42170  sticksstones13  42172  fimgmcyclem  42556  fsuppind  42613  flt4lem7  42682  nna4b4nsq  42683  pell1qrgaplem  42896  monotoddzzfi  42966  oddcomabszz  42968  zindbi  42970  rmxnn  42975  jm2.24  42987  acongeq  43007  jm2.23  43020  jm2.26lem3  43025  wepwsolem  43066  oe0rif  43309  onmcl  43355  omabs2  43356  omcl2  43357  onsucunipr  43396  oaun3lem1  43398  fzuntgd  43482  frege102d  43778  fnchoice  45053  refsum2cnlem1  45061  wallispilem3  46096  squeezedltsq  46918  wtgoldbnnsum4prm  47816  bgoldbnnsum3prm  47818  nn0sumshdiglem1  48601  mofeu  48826  toslat  48956  2arwcatlem2  49473  2arwcatlem3  49474  2arwcatlem4  49475  2arwcatlem5  49476  2arwcat  49477