Theorem mpjaodan 944

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

Syntax hints:   → wi 4   ∧ wa 386   ∨ wo 836

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 199  df-an 387  df-or 837

This theorem is referenced by:  mpjao3dan  1505  weniso  6876  isf32lem2  9511  isf32lem4  9513  fpwwe2lem11  9797  fpwwe2lem12  9798  lecasei  10482  ltlecasei  10484  xaddass  12391  xlesubadd  12405  xmulge0  12426  xadddi2  12439  xrsupss  12451  xrinfmss  12452  fzm1  12738  seqf1olem2  13159  expaddzlem  13221  discr  13320  fzomaxdif  14490  iseralt  14823  sumrb  14851  telfsumo  14938  fsumparts  14942  ntrivcvgtail  15035  prodrb  15065  bitsf1  15574  smupvallem  15611  eucalgf  15702  eucalginv  15703  vdwmc2  16087  mreexmrid  16689  mreexexlem3d  16692  mulgnn0p1  17939  mulgnn0subcl  17941  mulgsubcl  17942  mulgneg  17946  mulgz  17954  mulgnn0dir  17956  mulgdirlem  17957  mulgdir  17958  submmulg  17970  ghmmulg  18056  odid  18341  oddvds  18350  dfod2  18365  gexid  18380  gexdvds  18383  mulgnn0di  18617  mulgdi  18618  gsumzsplit  18713  lsppratlem5  19548  prmirred  20239  1stckgenlem  21765  qtoprest  21929  tgpmulg  22305  tsmssplit  22363  xblss2ps  22614  xblss2  22615  metustfbas  22770  nmoix  22941  nmoleub  22943  idnghm  22955  blcvx  23009  icccmp  23036  xrge0tsms  23045  metdstri  23062  nmoleub2lem  23321  rrxcph  23598  rrxdstprj1  23615  ivthle  23660  ivthle2  23661  dyadmbl  23804  volivth  23811  itg2const2  23945  itg2mulc  23951  dvlip2  24195  dvfsumlem1  24226  mdegmullem  24275  coemulhi  24447  dgrcolem2  24467  coseq00topi  24692  abssinper  24708  cxplea  24879  cxple2  24880  cxple2a  24882  cxpcn3  24929  cxpaddlelem  24932  cxpaddle  24933  ang180lem3  24989  dcubic2  25022  birthdaylem2  25131  jensen  25167  ppiltx  25355  chtub  25389  bcmono  25454  bcmax  25455  bpos  25470  lgseisenlem1  25552  2sqlem4  25598  pntrlog2bndlem5  25722  pntpbnd1  25727  tgldimor  25853  tgifscgr  25859  tgcgrxfr  25869  tgbtwnconn1  25926  tgbtwnconn2  25927  tgbtwnconn3  25928  tgbtwnconnln3  25929  tgbtwnconn22  25930  tgbtwnconnln1  25931  tgbtwnconnln2  25932  legtrid  25942  legbtwn  25945  tgcgrsub2  25946  legov3  25949  hlln  25958  hltr  25961  btwnhl  25965  ncolncol  25997  mirconn  26029  krippen  26042  midexlem  26043  midex  26085  opphllem2  26096  opphllem5  26099  opphllem6  26100  outpasch  26103  hlpasch  26104  trgcopyeulem  26153  cgrahl  26175  cgracol  26176  ex-natded5.7  27843  ex-natded5.13  27847  ex-natded9.20  27849  ex-natded9.20-2  27850  xrge0infss  30090  difioo  30108  iundisjcnt  30121  f1ocnt  30123  2sqmod  30210  xrsmulgzz  30240  ressmulgnn0  30246  xrge0addgt0  30253  xrge0adddir  30254  archirngz  30305  archiabllem2a  30310  xrge0tsmsd  30347  lindsun  30439  lbsdiflsp0  30440  submateq  30473  lmat22lem  30481  locfinref  30506  xrge0mulc1cn  30585  qqhval2lem  30623  nexple  30669  esumpcvgval  30738  esumcvg  30746  sigaclcu3  30783  measiuns  30878  voliune  30890  volfiniune  30891  volmeas  30892  sgncl  31199  sgnmul  31203  gsumnunsn  31214  signsply0  31228  signswch  31238  signslema  31239  signstfvneq0  31250  chtvalz  31309  bnj517  31554  bnj1408  31703  bnj1423  31718  bnj1452  31719  noetalem3  32454  dnibndlem13  33063  dnibnd  33064  poimirlem2  34021  fdc  34149  orel  34511  lsatcvat  35188  lkrpssN  35301  2at0mat0  35663  atmod1i1m  35996  lhp2at0nle  36173  trlcone  36866  tendoex  37113  dihlspsnssN  37470  dochkrsm  37596  lcfl8  37640  lclkrlem2b  37646  lclkrlem2s  37663  lcfrlem21  37701  mapdval2N  37768  mapdspex  37806  pell1qrgaplem  38379  monotoddzzfi  38448  oddcomabszz  38450  zindbi  38452  rmxnn  38459  jm2.24  38471  acongeq  38491  jm2.23  38504  jm2.26lem3  38509  wepwsolem  38553  frege102d  38985  fnchoice  40103  refsum2cnlem1  40111  wallispilem3  41193  wtgoldbnnsum4prm  42697  bgoldbnnsum3prm  42699  nn0sumshdiglem1  43412