Theorem mpjaodan 810

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

Syntax hints:   → wi 4   ∧ wa 104   ∨ wo 720

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjao3dan  1348  dcun  3637  ifcldadc  3670  ifeq1dadc  3671  ifeq2dadc  3672  ifeqdadc  3673  ifbothdadc  3674  ifcldcd  3678  2if2dc  3680  ifeqeqxdc  3687  exmidn0m  4336  exmidsssn  4337  exmidundif  4341  exmidundifim  4342  ordtri2or2exmidlem  4671  reg2exmidlema  4679  nnpredcl  4768  frecabcl  6664  nnsucuniel  6762  dcdifsnid  6771  pw2f1odclem  7128  phpm  7161  fidifsnen  7166  dif1enen  7178  fin0  7183  fimax2gtrilemstep  7199  finexdc  7201  elssdc  7203  eqsndc  7204  en2eqpr  7208  fientri3  7216  unsnfidcex  7221  unsnfidcel  7222  undifdcss  7224  prfidceq  7229  tpfidceq  7231  fiintim  7232  ssfirab  7238  fidcenumlemrks  7264  fidcenumlemr  7266  2omap  7312  omp1eomlem  7428  difinfsnlem  7433  difinfsn  7434  ctssdccl  7445  ctssdc  7447  enumct  7449  nninfninc  7457  nnnninf  7460  nnnninfeq  7462  nnnninfeq2  7463  nninfisol  7467  finomni  7474  ismkvnex  7489  nninfwlpoimlemg  7509  pr2cv1  7535  exmidfodomrlemeldju  7545  exmidfodomrlemreseldju  7546  exmidfodomrlemr  7548  exmidfodomrlemrALT  7549  exmidaclem  7558  exmidontriimlem3  7573  netap  7614  2omotaplemap  7617  mullocprlem  7931  recexprlemloc  7992  suplocsrlem  8169  btwnapz  9759  xnn0dcle  10187  xnn0letri  10188  z2ge  10211  xaddcom  10246  xnegdi  10253  xaddass  10254  xpncan  10256  xleadd1a  10258  xsubge0  10266  xlesubadd  10268  fztri3or  10426  fzm1  10490  fzneuz  10491  exfzdc  10642  zsupcllemstep  10645  infssuzex  10649  exbtwnzlemstep  10665  rebtwn2zlemstep  10670  xqltnle  10685  apbtwnz  10692  modifeq2int  10806  modsumfzodifsn  10816  iseqf1olemab  10922  iseqf1olemmo  10925  seq3f1olemqsumk  10932  seq3f1olemqsum  10933  seq3f1olemstep  10934  seqf1oglem1  10939  seqf1oglem2  10940  fser0const  10955  expaddzaplem  11002  qsqeqor  11070  resq01  11078  expnbnd  11084  nn0ltexp2  11130  apexp1  11139  bcval  11170  bccmpl  11175  bcval5  11184  bcpasc  11187  bccl  11188  hashennnuni  11201  hashnncl  11217  fiubm  11254  hashfibc  11266  hashf1  11270  zfz1isolemiso  11274  lswex  11339  ccatsymb  11353  ccat1st1st  11392  fzowrddc  11402  swrd0g  11415  swrdsbslen  11421  swrdspsleq  11422  pfxclz  11434  pfxwrdsymbg  11445  swrdccatin1  11480  resqrexlemnm  11767  resqrexlemcvg  11768  resqrexlemoverl  11770  resqrexlemglsq  11771  leabs  11823  nn0abscl  11834  ltabs  11836  abslt  11837  fzomaxdif  11862  maxleim  11954  maxabslemval  11957  zmaxcl  11973  2zsupmax  11975  minmax  11979  2zinfmin  11992  xrmaxleim  11993  xrmaxifle  11995  xrmaxiflemab  11996  xrmaxiflemlub  11997  xrmaxiflemcom  11998  xrmaxiflemval  11999  xrmaxaddlem  12009  xrmaxadd  12010  xrminmax  12014  sumdc  12107  fzf1o  12125  sumrbdc  12129  summodclem3  12130  summodclem2a  12131  zsumdc  12134  isumss  12141  fisumss  12142  isumss2  12143  fsumcllem  12149  fsumadd  12156  fsumsplit  12157  fsumsplitsn  12160  sumsplitdc  12182  fisumrev2  12196  fsummulc2  12198  telfsumo  12216  fsumparts  12220  cvgratnnlemseq  12276  cvgratz  12282  fproddccvg  12322  prodrbdc  12324  zproddc  12329  prod1dc  12336  fprodssdc  12340  fprodmul  12341  fprodsplitdc  12346  fprodsplit  12347  fprodunsn  12354  fprodcllem  12356  sinltxirr  12511  fsumdvds  12592  dvdsle  12594  mod2eq1n2dvds  12629  bitsmod  12706  gcdsupex  12717  gcdsupcl  12718  gcdval  12719  gcddvds  12723  gcdcl  12726  gcd0id  12739  gcdneg  12742  bezoutlemmain  12758  bezoutlemzz  12762  bezoutlemaz  12763  bezoutlembz  12764  dfgcd3  12770  dfgcd2  12774  nninfctlemfo  12800  nn0seqcvgd  12802  eucalgf  12816  eucalginv  12817  dvdslcm  12830  lcmcl  12833  lcmneg  12835  lcmgcd  12839  lcmdvds  12840  lcmid  12841  mulgcddvds  12855  isprm5lem  12902  pw2dvdslemn  12926  sqrt2irrap  12941  phibndlem  12977  prm23ge5  13026  pclemdc  13050  pcxqcl  13074  pcge0  13075  pcdvdsb  13082  pceq0  13084  pcneg  13087  pcdvdstr  13089  pcgcd1  13090  pcgcd  13091  pc2dvds  13092  pcz  13094  pcprmpw2  13095  pcaddlem  13101  pcadd  13102  pcmpt  13105  pcmpt2  13106  pcprod  13108  fldivp1  13110  qexpz  13114  1arithlem4  13128  1arith  13129  4sqlem19  13171  ennnfonelemss  13284  ennnfonelemkh  13286  ennnfonelemhf1o  13287  ctiunctlemudc  13311  bassetsnn  13392  fvprif  13647  gzsumwsubmcl  13784  gzsumwmhm  13786  gzsumcl  13787  mulgnn0p1  13919  mulgnn0subcl  13921  mulgsubcl  13922  mulgneg  13926  mulgz  13936  mulgnn0dir  13938  mulgdirlem  13939  mulgdir  13940  submmulg  13952  ghmmulg  14042  gzsumreidx  14124  gzsumsubmcl  14125  gzsummhm  14128  gzsumsplit0  14131  gsumvalfi  14135  gzsumgsum  14138  lringuplu  14486  aprlring  14583  znf1o  14969  xblss2ps  15488  xblss2  15489  qtopbas  15606  dedekindeulemeu  15706  dedekindeu  15707  suplociccreex  15708  dedekindicclemeu  15715  dedekindicclemicc  15716  limcimolemlt  15748  cnplimclemle  15752  dvmptc  15801  reeff1o  15857  efltlemlt  15858  sin0pilem2  15866  coseq0negpitopi  15920  abssinper  15930  cos02pilt1  15935  logbgcd1irraplemexp  16053  birthdaylem2  16071  birthdaylem3  16072  lgslem4  16105  lgsneg  16126  lgsneg1  16127  lgsmod  16128  lgsdilem  16129  lgsdir2  16135  lgsdirprm  16136  lgsdir  16137  lgsdi  16139  lgsne0  16140  lgsdirnn0  16149  lgsdinn0  16150  gausslemma2dlem1a  16160  gausslemma2dlem1f1o  16162  gausslemma2dlem4  16166  lgseisenlem1  16172  lgsquad3  16186  2sqlem4  16220  2sqlem9  16226  eupth2lem3lem3fi  16694  eupth2lem3lem4fi  16697  eupth2lem3lem7fi  16698  dichmul0orlem3  16738  dichmul0orlem7  16742  nnsf  17022  nninfsellemsuc  17029  nnnninfex  17039  trilpolemclim  17059  trilpolemisumle  17061  trilpolemeq1  17063  trilpolemlt1  17064  trirec0  17067  apdifflemf  17069  apdifflemr  17070  apdiff  17071  iswomni0  17075  nconstwlpolemgt0  17088  nconstwlpolem  17089  neapmkvlem  17091