Theorem mpjaodan 960

Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule ∨ E (∨ elimination), see natded 30478. (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  6424  weniso  7300  isf32lem2  10264  isf32lem4  10266  fpwwe2lem10  10551  fpwwe2lem11  10552  lecasei  11239  ltlecasei  11241  xaddass  13164  xlesubadd  13178  xmulge0  13199  xadddi2  13212  xrsupss  13224  xrinfmss  13225  fzm1  13523  seqf1olem2  13965  expaddzlem  14028  discr  14163  fzomaxdif  15267  iseralt  15608  sumrb  15636  telfsumo  15725  fsumparts  15729  ntrivcvgtail  15823  prodrb  15855  bitsf1  16373  smupvallem  16410  eucalgf  16510  eucalginv  16511  vdwmc2  16907  fvprif  17482  mreexmrid  17566  mreexexlem3d  17569  chnub  18545  chnccats1  18548  chnccat  18549  mulgfval  18999  ressmulgnn0  19007  mulgnn0p1  19015  mulgnn0subcl  19017  mulgsubcl  19018  mulgneg  19022  mulgz  19032  mulgnn0dir  19034  mulgdirlem  19035  mulgdir  19036  submmulg  19048  ghmmulg  19157  odid  19467  oddvds  19476  dfod2  19493  gexid  19510  gexdvds  19513  mulgnn0di  19754  mulgdi  19755  gsumzsplit  19856  2nsgsimpgd  20033  prmgrpsimpgd  20045  lringuplu  20477  lsppratlem5  21106  prmirred  21429  mhpmulcl  22092  1stckgenlem  23497  qtoprest  23661  tgpmulg  24037  tsmssplit  24096  xblss2ps  24345  xblss2  24346  metustfbas  24501  nmoix  24673  nmoleub  24675  idnghm  24687  blcvx  24742  icccmp  24770  xrge0tsms  24779  metdstri  24796  nmoleub2lem  25070  rrxcph  25348  rrxdstprj1  25365  ivthle  25413  ivthle2  25414  dyadmbl  25557  volivth  25564  itg2const2  25698  itg2mulc  25704  dvlip2  25956  dvfsumlem1  25988  mdegmullem  26039  coemulhi  26215  dgrcolem2  26236  coseq00topi  26467  abssinper  26486  cxplea  26661  cxple2  26662  cxple2a  26664  cxpcn3  26714  cxpaddlelem  26717  cxpaddle  26718  ang180lem3  26777  dcubic2  26810  birthdaylem2  26918  jensen  26955  ppiltx  27143  chtub  27179  bcmono  27244  bcmax  27245  bpos  27260  lgseisenlem1  27342  2sqlem4  27388  2sqmod  27403  pntrlog2bndlem5  27548  pntpbnd1  27553  noinfbnd2lem1  27698  noetasuplem4  27704  noetainflem4  27708  mulsproplem12  28123  mulsproplem13  28124  mulsproplem14  28125  lemulsd  28134  mulsge0d  28142  mulscan2d  28175  lemuls1ad  28178  absmuls  28240  absnegs  28243  leabss  28244  tgldimor  28574  tgifscgr  28580  tgcgrxfr  28590  tgbtwnconn1  28647  tgbtwnconn2  28648  tgbtwnconn3  28649  tgbtwnconnln3  28650  tgbtwnconn22  28651  tgbtwnconnln1  28652  tgbtwnconnln2  28653  legtrid  28663  legbtwn  28666  tgcgrsub2  28667  legov3  28670  hlln  28679  hltr  28682  btwnhl  28686  ncolncol  28718  mirconn  28750  krippen  28763  midexlem  28764  midex  28809  opphllem2  28820  opphllem5  28823  opphllem6  28824  outpasch  28827  hlpasch  28828  trgcopyeulem  28877  cgrahl  28899  cgracol  28900  ex-natded5.7  30486  ex-natded5.13  30490  ex-natded9.20  30492  ex-natded9.20-2  30493  fconst7v  32698  suppovss  32760  nn0mnfxrd  32831  xrge0infss  32840  xnn0gt0  32849  nn0xmulclb  32851  difioo  32862  iundisjcnt  32878  f1ocnt  32880  fzo0opth  32883  hashxpe  32887  sgncl  32912  sgnmul  32916  nexple  32925  2exple2exp  32926  ccatws1f1o  33033  xrsmulgzz  33091  xrge0addgt0  33099  xrge0adddir  33100  ressmulgnn0d  33127  xrge0tsmsd  33155  gsumwun  33158  tocyc01  33200  cycpmco2lem4  33211  cycpmco2lem7  33214  cycpmco2  33215  cyc3co2  33222  cycpmrn  33225  archirngz  33271  archiabllem2a  33276  elrgspnlem2  33325  ssdifidllem  33537  ssmxidllem  33554  rprmirred  33612  rprmdvdspow  33614  1arithufdlem3  33627  dfufd2lem  33630  ply1dg3rt0irred  33665  lindsun  33782  lbsdiflsp0  33783  fldextrspunlsplem  33830  constrmon  33901  constrconj  33902  constrfin  33903  constrelextdg2  33904  constrextdg2lem  33905  zconstr  33921  submateq  33966  lmat22lem  33974  locfinref  33998  xrge0mulc1cn  34098  zrhcntr  34136  qqhval2lem  34138  esumpcvgval  34235  esumcvg  34243  sigaclcu3  34279  measiuns  34374  voliune  34386  volfiniune  34387  volmeas  34388  gsumnunsn  34698  signsply0  34708  signswch  34718  signslema  34719  signstfvneq0  34729  chtvalz  34786  bnj517  35041  bnj1408  35192  bnj1423  35207  bnj1452  35208  weiunse  36662  dnibndlem13  36690  dnibnd  36691  irrdifflemf  37530  poimirlem2  37823  fdc  37946  orel  38303  lsatcvat  39310  lkrpssN  39423  2at0mat0  39785  atmod1i1m  40118  lhp2at0nle  40295  trlcone  40988  tendoex  41235  dihlspsnssN  41592  dochkrsm  41718  lcfl8  41762  lclkrlem2b  41768  lclkrlem2s  41785  lcfrlem21  41823  mapdval2N  41890  mapdspex  41928  aks4d1p5  42334  hashnexinjle  42383  sticksstones12a  42411  sticksstones13  42413  sn-msqgt0d  42741  fimgmcyclem  42788  fsuppind  42833  flt4lem7  42902  nna4b4nsq  42903  pell1qrgaplem  43115  monotoddzzfi  43184  oddcomabszz  43186  zindbi  43188  rmxnn  43193  jm2.24  43205  acongeq  43225  jm2.23  43238  jm2.26lem3  43243  wepwsolem  43284  oe0rif  43527  onmcl  43573  omabs2  43574  omcl2  43575  onsucunipr  43614  oaun3lem1  43616  fzuntgd  43699  frege102d  43995  fnchoice  45274  refsum2cnlem1  45282  wallispilem3  46311  chnsubseqwl  47123  squeezedltsq  47132  wtgoldbnnsum4prm  48048  bgoldbnnsum3prm  48050  nn0sumshdiglem1  48867  mofeu  49093  toslat  49227  2arwcatlem2  49841  2arwcatlem3  49842  2arwcatlem4  49843  2arwcatlem5  49844  2arwcat  49845