Theorem mpjaodan 966

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

Syntax hints:   → wi 4   ∧ wa 396   ∨ wo 853

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 208  df-an 397  df-or 854

This theorem is referenced by:  onunel  6424  weniso  7305  isf32lem2  10274  isf32lem4  10276  fpwwe2lem10  10561  fpwwe2lem11  10562  lecasei  11250  ltlecasei  11252  xaddass  13199  xlesubadd  13213  xmulge0  13234  xadddi2  13247  xrsupss  13259  xrinfmss  13260  fzm1  13559  seqf1olem2  14002  expaddzlem  14065  discr  14200  fzomaxdif  15304  iseralt  15645  sumrb  15673  telfsumo  15763  fsumparts  15767  ntrivcvgtail  15863  prodrb  15895  bitsf1  16413  smupvallem  16450  eucalgf  16550  eucalginv  16551  vdwmc2  16948  fvprif  17523  mreexmrid  17607  mreexexlem3d  17610  chnub  18586  chnccats1  18589  chnccat  18590  mulgfval  19043  ressmulgnn0  19051  mulgnn0p1  19059  mulgnn0subcl  19061  mulgsubcl  19062  mulgneg  19066  mulgz  19076  mulgnn0dir  19078  mulgdirlem  19079  mulgdir  19080  submmulg  19092  ghmmulg  19201  odid  19511  oddvds  19520  dfod2  19537  gexid  19554  gexdvds  19557  mulgnn0di  19798  mulgdi  19799  gsumzsplit  19900  2nsgsimpgd  20077  prmgrpsimpgd  20089  lringuplu  20523  lsppratlem5  21151  prmirred  21456  mhpmulcl  22144  1stckgenlem  23543  qtoprest  23707  tgpmulg  24083  tsmssplit  24142  xblss2ps  24391  xblss2  24392  metustfbas  24547  nmoix  24719  nmoleub  24721  idnghm  24733  blcvx  24788  icccmp  24816  xrge0tsms  24825  metdstri  24842  nmoleub2lem  25106  rrxcph  25384  rrxdstprj1  25401  ivthle  25448  ivthle2  25449  dyadmbl  25592  volivth  25599  itg2const2  25733  itg2mulc  25739  dvlip2  25987  dvfsumlem1  26018  mdegmullem  26068  coemulhi  26244  dgrcolem2  26264  coseq00topi  26491  abssinper  26510  cxplea  26685  cxple2  26686  cxple2a  26688  cxpcn3  26737  cxpaddlelem  26740  cxpaddle  26741  ang180lem3  26800  dcubic2  26833  birthdaylem2  26941  jensen  26977  ppiltx  27165  chtub  27200  bcmono  27265  bcmax  27266  bpos  27281  lgseisenlem1  27363  2sqlem4  27409  2sqmod  27424  pntrlog2bndlem5  27569  pntpbnd1  27574  noinfbnd2lem1  27719  noetasuplem4  27725  noetainflem4  27729  mulsproplem12  28144  mulsproplem13  28145  mulsproplem14  28146  lemulsd  28155  mulsge0d  28163  mulscan2d  28196  lemuls1ad  28199  absmuls  28261  absnegs  28264  leabss  28265  tgldimor  28595  tgifscgr  28601  tgcgrxfr  28611  tgbtwnconn1  28668  tgbtwnconn2  28669  tgbtwnconn3  28670  tgbtwnconnln3  28671  tgbtwnconn22  28672  tgbtwnconnln1  28673  tgbtwnconnln2  28674  legtrid  28684  legbtwn  28687  tgcgrsub2  28688  legov3  28691  hlln  28700  hltr  28703  btwnhl  28707  ncolncol  28739  mirconn  28771  krippen  28784  midexlem  28785  midex  28830  opphllem2  28841  opphllem5  28844  opphllem6  28845  outpasch  28848  hlpasch  28849  trgcopyeulem  28898  cgrahl  28920  cgracol  28921  ex-natded5.7  30506  ex-natded5.13  30510  ex-natded9.20  30512  ex-natded9.20-2  30513  fconst7v  32719  suppovss  32780  nn0mnfxrd  32850  xrge0infss  32859  xnn0gt0  32868  nn0xmulclb  32870  difioo  32881  iundisjcnt  32897  f1ocnt  32899  fzo0opth  32902  hashxpe  32906  sgncl  32930  sgnmul  32934  nexple  32943  2exple2exp  32944  ccatws1f1o  33037  xrsmulgzz  33095  xrge0addgt0  33103  xrge0adddir  33104  ressmulgnn0d  33132  xrge0tsmsd  33161  gsumwun  33164  tocyc01  33206  cycpmco2lem4  33217  cycpmco2lem7  33220  cycpmco2  33221  cyc3co2  33228  cycpmrn  33231  archirngz  33277  archiabllem2a  33282  elrgspnlem2  33331  ssdifidllem  33546  ssmxidllem  33563  rprmirred  33621  rprmdvdspow  33623  1arithufdlem3  33636  dfufd2lem  33639  ply1dg3rt0irred  33674  esplyfval1  33764  lindsun  33816  lbsdiflsp0  33817  fldextrspunlsplem  33864  constrmon  33935  constrconj  33936  constrfin  33937  constrelextdg2  33938  constrextdg2lem  33939  zconstr  33955  submateq  34000  lmat22lem  34008  locfinref  34032  xrge0mulc1cn  34132  zrhcntr  34170  qqhval2lem  34172  esumpcvgval  34269  esumcvg  34277  sigaclcu3  34313  measiuns  34408  voliune  34420  volfiniune  34421  volmeas  34422  gsumnunsn  34732  signsply0  34742  signswch  34752  signslema  34753  signstfvneq0  34763  chtvalz  34820  bnj517  35074  bnj1408  35225  bnj1423  35240  bnj1452  35241  weiunse  36703  dnibndlem13  36803  dnibnd  36804  irrdifflemf  37692  poimirlem2  37996  fdc  38119  orel  38476  lsatcvat  39549  lkrpssN  39662  2at0mat0  40024  atmod1i1m  40357  lhp2at0nle  40534  trlcone  41227  tendoex  41474  dihlspsnssN  41831  dochkrsm  41957  lcfl8  42001  lclkrlem2b  42007  lclkrlem2s  42024  lcfrlem21  42062  mapdval2N  42129  mapdspex  42167  aks4d1p5  42572  hashnexinjle  42621  sticksstones12a  42649  sticksstones13  42651  sn-msqgt0d  42983  fimgmcyclem  43026  fsuppind  43047  flt4lem7  43116  nna4b4nsq  43117  pell1qrgaplem  43325  monotoddzzfi  43394  oddcomabszz  43396  zindbi  43398  rmxnn  43403  jm2.24  43415  acongeq  43435  jm2.23  43448  jm2.26lem3  43453  wepwsolem  43494  oe0rif  43737  onmcl  43783  omabs2  43784  omcl2  43785  onsucunipr  43824  oaun3lem1  43826  fzuntgd  43909  frege102d  44205  fnchoice  45484  refsum2cnlem1  45492  wallispilem3  46517  chnsubseqwl  47331  squeezedltsq  47340  wtgoldbnnsum4prm  48300  bgoldbnnsum3prm  48302  nn0sumshdiglem1  49119  mofeu  49345  toslat  49479  2arwcatlem2  50093  2arwcatlem3  50094  2arwcatlem4  50095  2arwcatlem5  50096  2arwcat  50097