Theorem mpjaodan 960

Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule ∨ E (∨ elimination), see natded 30332. (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  6439  weniso  7329  isf32lem2  10307  isf32lem4  10309  fpwwe2lem10  10593  fpwwe2lem11  10594  lecasei  11280  ltlecasei  11282  xaddass  13209  xlesubadd  13223  xmulge0  13244  xadddi2  13257  xrsupss  13269  xrinfmss  13270  fzm1  13568  seqf1olem2  14007  expaddzlem  14070  discr  14205  fzomaxdif  15310  iseralt  15651  sumrb  15679  telfsumo  15768  fsumparts  15772  ntrivcvgtail  15866  prodrb  15898  bitsf1  16416  smupvallem  16453  eucalgf  16553  eucalginv  16554  vdwmc2  16950  fvprif  17524  mreexmrid  17604  mreexexlem3d  17607  mulgfval  19001  ressmulgnn0  19009  mulgnn0p1  19017  mulgnn0subcl  19019  mulgsubcl  19020  mulgneg  19024  mulgz  19034  mulgnn0dir  19036  mulgdirlem  19037  mulgdir  19038  submmulg  19050  ghmmulg  19160  odid  19468  oddvds  19477  dfod2  19494  gexid  19511  gexdvds  19514  mulgnn0di  19755  mulgdi  19756  gsumzsplit  19857  2nsgsimpgd  20034  prmgrpsimpgd  20046  lringuplu  20453  lsppratlem5  21061  prmirred  21384  mhpmulcl  22036  1stckgenlem  23440  qtoprest  23604  tgpmulg  23980  tsmssplit  24039  xblss2ps  24289  xblss2  24290  metustfbas  24445  nmoix  24617  nmoleub  24619  idnghm  24631  blcvx  24686  icccmp  24714  xrge0tsms  24723  metdstri  24740  nmoleub2lem  25014  rrxcph  25292  rrxdstprj1  25309  ivthle  25357  ivthle2  25358  dyadmbl  25501  volivth  25508  itg2const2  25642  itg2mulc  25648  dvlip2  25900  dvfsumlem1  25932  mdegmullem  25983  coemulhi  26159  dgrcolem2  26180  coseq00topi  26411  abssinper  26430  cxplea  26605  cxple2  26606  cxple2a  26608  cxpcn3  26658  cxpaddlelem  26661  cxpaddle  26662  ang180lem3  26721  dcubic2  26754  birthdaylem2  26862  jensen  26899  ppiltx  27087  chtub  27123  bcmono  27188  bcmax  27189  bpos  27204  lgseisenlem1  27286  2sqlem4  27332  2sqmod  27347  pntrlog2bndlem5  27492  pntpbnd1  27497  noinfbnd2lem1  27642  noetasuplem4  27648  noetainflem4  27652  mulsproplem12  28030  mulsproplem13  28031  mulsproplem14  28032  slemuld  28041  mulsge0d  28049  mulscan2d  28082  slemul1ad  28085  absmuls  28146  abssneg  28149  sleabs  28150  tgldimor  28429  tgifscgr  28435  tgcgrxfr  28445  tgbtwnconn1  28502  tgbtwnconn2  28503  tgbtwnconn3  28504  tgbtwnconnln3  28505  tgbtwnconn22  28506  tgbtwnconnln1  28507  tgbtwnconnln2  28508  legtrid  28518  legbtwn  28521  tgcgrsub2  28522  legov3  28525  hlln  28534  hltr  28537  btwnhl  28541  ncolncol  28573  mirconn  28605  krippen  28618  midexlem  28619  midex  28664  opphllem2  28675  opphllem5  28678  opphllem6  28679  outpasch  28682  hlpasch  28683  trgcopyeulem  28732  cgrahl  28754  cgracol  28755  ex-natded5.7  30340  ex-natded5.13  30344  ex-natded9.20  30346  ex-natded9.20-2  30347  suppovss  32604  xrge0infss  32683  xnn0gt0  32692  nn0xmulclb  32694  difioo  32705  iundisjcnt  32721  f1ocnt  32725  fzo0opth  32728  hashxpe  32732  sgncl  32756  sgnmul  32760  nexple  32769  2exple2exp  32770  ccatws1f1o  32873  chnub  32938  chnccats1  32941  xrsmulgzz  32947  xrge0addgt0  32958  xrge0adddir  32959  ressmulgnn0d  32985  xrge0tsmsd  33002  gsumwun  33005  tocyc01  33075  cycpmco2lem4  33086  cycpmco2lem7  33089  cycpmco2  33090  cyc3co2  33097  cycpmrn  33100  archirngz  33143  archiabllem2a  33148  elrgspnlem2  33194  ssdifidllem  33427  ssmxidllem  33444  rprmirred  33502  rprmdvdspow  33504  1arithufdlem3  33517  dfufd2lem  33520  ply1dg3rt0irred  33551  lindsun  33621  lbsdiflsp0  33622  fldextrspunlsplem  33668  constrmon  33734  constrconj  33735  constrfin  33736  constrelextdg2  33737  constrextdg2lem  33738  zconstr  33754  submateq  33799  lmat22lem  33807  locfinref  33831  xrge0mulc1cn  33931  zrhcntr  33969  qqhval2lem  33971  esumpcvgval  34068  esumcvg  34076  sigaclcu3  34112  measiuns  34207  voliune  34219  volfiniune  34220  volmeas  34221  gsumnunsn  34532  signsply0  34542  signswch  34552  signslema  34553  signstfvneq0  34563  chtvalz  34620  bnj517  34875  bnj1408  35026  bnj1423  35041  bnj1452  35042  weiunse  36456  dnibndlem13  36478  dnibnd  36479  irrdifflemf  37313  poimirlem2  37616  fdc  37739  orel  38096  lsatcvat  39043  lkrpssN  39156  2at0mat0  39519  atmod1i1m  39852  lhp2at0nle  40029  trlcone  40722  tendoex  40969  dihlspsnssN  41326  dochkrsm  41452  lcfl8  41496  lclkrlem2b  41502  lclkrlem2s  41519  lcfrlem21  41557  mapdval2N  41624  mapdspex  41662  aks4d1p5  42068  hashnexinjle  42117  sticksstones12a  42145  sticksstones13  42147  sn-msqgt0d  42474  fimgmcyclem  42521  fsuppind  42578  flt4lem7  42647  nna4b4nsq  42648  pell1qrgaplem  42861  monotoddzzfi  42931  oddcomabszz  42933  zindbi  42935  rmxnn  42940  jm2.24  42952  acongeq  42972  jm2.23  42985  jm2.26lem3  42990  wepwsolem  43031  oe0rif  43274  onmcl  43320  omabs2  43321  omcl2  43322  onsucunipr  43361  oaun3lem1  43363  fzuntgd  43447  frege102d  43743  fnchoice  45023  refsum2cnlem1  45031  wallispilem3  46065  squeezedltsq  46887  wtgoldbnnsum4prm  47803  bgoldbnnsum3prm  47805  nn0sumshdiglem1  48610  mofeu  48836  toslat  48970  2arwcatlem2  49585  2arwcatlem3  49586  2arwcatlem4  49587  2arwcatlem5  49588  2arwcat  49589