Theorem mpjaodan 961

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

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

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 849

This theorem is referenced by:  onunel  6489  weniso  7374  isf32lem2  10394  isf32lem4  10396  fpwwe2lem10  10680  fpwwe2lem11  10681  lecasei  11367  ltlecasei  11369  xaddass  13291  xlesubadd  13305  xmulge0  13326  xadddi2  13339  xrsupss  13351  xrinfmss  13352  fzm1  13647  seqf1olem2  14083  expaddzlem  14146  discr  14279  fzomaxdif  15382  iseralt  15721  sumrb  15749  telfsumo  15838  fsumparts  15842  ntrivcvgtail  15936  prodrb  15968  bitsf1  16483  smupvallem  16520  eucalgf  16620  eucalginv  16621  vdwmc2  17017  fvprif  17606  mreexmrid  17686  mreexexlem3d  17689  mulgfval  19087  ressmulgnn0  19095  mulgnn0p1  19103  mulgnn0subcl  19105  mulgsubcl  19106  mulgneg  19110  mulgz  19120  mulgnn0dir  19122  mulgdirlem  19123  mulgdir  19124  submmulg  19136  ghmmulg  19246  odid  19556  oddvds  19565  dfod2  19582  gexid  19599  gexdvds  19602  mulgnn0di  19843  mulgdi  19844  gsumzsplit  19945  2nsgsimpgd  20122  prmgrpsimpgd  20134  lringuplu  20544  lsppratlem5  21153  prmirred  21485  mhpmulcl  22153  1stckgenlem  23561  qtoprest  23725  tgpmulg  24101  tsmssplit  24160  xblss2ps  24411  xblss2  24412  metustfbas  24570  nmoix  24750  nmoleub  24752  idnghm  24764  blcvx  24819  icccmp  24847  xrge0tsms  24856  metdstri  24873  nmoleub2lem  25147  rrxcph  25426  rrxdstprj1  25443  ivthle  25491  ivthle2  25492  dyadmbl  25635  volivth  25642  itg2const2  25776  itg2mulc  25782  dvlip2  26034  dvfsumlem1  26066  mdegmullem  26117  coemulhi  26293  dgrcolem2  26314  coseq00topi  26544  abssinper  26563  cxplea  26738  cxple2  26739  cxple2a  26741  cxpcn3  26791  cxpaddlelem  26794  cxpaddle  26795  ang180lem3  26854  dcubic2  26887  birthdaylem2  26995  jensen  27032  ppiltx  27220  chtub  27256  bcmono  27321  bcmax  27322  bpos  27337  lgseisenlem1  27419  2sqlem4  27465  2sqmod  27480  pntrlog2bndlem5  27625  pntpbnd1  27630  noinfbnd2lem1  27775  noetasuplem4  27781  noetainflem4  27785  mulsproplem12  28153  mulsproplem13  28154  mulsproplem14  28155  slemuld  28164  mulsge0d  28172  mulscan2d  28205  slemul1ad  28208  absmuls  28268  abssneg  28271  sleabs  28272  tgldimor  28510  tgifscgr  28516  tgcgrxfr  28526  tgbtwnconn1  28583  tgbtwnconn2  28584  tgbtwnconn3  28585  tgbtwnconnln3  28586  tgbtwnconn22  28587  tgbtwnconnln1  28588  tgbtwnconnln2  28589  legtrid  28599  legbtwn  28602  tgcgrsub2  28603  legov3  28606  hlln  28615  hltr  28618  btwnhl  28622  ncolncol  28654  mirconn  28686  krippen  28699  midexlem  28700  midex  28745  opphllem2  28756  opphllem5  28759  opphllem6  28760  outpasch  28763  hlpasch  28764  trgcopyeulem  28813  cgrahl  28835  cgracol  28836  ex-natded5.7  30430  ex-natded5.13  30434  ex-natded9.20  30436  ex-natded9.20-2  30437  suppovss  32690  xrge0infss  32764  xnn0gt0  32773  nn0xmulclb  32775  difioo  32784  iundisjcnt  32800  f1ocnt  32804  fzo0opth  32807  hashxpe  32811  nexple  32833  2exple2exp  32834  ccatws1f1o  32936  chnub  33002  chnccats1  33005  xrsmulgzz  33011  xrge0addgt0  33022  xrge0adddir  33023  xrge0tsmsd  33065  gsumwun  33068  tocyc01  33138  cycpmco2lem4  33149  cycpmco2lem7  33152  cycpmco2  33153  cyc3co2  33160  cycpmrn  33163  archirngz  33196  archiabllem2a  33201  elrgspnlem2  33247  ssdifidllem  33484  ssmxidllem  33501  rprmirred  33559  rprmdvdspow  33561  1arithufdlem3  33574  dfufd2lem  33577  ply1dg3rt0irred  33607  lindsun  33676  lbsdiflsp0  33677  fldextrspunlsplem  33723  constrmon  33785  constrconj  33786  constrfin  33787  constrelextdg2  33788  constrextdg2lem  33789  submateq  33808  lmat22lem  33816  locfinref  33840  xrge0mulc1cn  33940  zrhcntr  33980  qqhval2lem  33982  esumpcvgval  34079  esumcvg  34087  sigaclcu3  34123  measiuns  34218  voliune  34230  volfiniune  34231  volmeas  34232  sgncl  34541  sgnmul  34545  gsumnunsn  34556  signsply0  34566  signswch  34576  signslema  34577  signstfvneq0  34587  chtvalz  34644  bnj517  34899  bnj1408  35050  bnj1423  35065  bnj1452  35066  weiunse  36469  dnibndlem13  36491  dnibnd  36492  irrdifflemf  37326  poimirlem2  37629  fdc  37752  orel  38109  lsatcvat  39051  lkrpssN  39164  2at0mat0  39527  atmod1i1m  39860  lhp2at0nle  40037  trlcone  40730  tendoex  40977  dihlspsnssN  41334  dochkrsm  41460  lcfl8  41504  lclkrlem2b  41510  lclkrlem2s  41527  lcfrlem21  41565  mapdval2N  41632  mapdspex  41670  aks4d1p5  42081  hashnexinjle  42130  sticksstones12a  42158  sticksstones13  42160  fimgmcyclem  42543  fsuppind  42600  flt4lem7  42669  nna4b4nsq  42670  pell1qrgaplem  42884  monotoddzzfi  42954  oddcomabszz  42956  zindbi  42958  rmxnn  42963  jm2.24  42975  acongeq  42995  jm2.23  43008  jm2.26lem3  43013  wepwsolem  43054  oe0rif  43298  onmcl  43344  omabs2  43345  omcl2  43346  onsucunipr  43385  oaun3lem1  43387  fzuntgd  43471  frege102d  43767  fnchoice  45034  refsum2cnlem1  45042  wallispilem3  46082  wtgoldbnnsum4prm  47789  bgoldbnnsum3prm  47791  nn0sumshdiglem1  48542  mofeu  48757  toslat  48871