Theorem mpjaodan 960

Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule ∨ E (∨ elimination), see natded 30431. (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  6490  weniso  7373  isf32lem2  10391  isf32lem4  10393  fpwwe2lem10  10677  fpwwe2lem11  10678  lecasei  11364  ltlecasei  11366  xaddass  13287  xlesubadd  13301  xmulge0  13322  xadddi2  13335  xrsupss  13347  xrinfmss  13348  fzm1  13643  seqf1olem2  14079  expaddzlem  14142  discr  14275  fzomaxdif  15378  iseralt  15717  sumrb  15745  telfsumo  15834  fsumparts  15838  ntrivcvgtail  15932  prodrb  15964  bitsf1  16479  smupvallem  16516  eucalgf  16616  eucalginv  16617  vdwmc2  17012  fvprif  17607  mreexmrid  17687  mreexexlem3d  17690  mulgfval  19099  ressmulgnn0  19107  mulgnn0p1  19115  mulgnn0subcl  19117  mulgsubcl  19118  mulgneg  19122  mulgz  19132  mulgnn0dir  19134  mulgdirlem  19135  mulgdir  19136  submmulg  19148  ghmmulg  19258  odid  19570  oddvds  19579  dfod2  19596  gexid  19613  gexdvds  19616  mulgnn0di  19857  mulgdi  19858  gsumzsplit  19959  2nsgsimpgd  20136  prmgrpsimpgd  20148  lringuplu  20560  lsppratlem5  21170  prmirred  21502  mhpmulcl  22170  1stckgenlem  23576  qtoprest  23740  tgpmulg  24116  tsmssplit  24175  xblss2ps  24426  xblss2  24427  metustfbas  24585  nmoix  24765  nmoleub  24767  idnghm  24779  blcvx  24833  icccmp  24860  xrge0tsms  24869  metdstri  24886  nmoleub2lem  25160  rrxcph  25439  rrxdstprj1  25456  ivthle  25504  ivthle2  25505  dyadmbl  25648  volivth  25655  itg2const2  25790  itg2mulc  25796  dvlip2  26048  dvfsumlem1  26080  mdegmullem  26131  coemulhi  26307  dgrcolem2  26328  coseq00topi  26558  abssinper  26577  cxplea  26752  cxple2  26753  cxple2a  26755  cxpcn3  26805  cxpaddlelem  26808  cxpaddle  26809  ang180lem3  26868  dcubic2  26901  birthdaylem2  27009  jensen  27046  ppiltx  27234  chtub  27270  bcmono  27335  bcmax  27336  bpos  27351  lgseisenlem1  27433  2sqlem4  27479  2sqmod  27494  pntrlog2bndlem5  27639  pntpbnd1  27644  noinfbnd2lem1  27789  noetasuplem4  27795  noetainflem4  27799  mulsproplem12  28167  mulsproplem13  28168  mulsproplem14  28169  slemuld  28178  mulsge0d  28186  mulscan2d  28219  slemul1ad  28222  absmuls  28282  abssneg  28285  sleabs  28286  tgldimor  28524  tgifscgr  28530  tgcgrxfr  28540  tgbtwnconn1  28597  tgbtwnconn2  28598  tgbtwnconn3  28599  tgbtwnconnln3  28600  tgbtwnconn22  28601  tgbtwnconnln1  28602  tgbtwnconnln2  28603  legtrid  28613  legbtwn  28616  tgcgrsub2  28617  legov3  28620  hlln  28629  hltr  28632  btwnhl  28636  ncolncol  28668  mirconn  28700  krippen  28713  midexlem  28714  midex  28759  opphllem2  28770  opphllem5  28773  opphllem6  28774  outpasch  28777  hlpasch  28778  trgcopyeulem  28827  cgrahl  28849  cgracol  28850  ex-natded5.7  30439  ex-natded5.13  30443  ex-natded9.20  30445  ex-natded9.20-2  30446  suppovss  32695  xrge0infss  32770  xnn0gt0  32779  nn0xmulclb  32781  difioo  32790  iundisjcnt  32805  f1ocnt  32809  fzo0opth  32812  hashxpe  32816  ccatws1f1o  32920  chnub  32985  xrsmulgzz  32993  xrge0addgt0  33004  xrge0adddir  33005  xrge0tsmsd  33047  gsumwun  33050  tocyc01  33120  cycpmco2lem4  33131  cycpmco2lem7  33134  cycpmco2  33135  cyc3co2  33142  cycpmrn  33145  archirngz  33178  archiabllem2a  33183  elrgspnlem2  33232  ssdifidllem  33463  ssmxidllem  33480  rprmirred  33538  rprmdvdspow  33540  1arithufdlem3  33553  dfufd2lem  33556  ply1dg3rt0irred  33586  lindsun  33652  lbsdiflsp0  33653  constrmon  33748  constrconj  33749  constrfin  33750  constrelextdg2  33751  submateq  33769  lmat22lem  33777  locfinref  33801  xrge0mulc1cn  33901  zrhcntr  33941  qqhval2lem  33943  nexple  33989  esumpcvgval  34058  esumcvg  34066  sigaclcu3  34102  measiuns  34197  voliune  34209  volfiniune  34210  volmeas  34211  sgncl  34519  sgnmul  34523  gsumnunsn  34534  signsply0  34544  signswch  34554  signslema  34555  signstfvneq0  34565  chtvalz  34622  bnj517  34877  bnj1408  35028  bnj1423  35043  bnj1452  35044  weiunse  36450  dnibndlem13  36472  dnibnd  36473  irrdifflemf  37307  poimirlem2  37608  fdc  37731  orel  38088  lsatcvat  39031  lkrpssN  39144  2at0mat0  39507  atmod1i1m  39840  lhp2at0nle  40017  trlcone  40710  tendoex  40957  dihlspsnssN  41314  dochkrsm  41440  lcfl8  41484  lclkrlem2b  41490  lclkrlem2s  41507  lcfrlem21  41545  mapdval2N  41612  mapdspex  41650  aks4d1p5  42061  hashnexinjle  42110  sticksstones12a  42138  sticksstones13  42140  fimgmcyclem  42519  fsuppind  42576  flt4lem7  42645  nna4b4nsq  42646  pell1qrgaplem  42860  monotoddzzfi  42930  oddcomabszz  42932  zindbi  42934  rmxnn  42939  jm2.24  42951  acongeq  42971  jm2.23  42984  jm2.26lem3  42989  wepwsolem  43030  oe0rif  43274  onmcl  43320  omabs2  43321  omcl2  43322  onsucunipr  43361  oaun3lem1  43363  fzuntgd  43447  frege102d  43743  fnchoice  44966  refsum2cnlem1  44974  wallispilem3  46022  wtgoldbnnsum4prm  47726  bgoldbnnsum3prm  47728  nn0sumshdiglem1  48470  mofeu  48677  toslat  48770