Theorem mpjaodan 957

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

Syntax hints:   → wi 4   ∧ wa 397   ∨ wo 845

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 398  df-or 846

This theorem is referenced by:  mpjao3danOLD  1432  weniso  7286  isf32lem2  10216  isf32lem4  10218  fpwwe2lem10  10502  fpwwe2lem11  10503  lecasei  11187  ltlecasei  11189  xaddass  13089  xlesubadd  13103  xmulge0  13124  xadddi2  13137  xrsupss  13149  xrinfmss  13150  fzm1  13442  seqf1olem2  13869  expaddzlem  13932  discr  14061  fzomaxdif  15155  iseralt  15496  sumrb  15525  telfsumo  15614  fsumparts  15618  ntrivcvgtail  15712  prodrb  15742  bitsf1  16253  smupvallem  16290  eucalgf  16386  eucalginv  16387  vdwmc2  16778  fvprif  17370  mreexmrid  17450  mreexexlem3d  17453  mulgfval  18799  mulgnn0p1  18812  mulgnn0subcl  18814  mulgsubcl  18815  mulgneg  18819  mulgz  18828  mulgnn0dir  18830  mulgdirlem  18831  mulgdir  18832  submmulg  18844  ghmmulg  18943  odid  19243  oddvds  19252  dfod2  19268  gexid  19283  gexdvds  19286  mulgnn0di  19523  mulgdi  19524  gsumzsplit  19623  2nsgsimpgd  19800  prmgrpsimpgd  19812  lsppratlem5  20519  prmirred  20802  mhpmulcl  21445  1stckgenlem  22810  qtoprest  22974  tgpmulg  23350  tsmssplit  23409  xblss2ps  23660  xblss2  23661  metustfbas  23819  nmoix  23999  nmoleub  24001  idnghm  24013  blcvx  24067  icccmp  24094  xrge0tsms  24103  metdstri  24120  nmoleub2lem  24383  rrxcph  24662  rrxdstprj1  24679  ivthle  24726  ivthle2  24727  dyadmbl  24870  volivth  24877  itg2const2  25012  itg2mulc  25018  dvlip2  25265  dvfsumlem1  25296  mdegmullem  25349  coemulhi  25521  dgrcolem2  25541  coseq00topi  25765  abssinper  25783  cxplea  25957  cxple2  25958  cxple2a  25960  cxpcn3  26007  cxpaddlelem  26010  cxpaddle  26011  ang180lem3  26067  dcubic2  26100  birthdaylem2  26208  jensen  26244  ppiltx  26432  chtub  26466  bcmono  26531  bcmax  26532  bpos  26547  lgseisenlem1  26629  2sqlem4  26675  2sqmod  26690  pntrlog2bndlem5  26835  pntpbnd1  26840  noinfbnd2lem1  26984  noetasuplem4  26990  noetainflem4  26994  tgldimor  27152  tgifscgr  27158  tgcgrxfr  27168  tgbtwnconn1  27225  tgbtwnconn2  27226  tgbtwnconn3  27227  tgbtwnconnln3  27228  tgbtwnconn22  27229  tgbtwnconnln1  27230  tgbtwnconnln2  27231  legtrid  27241  legbtwn  27244  tgcgrsub2  27245  legov3  27248  hlln  27257  hltr  27260  btwnhl  27264  ncolncol  27296  mirconn  27328  krippen  27341  midexlem  27342  midex  27387  opphllem2  27398  opphllem5  27401  opphllem6  27402  outpasch  27405  hlpasch  27406  trgcopyeulem  27455  cgrahl  27477  cgracol  27478  ex-natded5.7  29063  ex-natded5.13  29067  ex-natded9.20  29069  ex-natded9.20-2  29070  suppovss  31302  xrge0infss  31368  xnn0gt0  31377  nn0xmulclb  31379  difioo  31388  iundisjcnt  31404  f1ocnt  31408  hashxpe  31412  xrsmulgzz  31572  ressmulgnn0  31578  xrge0addgt0  31585  xrge0adddir  31586  xrge0tsmsd  31602  tocyc01  31670  cycpmco2lem4  31681  cycpmco2lem7  31684  cycpmco2  31685  cyc3co2  31692  cycpmrn  31695  archirngz  31728  archiabllem2a  31733  ssmxidllem  31936  lindsun  32002  lbsdiflsp0  32003  submateq  32055  lmat22lem  32063  locfinref  32087  xrge0mulc1cn  32187  qqhval2lem  32227  nexple  32273  esumpcvgval  32342  esumcvg  32350  sigaclcu3  32386  measiuns  32481  voliune  32493  volfiniune  32494  volmeas  32495  sgncl  32803  sgnmul  32807  gsumnunsn  32818  signsply0  32828  signswch  32838  signslema  32839  signstfvneq0  32849  chtvalz  32907  bnj517  33162  bnj1408  33313  bnj1423  33328  bnj1452  33329  onunel  33977  dnibndlem13  34807  dnibnd  34808  irrdifflemf  35650  poimirlem2  35933  fdc  36057  orel  36414  lsatcvat  37366  lkrpssN  37479  2at0mat0  37842  atmod1i1m  38175  lhp2at0nle  38352  trlcone  39045  tendoex  39292  dihlspsnssN  39649  dochkrsm  39775  lcfl8  39819  lclkrlem2b  39825  lclkrlem2s  39842  lcfrlem21  39880  mapdval2N  39947  mapdspex  39985  aks4d1p5  40391  sticksstones12a  40419  sticksstones13  40421  fsuppind  40588  flt4lem7  40807  nna4b4nsq  40808  pell1qrgaplem  41006  monotoddzzfi  41076  oddcomabszz  41078  zindbi  41080  rmxnn  41085  jm2.24  41097  acongeq  41117  jm2.23  41130  jm2.26lem3  41135  wepwsolem  41179  omabs2  41367  omcl2  41368  fzuntgd  41437  frege102d  41733  fnchoice  42943  refsum2cnlem1  42951  wallispilem3  43994  wtgoldbnnsum4prm  45670  bgoldbnnsum3prm  45672  nn0sumshdiglem1  46383  mofeu  46591  toslat  46684