Theorem mpjaodan 955

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

Syntax hints:   → wi 4   ∧ wa 398   ∨ 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 209  df-an 399  df-or 844

This theorem is referenced by:  mpjao3danOLD  1428  weniso  7106  isf32lem2  9775  isf32lem4  9777  fpwwe2lem11  10061  fpwwe2lem12  10062  lecasei  10745  ltlecasei  10747  xaddass  12641  xlesubadd  12655  xmulge0  12676  xadddi2  12689  xrsupss  12701  xrinfmss  12702  fzm1  12986  seqf1olem2  13409  expaddzlem  13471  discr  13600  fzomaxdif  14702  iseralt  15040  sumrb  15069  telfsumo  15156  fsumparts  15160  ntrivcvgtail  15255  prodrb  15285  bitsf1  15794  smupvallem  15831  eucalgf  15926  eucalginv  15927  vdwmc2  16314  fvprif  16833  mreexmrid  16913  mreexexlem3d  16916  mulgfval  18225  mulgnn0p1  18238  mulgnn0subcl  18240  mulgsubcl  18241  mulgneg  18245  mulgz  18254  mulgnn0dir  18256  mulgdirlem  18257  mulgdir  18258  submmulg  18270  ghmmulg  18369  odid  18665  oddvds  18674  dfod2  18690  gexid  18705  gexdvds  18708  mulgnn0di  18945  mulgdi  18946  gsumzsplit  19046  2nsgsimpgd  19223  prmgrpsimpgd  19235  lsppratlem5  19922  prmirred  20641  1stckgenlem  22160  qtoprest  22324  tgpmulg  22700  tsmssplit  22759  xblss2ps  23010  xblss2  23011  metustfbas  23166  nmoix  23337  nmoleub  23339  idnghm  23351  blcvx  23405  icccmp  23432  xrge0tsms  23441  metdstri  23458  nmoleub2lem  23717  rrxcph  23994  rrxdstprj1  24011  ivthle  24056  ivthle2  24057  dyadmbl  24200  volivth  24207  itg2const2  24341  itg2mulc  24347  dvlip2  24591  dvfsumlem1  24622  mdegmullem  24671  coemulhi  24843  dgrcolem2  24863  coseq00topi  25087  abssinper  25105  cxplea  25278  cxple2  25279  cxple2a  25281  cxpcn3  25328  cxpaddlelem  25331  cxpaddle  25332  ang180lem3  25388  dcubic2  25421  birthdaylem2  25529  jensen  25565  ppiltx  25753  chtub  25787  bcmono  25852  bcmax  25853  bpos  25868  lgseisenlem1  25950  2sqlem4  25996  2sqmod  26011  pntrlog2bndlem5  26156  pntpbnd1  26161  tgldimor  26287  tgifscgr  26293  tgcgrxfr  26303  tgbtwnconn1  26360  tgbtwnconn2  26361  tgbtwnconn3  26362  tgbtwnconnln3  26363  tgbtwnconn22  26364  tgbtwnconnln1  26365  tgbtwnconnln2  26366  legtrid  26376  legbtwn  26379  tgcgrsub2  26380  legov3  26383  hlln  26392  hltr  26395  btwnhl  26399  ncolncol  26431  mirconn  26463  krippen  26476  midexlem  26477  midex  26522  opphllem2  26533  opphllem5  26536  opphllem6  26537  outpasch  26540  hlpasch  26541  trgcopyeulem  26590  cgrahl  26612  cgracol  26613  ex-natded5.7  28189  ex-natded5.13  28193  ex-natded9.20  28195  ex-natded9.20-2  28196  suppovss  30425  xrge0infss  30483  xnn0gt0  30493  nn0xmulclb  30495  difioo  30504  iundisjcnt  30520  f1ocnt  30524  hashxpe  30528  xrsmulgzz  30665  ressmulgnn0  30671  xrge0addgt0  30678  xrge0adddir  30679  xrge0tsmsd  30692  tocyc01  30760  cycpmco2lem4  30771  cycpmco2lem7  30774  cycpmco2  30775  cyc3co2  30782  cycpmrn  30785  archirngz  30818  archiabllem2a  30823  ssmxidllem  30978  lindsun  31021  lbsdiflsp0  31022  submateq  31074  lmat22lem  31082  locfinref  31105  xrge0mulc1cn  31184  qqhval2lem  31222  nexple  31268  esumpcvgval  31337  esumcvg  31345  sigaclcu3  31381  measiuns  31476  voliune  31488  volfiniune  31489  volmeas  31490  sgncl  31796  sgnmul  31800  gsumnunsn  31811  signsply0  31821  signswch  31831  signslema  31832  signstfvneq0  31842  chtvalz  31900  bnj517  32157  bnj1408  32308  bnj1423  32323  bnj1452  32324  noetalem3  33219  dnibndlem13  33829  dnibnd  33830  poimirlem2  34893  fdc  35019  orel  35379  lsatcvat  36185  lkrpssN  36298  2at0mat0  36660  atmod1i1m  36993  lhp2at0nle  37170  trlcone  37863  tendoex  38110  dihlspsnssN  38467  dochkrsm  38593  lcfl8  38637  lclkrlem2b  38643  lclkrlem2s  38660  lcfrlem21  38698  mapdval2N  38765  mapdspex  38803  pell1qrgaplem  39468  monotoddzzfi  39537  oddcomabszz  39539  zindbi  39541  rmxnn  39546  jm2.24  39558  acongeq  39578  jm2.23  39591  jm2.26lem3  39596  wepwsolem  39640  frege102d  40097  fnchoice  41284  refsum2cnlem1  41292  wallispilem3  42351  wtgoldbnnsum4prm  43966  bgoldbnnsum3prm  43968  nn0sumshdiglem1  44680