Theorem mpjaodan 973

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∨ wo 860

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861

This theorem is used by:  onunel  6468  weniso  7352  isf32lem2  10342  isf32lem4  10344  fpwwe2lem10  10629  fpwwe2lem11  10630  lecasei  11320  ltlecasei  11322  xaddass  13279  xlesubadd  13293  xmulge0  13314  xadddi2  13327  xrsupss  13339  xrinfmss  13340  fzm1  13640  seqf1olem2  14083  expaddzlem  14146  discr  14281  sgncl  15139  sgnmul  15149  fzomaxdif  15400  iseralt  15741  sumrb  15769  telfsumo  15859  fsumparts  15863  ntrivcvgtail  15959  prodrb  15991  bitsf1  16508  smupvallem  16545  eucalgf  16645  eucalginv  16646  vdwmc2  17043  fvprif  17619  mreexmrid  17703  mreexexlem3d  17706  chnub  18682  chnccats1  18685  chnccat  18686  mulgfval  19139  ressmulgnn0  19147  mulgnn0p1  19155  mulgnn0subcl  19157  mulgsubcl  19158  mulgneg  19162  mulgz  19172  mulgnn0dir  19174  mulgdirlem  19175  mulgdir  19176  submmulg  19188  ghmmulg  19302  odid  19612  oddvds  19621  dfod2  19638  gexid  19655  gexdvds  19658  mulgnn0di  19899  mulgdi  19900  gsumzsplit  20001  2nsgsimpgd  20178  prmgrpsimpgd  20190  lringuplu  20652  lsppratlem5  21284  ssdifidllem  21493  prmirred  21633  mhpmulcl  22321  1stckgenlem  23719  qtoprest  23883  tgpmulg  24259  tsmssplit  24318  xblss2ps  24567  xblss2  24568  metustfbas  24723  nmoix  24895  nmoleub  24897  idnghm  24909  blcvx  24964  icccmp  24992  xrge0tsms  25001  metdstri  25018  nmoleub2lem  25282  rrxcph  25560  rrxdstprj1  25577  ivthle  25624  ivthle2  25625  dyadmbl  25768  volivth  25775  itg2const2  25909  itg2mulc  25915  dvlip2  26163  dvfsumlem1  26194  mdegmullem  26244  coemulhi  26420  dgrcolem2  26440  coseq00topi  26676  abssinper  26695  cxplea  26870  cxple2  26871  cxple2a  26873  cxpcn3  26922  cxpaddlelem  26925  cxpaddle  26926  ang180lem3  26985  dcubic2  27018  birthdaylem2  27126  jensen  27162  ppiltx  27350  chtub  27385  bcmono  27450  bcmax  27451  bpos  27466  lgseisenlem1  27548  2sqlem4  27594  2sqmod  27609  pntrlog2bndlem5  27754  pntpbnd1  27759  noinfbnd2lem1  27903  noetasuplem4  27909  noetainflem4  27913  mulsproplem12  28329  mulsproplem13  28330  mulsproplem14  28331  lemulsd  28340  mulsge0d  28348  mulscan2d  28381  lemuls1ad  28384  absmuls  28446  absnegs  28449  leabss  28450  tgldimor  28780  tgifscgr  28786  tgcgrxfr  28796  tgbtwnconn1  28853  tgbtwnconn2  28854  tgbtwnconn3  28855  tgbtwnconnln3  28856  tgbtwnconn22  28857  tgbtwnconnln1  28858  tgbtwnconnln2  28859  legtrid  28869  legbtwn  28872  tgcgrsub2  28873  legov3  28876  hlln  28888  hltr  28891  btwnhl  28895  ncolncol  28929  mirconn  28964  krippen  28977  midexlem  28978  midex  29027  opphllem2  29038  opphllem5  29041  opphllem6  29042  outpasch  29046  hlpasch  29047  plngcplem  29076  plngrotlem1  29078  plngrotlem2  29079  lnssplng  29083  trgcopyeulem  29125  cgrahl  29147  cgracol  29148  prlngmolem2  29212  ex-natded5.7  30771  ex-natded5.13  30775  ex-natded9.20  30777  ex-natded9.20-2  30778  fconst7v  32974  suppovss  33035  nn0mnfxrd  33105  xrge0infss  33114  xnn0gt0  33123  nn0xmulclb  33125  difioo  33136  iundisjcnt  33152  f1ocnt  33154  fzo0opth  33157  hashxpe  33161  nexple  33186  2exple2exp  33187  ccatws1f1o  33280  xrsmulgzz  33338  xrge0addgt0  33346  xrge0adddir  33347  ressmulgnn0d  33373  xrge0tsmsd  33402  gsumwun  33405  tocyc01  33447  cycpmco2lem4  33458  cycpmco2lem7  33461  cycpmco2  33462  cyc3co2  33469  cycpmrn  33472  archirngz  33518  archiabllem2a  33523  elrgspnlem2  33572  ssmxidllem  33765  rprmirred  33830  rprmdvdspow  33832  1arithufdlem3  33845  dfufd2lem  33848  ply1dg3rt0irred  33883  esplyfval1  33972  lindsun  34024  lbsdiflsp0  34025  fldextrspunlsplem  34072  constrmon  34143  constrconj  34144  constrfin  34145  constrelextdg2  34146  constrextdg2lem  34147  zconstr  34163  submateq  34208  lmat22lem  34216  locfinref  34240  xrge0mulc1cn  34340  zrhcntr  34378  qqhval2lem  34380  esumpcvgval  34477  esumcvg  34485  sigaclcu3  34521  measiuns  34616  voliune  34628  volfiniune  34629  volmeas  34630  gsumnunsn  34940  signsply0  34947  signswch  34957  signslema  34958  signstfvneq0  34968  chtvalz  35025  btwnlng13  35066  bnj517  35282  bnj1408  35433  bnj1423  35448  bnj1452  35449  weiunse  37007  dnibndlem13  37107  dnibnd  37108  irrdifflemf  37997  poimirlem2  38301  fdc  38424  orel  38779  lsatcvat  39852  lkrpssN  39965  2at0mat0  40327  atmod1i1m  40660  lhp2at0nle  40837  trlcone  41530  tendoex  41777  dihlspsnssN  42134  dochkrsm  42260  lcfl8  42304  lclkrlem2b  42310  lclkrlem2s  42327  lcfrlem21  42365  mapdval2N  42432  mapdspex  42470  aks4d1p5  42875  hashnexinjle  42924  sticksstones12a  42952  sticksstones13  42954  sn-msqgt0d  43288  fimgmcyclem  43329  fsuppind  43350  flt4lem7  43419  nna4b4nsq  43420  pell1qrgaplem  43628  monotoddzzfi  43697  oddcomabszz  43699  zindbi  43701  rmxnn  43706  jm2.24  43718  acongeq  43738  jm2.23  43751  jm2.26lem3  43756  wepwsolem  43797  oe0rif  44040  onmcl  44086  omabs2  44087  omcl2  44088  onsucunipr  44127  oaun3lem1  44129  fzuntgd  44212  frege102d  44508  fnchoice  45777  refsum2cnlem1  45785  wallispilem3  46809  chnsubseqwl  47623  squeezedltsq  47631  wtgoldbnnsum4prm  48595  bgoldbnnsum3prm  48597  nn0sumshdiglem1  49429  mofeu  49654  toslat  49788  2arwcatlem2  50402  2arwcatlem3  50403  2arwcatlem4  50404  2arwcatlem5  50405  2arwcat  50406