Theorem mpjaodan 960

Description: Eliminate a disjunction in a deduction. A translation of natural deduction rule ∨ E (∨ elimination), see natded 30381. (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  6413  weniso  7288  isf32lem2  10245  isf32lem4  10247  fpwwe2lem10  10531  fpwwe2lem11  10532  lecasei  11219  ltlecasei  11221  xaddass  13148  xlesubadd  13162  xmulge0  13183  xadddi2  13196  xrsupss  13208  xrinfmss  13209  fzm1  13507  seqf1olem2  13949  expaddzlem  14012  discr  14147  fzomaxdif  15251  iseralt  15592  sumrb  15620  telfsumo  15709  fsumparts  15713  ntrivcvgtail  15807  prodrb  15839  bitsf1  16357  smupvallem  16394  eucalgf  16494  eucalginv  16495  vdwmc2  16891  fvprif  17465  mreexmrid  17549  mreexexlem3d  17552  chnub  18528  chnccats1  18531  chnccat  18532  mulgfval  18982  ressmulgnn0  18990  mulgnn0p1  18998  mulgnn0subcl  19000  mulgsubcl  19001  mulgneg  19005  mulgz  19015  mulgnn0dir  19017  mulgdirlem  19018  mulgdir  19019  submmulg  19031  ghmmulg  19141  odid  19451  oddvds  19460  dfod2  19477  gexid  19494  gexdvds  19497  mulgnn0di  19738  mulgdi  19739  gsumzsplit  19840  2nsgsimpgd  20017  prmgrpsimpgd  20029  lringuplu  20460  lsppratlem5  21089  prmirred  21412  mhpmulcl  22065  1stckgenlem  23469  qtoprest  23633  tgpmulg  24009  tsmssplit  24068  xblss2ps  24317  xblss2  24318  metustfbas  24473  nmoix  24645  nmoleub  24647  idnghm  24659  blcvx  24714  icccmp  24742  xrge0tsms  24751  metdstri  24768  nmoleub2lem  25042  rrxcph  25320  rrxdstprj1  25337  ivthle  25385  ivthle2  25386  dyadmbl  25529  volivth  25536  itg2const2  25670  itg2mulc  25676  dvlip2  25928  dvfsumlem1  25960  mdegmullem  26011  coemulhi  26187  dgrcolem2  26208  coseq00topi  26439  abssinper  26458  cxplea  26633  cxple2  26634  cxple2a  26636  cxpcn3  26686  cxpaddlelem  26689  cxpaddle  26690  ang180lem3  26749  dcubic2  26782  birthdaylem2  26890  jensen  26927  ppiltx  27115  chtub  27151  bcmono  27216  bcmax  27217  bpos  27232  lgseisenlem1  27314  2sqlem4  27360  2sqmod  27375  pntrlog2bndlem5  27520  pntpbnd1  27525  noinfbnd2lem1  27670  noetasuplem4  27676  noetainflem4  27680  mulsproplem12  28067  mulsproplem13  28068  mulsproplem14  28069  slemuld  28078  mulsge0d  28086  mulscan2d  28119  slemul1ad  28122  absmuls  28183  abssneg  28186  sleabs  28187  tgldimor  28481  tgifscgr  28487  tgcgrxfr  28497  tgbtwnconn1  28554  tgbtwnconn2  28555  tgbtwnconn3  28556  tgbtwnconnln3  28557  tgbtwnconn22  28558  tgbtwnconnln1  28559  tgbtwnconnln2  28560  legtrid  28570  legbtwn  28573  tgcgrsub2  28574  legov3  28577  hlln  28586  hltr  28589  btwnhl  28593  ncolncol  28625  mirconn  28657  krippen  28670  midexlem  28671  midex  28716  opphllem2  28727  opphllem5  28730  opphllem6  28731  outpasch  28734  hlpasch  28735  trgcopyeulem  28784  cgrahl  28806  cgracol  28807  ex-natded5.7  30389  ex-natded5.13  30393  ex-natded9.20  30395  ex-natded9.20-2  30396  fconst7v  32601  suppovss  32660  xrge0infss  32741  xnn0gt0  32750  nn0xmulclb  32752  difioo  32763  iundisjcnt  32778  f1ocnt  32780  fzo0opth  32783  hashxpe  32787  sgncl  32812  sgnmul  32816  nexple  32825  2exple2exp  32826  ccatws1f1o  32930  xrsmulgzz  32988  xrge0addgt0  32996  xrge0adddir  32997  ressmulgnn0d  33023  xrge0tsmsd  33040  gsumwun  33043  tocyc01  33085  cycpmco2lem4  33096  cycpmco2lem7  33099  cycpmco2  33100  cyc3co2  33107  cycpmrn  33110  archirngz  33156  archiabllem2a  33161  elrgspnlem2  33208  ssdifidllem  33419  ssmxidllem  33436  rprmirred  33494  rprmdvdspow  33496  1arithufdlem3  33509  dfufd2lem  33512  ply1dg3rt0irred  33544  lindsun  33636  lbsdiflsp0  33637  fldextrspunlsplem  33684  constrmon  33755  constrconj  33756  constrfin  33757  constrelextdg2  33758  constrextdg2lem  33759  zconstr  33775  submateq  33820  lmat22lem  33828  locfinref  33852  xrge0mulc1cn  33952  zrhcntr  33990  qqhval2lem  33992  esumpcvgval  34089  esumcvg  34097  sigaclcu3  34133  measiuns  34228  voliune  34240  volfiniune  34241  volmeas  34242  gsumnunsn  34552  signsply0  34562  signswch  34572  signslema  34573  signstfvneq0  34583  chtvalz  34640  bnj517  34895  bnj1408  35046  bnj1423  35061  bnj1452  35062  weiunse  36508  dnibndlem13  36530  dnibnd  36531  irrdifflemf  37365  poimirlem2  37668  fdc  37791  orel  38148  lsatcvat  39095  lkrpssN  39208  2at0mat0  39570  atmod1i1m  39903  lhp2at0nle  40080  trlcone  40773  tendoex  41020  dihlspsnssN  41377  dochkrsm  41503  lcfl8  41547  lclkrlem2b  41553  lclkrlem2s  41570  lcfrlem21  41608  mapdval2N  41675  mapdspex  41713  aks4d1p5  42119  hashnexinjle  42168  sticksstones12a  42196  sticksstones13  42198  sn-msqgt0d  42525  fimgmcyclem  42572  fsuppind  42629  flt4lem7  42698  nna4b4nsq  42699  pell1qrgaplem  42912  monotoddzzfi  42981  oddcomabszz  42983  zindbi  42985  rmxnn  42990  jm2.24  43002  acongeq  43022  jm2.23  43035  jm2.26lem3  43040  wepwsolem  43081  oe0rif  43324  onmcl  43370  omabs2  43371  omcl2  43372  onsucunipr  43411  oaun3lem1  43413  fzuntgd  43497  frege102d  43793  fnchoice  45072  refsum2cnlem1  45080  wallispilem3  46111  squeezedltsq  46923  wtgoldbnnsum4prm  47839  bgoldbnnsum3prm  47841  nn0sumshdiglem1  48659  mofeu  48885  toslat  49019  2arwcatlem2  49634  2arwcatlem3  49635  2arwcatlem4  49636  2arwcatlem5  49637  2arwcat  49638