Theorem mpjaodan 973

Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule ∨ E (∨ elimination), see natded 31037. (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 700	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ wo 861

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 402  df-or 862

This theorem is used by:  onunel  6491  weniso  7390  isf32lem2  10462  isf32lem4  10464  fpwwe2lem10  10755  fpwwe2lem11  10756  lecasei  11446  ltlecasei  11448  xaddass  13409  xlesubadd  13423  xmulge0  13444  xadddi2  13457  xrsupss  13469  xrinfmss  13470  fzm1  13771  seqf1olem2  14215  expaddzlem  14278  discr  14414  sgncl  15282  sgnmul  15292  fzomaxdif  15543  iseralt  15884  sumrb  15911  telfsumo  16001  fsumparts  16005  ntrivcvgtail  16101  prodrb  16131  bitsf1  16648  smupvallem  16685  eucalgf  16790  eucalginv  16791  vdwmc2  17189  fvprif  17765  mreexmrid  17849  mreexexlem3d  17852  chnub  18828  chnccats1  18831  chnccat  18832  mulgfval  19311  ressmulgnn0  19319  mulgnn0p1  19327  mulgnn0subcl  19329  mulgsubcl  19330  mulgneg  19334  mulgz  19344  mulgnn0dir  19346  mulgdirlem  19347  mulgdir  19348  submmulg  19360  ghmmulg  19474  odid  19785  oddvds  19794  dfod2  19811  gexid  19828  gexdvds  19831  mulgnn0di  20072  mulgdi  20073  gsumzsplit  20174  2nsgsimpgd  20351  prmgrpsimpgd  20363  lringuplu  20829  lsppratlem5  21462  ssdifidllem  21673  prmirred  21813  mhpmulcl  22503  1stckgenlem  23905  qtoprest  24069  tgpmulg  24445  tsmssplit  24504  xblss2ps  24753  xblss2  24754  metustfbas  24909  nmoix  25081  nmoleub  25083  idnghm  25095  blcvx  25150  icccmp  25178  xrge0tsms  25187  metdstri  25204  nmoleub2lem  25468  rrxcph  25746  rrxdstprj1  25763  ivthle  25810  ivthle2  25811  dyadmbl  25954  volivth  25961  itg2const2  26095  itg2mulc  26101  dvlip2  26348  dvfsumlem1  26379  mdegmullem  26429  coemulhi  26606  dgrcolem2  26626  coseq00topi  26864  abssinper  26882  cxplea  27057  cxple2  27058  cxple2a  27060  cxpcn3  27109  cxpaddlelem  27112  cxpaddle  27113  ang180lem3  27172  dcubic2  27205  birthdaylem2  27313  jensen  27349  ppiltx  27537  chtub  27572  bcmono  27637  bcmax  27638  bpos  27653  lgseisenlem1  27735  2sqlem4  27781  2sqmod  27796  pntrlog2bndlem5  27941  pntpbnd1  27946  flt4lem7  28022  nna4b4nsq  28023  noinfbnd2lem1  28120  noetasuplem4  28126  noetainflem4  28130  mulsproplem12  28546  mulsproplem13  28547  mulsproplem14  28548  lemulsd  28557  mulsge0d  28565  mulscan2d  28598  lemuls1ad  28601  absmuls  28663  absnegs  28666  leabss  28667  tgldimor  28998  tgifscgr  29004  tgcgrxfr  29014  tgbtwnconn1  29071  tgbtwnconn2  29072  tgbtwnconn3  29073  tgbtwnconnln3  29074  tgbtwnconn22  29075  tgbtwnconnln1  29076  tgbtwnconnln2  29077  legtrid  29087  legbtwn  29090  tgcgrsub2  29091  legov3  29094  hlln  29106  hltr  29109  btwnhl  29113  ncolncol  29148  mirconn  29183  krippen  29196  midexlem  29197  midex  29246  opphllem2  29257  opphllem5  29260  opphllem6  29261  outpasch  29266  hlpasch  29267  plngcplem  29296  plngrotlem1  29298  plngrotlem2  29299  lnssplng  29303  trgcopyeulem  29345  cgrahl  29368  cgracol  29369  tgaaddcpbllem3  29384  tgaaddcpbl2  29386  angmgmaddov1lem  29419  angmgmaddov2lem  29420  angmgmaddcpbl  29423  angmgmaddcl  29424  angmgmaddrid  29426  prlngmolem2  29464  ex-natded5.7  31045  ex-natded5.13  31049  ex-natded9.20  31051  ex-natded9.20-2  31052  inagbtwn  33081  inagcgratrgn  33091  cgrainag  33093  tgextahpl  33102  tgextahp  33106  tgaasne  33115  fconst7v  33289  suppovss  33348  nn0mnfxrd  33416  xrge0infss  33425  xnn0gt0  33434  nn0xmulclb  33436  difioo  33447  iundisjcnt  33463  f1ocnt  33465  fzo0opth  33468  hashxpe  33472  nexple  33497  2exple2exp  33498  ccatws1f1o  33587  xrsmulgzz  33646  xrge0addgt0  33654  xrge0adddir  33655  ressmulgnn0d  33681  xrge0tsmsd  33710  gsumwun  33713  tocyc01  33755  cycpmco2lem4  33766  cycpmco2lem7  33769  cycpmco2  33770  cyc3co2  33777  cycpmrn  33780  archirngz  33826  archiabllem2a  33831  elrgspnlem2  33880  edompidlem  33940  ssmxidllem  34082  rprmirred  34147  rprmdvdspow  34149  1arithufdlem3  34162  dfufd2lem  34165  ply1dg3rt0irred  34199  esplyfval1  34288  lindsun  34340  lbsdiflsp0  34341  fldextrspunlsplem  34388  constrmon  34459  constrconj  34460  constrfin  34461  constrelextdg2  34462  constrextdg2lem  34463  zconstr  34479  submateq  34524  lmat22lem  34532  locfinref  34556  xrge0mulc1cn  34656  zrhcntr  34694  qqhval2lem  34696  esumpcvgval  34793  esumcvg  34801  sigaclcu3  34837  measiuns  34933  voliune  34945  volfiniune  34946  volmeas  34947  gsumnunsn  35256  signsply0  35263  signswch  35273  signslema  35274  signstfvneq0  35284  chtvalz  35341  btwnlng13  35382  bnj517  35598  bnj1408  35749  bnj1423  35764  bnj1452  35765  weiunse  37447  dnibndlem13  37547  dnibnd  37548  irrdifflemf  38451  poimirlem2  38745  fdc  38882  orel  39237  lsatcvat  40310  lkrpssN  40423  2at0mat0  40785  atmod1i1m  41118  lhp2at0nle  41295  trlcone  41988  tendoex  42235  dihlspsnssN  42592  dochkrsm  42718  lcfl8  42762  lclkrlem2b  42768  lclkrlem2s  42785  lcfrlem21  42823  mapdval2N  42890  mapdspex  42928  aks4d1p5  43333  hashnexinjle  43382  sticksstones12a  43410  sticksstones13  43412  sn-msqgt0d  43754  fimgmcyclem  43801  fsuppind  43822  pell1qrgaplem  44084  monotoddzzfi  44153  oddcomabszz  44155  zindbi  44157  rmxnn  44162  jm2.24  44174  acongeq  44194  jm2.23  44207  jm2.26lem3  44212  wepwsolem  44253  oe0rif  44490  onmcl  44536  omabs2  44537  omcl2  44538  onsucunipr  44577  oaun3lem1  44579  fzuntgd  44662  frege102d  44957  fnchoice  46262  refsum2cnlem1  46270  wallispilem3  47292  chnsubseqwl  48104  wtgoldbnnsum4prm  49115  bgoldbnnsum3prm  49117  nn0sumshdiglem1  49948  mofeu  50174  toslat  50311  2arwcatlem2  50949  2arwcatlem3  50950  2arwcatlem4  50951  2arwcatlem5  50952  2arwcat  50953  parhomco2  50975  parhomco  50976  parmapco2  50987  parmapco  50988  veronesevrowd  51291