Theorem mpjaodan 955

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 843

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 206  df-an 396  df-or 844

This theorem is referenced by:  mpjao3danOLD  1430  weniso  7205  isf32lem2  10041  isf32lem4  10043  fpwwe2lem10  10327  fpwwe2lem11  10328  lecasei  11011  ltlecasei  11013  xaddass  12912  xlesubadd  12926  xmulge0  12947  xadddi2  12960  xrsupss  12972  xrinfmss  12973  fzm1  13265  seqf1olem2  13691  expaddzlem  13754  discr  13883  fzomaxdif  14983  iseralt  15324  sumrb  15353  telfsumo  15442  fsumparts  15446  ntrivcvgtail  15540  prodrb  15570  bitsf1  16081  smupvallem  16118  eucalgf  16216  eucalginv  16217  vdwmc2  16608  fvprif  17189  mreexmrid  17269  mreexexlem3d  17272  mulgfval  18617  mulgnn0p1  18630  mulgnn0subcl  18632  mulgsubcl  18633  mulgneg  18637  mulgz  18646  mulgnn0dir  18648  mulgdirlem  18649  mulgdir  18650  submmulg  18662  ghmmulg  18761  odid  19061  oddvds  19070  dfod2  19086  gexid  19101  gexdvds  19104  mulgnn0di  19342  mulgdi  19343  gsumzsplit  19443  2nsgsimpgd  19620  prmgrpsimpgd  19632  lsppratlem5  20328  prmirred  20608  mhpmulcl  21249  1stckgenlem  22612  qtoprest  22776  tgpmulg  23152  tsmssplit  23211  xblss2ps  23462  xblss2  23463  metustfbas  23619  nmoix  23799  nmoleub  23801  idnghm  23813  blcvx  23867  icccmp  23894  xrge0tsms  23903  metdstri  23920  nmoleub2lem  24183  rrxcph  24461  rrxdstprj1  24478  ivthle  24525  ivthle2  24526  dyadmbl  24669  volivth  24676  itg2const2  24811  itg2mulc  24817  dvlip2  25064  dvfsumlem1  25095  mdegmullem  25148  coemulhi  25320  dgrcolem2  25340  coseq00topi  25564  abssinper  25582  cxplea  25756  cxple2  25757  cxple2a  25759  cxpcn3  25806  cxpaddlelem  25809  cxpaddle  25810  ang180lem3  25866  dcubic2  25899  birthdaylem2  26007  jensen  26043  ppiltx  26231  chtub  26265  bcmono  26330  bcmax  26331  bpos  26346  lgseisenlem1  26428  2sqlem4  26474  2sqmod  26489  pntrlog2bndlem5  26634  pntpbnd1  26639  tgldimor  26767  tgifscgr  26773  tgcgrxfr  26783  tgbtwnconn1  26840  tgbtwnconn2  26841  tgbtwnconn3  26842  tgbtwnconnln3  26843  tgbtwnconn22  26844  tgbtwnconnln1  26845  tgbtwnconnln2  26846  legtrid  26856  legbtwn  26859  tgcgrsub2  26860  legov3  26863  hlln  26872  hltr  26875  btwnhl  26879  ncolncol  26911  mirconn  26943  krippen  26956  midexlem  26957  midex  27002  opphllem2  27013  opphllem5  27016  opphllem6  27017  outpasch  27020  hlpasch  27021  trgcopyeulem  27070  cgrahl  27092  cgracol  27093  ex-natded5.7  28676  ex-natded5.13  28680  ex-natded9.20  28682  ex-natded9.20-2  28683  suppovss  30919  xrge0infss  30985  xnn0gt0  30994  nn0xmulclb  30996  difioo  31005  iundisjcnt  31021  f1ocnt  31025  hashxpe  31029  xrsmulgzz  31189  ressmulgnn0  31195  xrge0addgt0  31202  xrge0adddir  31203  xrge0tsmsd  31219  tocyc01  31287  cycpmco2lem4  31298  cycpmco2lem7  31301  cycpmco2  31302  cyc3co2  31309  cycpmrn  31312  archirngz  31345  archiabllem2a  31350  ssmxidllem  31543  lindsun  31608  lbsdiflsp0  31609  submateq  31661  lmat22lem  31669  locfinref  31693  xrge0mulc1cn  31793  qqhval2lem  31831  nexple  31877  esumpcvgval  31946  esumcvg  31954  sigaclcu3  31990  measiuns  32085  voliune  32097  volfiniune  32098  volmeas  32099  sgncl  32405  sgnmul  32409  gsumnunsn  32420  signsply0  32430  signswch  32440  signslema  32441  signstfvneq0  32451  chtvalz  32509  bnj517  32765  bnj1408  32916  bnj1423  32931  bnj1452  32932  onunel  33592  noinfbnd2lem1  33860  noetasuplem4  33866  noetainflem4  33870  dnibndlem13  34597  dnibnd  34598  irrdifflemf  35423  poimirlem2  35706  fdc  35830  orel  36187  lsatcvat  36991  lkrpssN  37104  2at0mat0  37466  atmod1i1m  37799  lhp2at0nle  37976  trlcone  38669  tendoex  38916  dihlspsnssN  39273  dochkrsm  39399  lcfl8  39443  lclkrlem2b  39449  lclkrlem2s  39466  lcfrlem21  39504  mapdval2N  39571  mapdspex  39609  aks4d1p5  40016  sticksstones12a  40041  sticksstones13  40043  fsuppind  40202  flt4lem7  40412  nna4b4nsq  40413  pell1qrgaplem  40611  monotoddzzfi  40680  oddcomabszz  40682  zindbi  40684  rmxnn  40689  jm2.24  40701  acongeq  40721  jm2.23  40734  jm2.26lem3  40739  wepwsolem  40783  frege102d  41251  fnchoice  42461  refsum2cnlem1  42469  wallispilem3  43498  wtgoldbnnsum4prm  45142  bgoldbnnsum3prm  45144  nn0sumshdiglem1  45855  mofeu  46063  toslat  46156