Theorem mpjaodan 806

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 805	. 2 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)
5	1, 4	mpdan 421	1 ⊢ (𝜑 → 𝜒)

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

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjao3dan  1344  dcun  3623  ifcldadc  3656  ifeq1dadc  3657  ifeq2dadc  3658  ifeqdadc  3659  ifbothdadc  3660  ifcldcd  3664  2if2dc  3666  ifeqeqxdc  3673  exmidn0m  4319  exmidsssn  4320  exmidundif  4324  exmidundifim  4325  ordtri2or2exmidlem  4653  reg2exmidlema  4661  nnpredcl  4750  frecabcl  6643  nnsucuniel  6741  dcdifsnid  6750  pw2f1odclem  7100  phpm  7133  fidifsnen  7138  dif1enen  7150  fin0  7155  fimax2gtrilemstep  7171  finexdc  7173  elssdc  7175  eqsndc  7176  en2eqpr  7180  fientri3  7188  unsnfidcex  7193  unsnfidcel  7194  undifdcss  7196  prfidceq  7201  tpfidceq  7203  fiintim  7204  ssfirab  7210  fidcenumlemrks  7236  fidcenumlemr  7238  2omap  7282  omp1eomlem  7398  difinfsnlem  7403  difinfsn  7404  ctssdccl  7415  ctssdc  7417  enumct  7419  nninfninc  7427  nnnninf  7430  nnnninfeq  7432  nnnninfeq2  7433  nninfisol  7437  finomni  7444  ismkvnex  7459  nninfwlpoimlemg  7479  pr2cv1  7505  exmidfodomrlemeldju  7515  exmidfodomrlemreseldju  7516  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  exmidaclem  7528  exmidontriimlem3  7543  netap  7584  2omotaplemap  7587  mullocprlem  7901  recexprlemloc  7962  suplocsrlem  8139  btwnapz  9726  xnn0dcle  10154  xnn0letri  10155  z2ge  10178  xaddcom  10213  xnegdi  10220  xaddass  10221  xpncan  10223  xleadd1a  10225  xsubge0  10233  xlesubadd  10235  fztri3or  10393  fzm1  10456  fzneuz  10457  exfzdc  10608  zsupcllemstep  10611  infssuzex  10615  exbtwnzlemstep  10631  rebtwn2zlemstep  10636  xqltnle  10651  apbtwnz  10658  modifeq2int  10772  modsumfzodifsn  10782  iseqf1olemab  10888  iseqf1olemmo  10891  seq3f1olemqsumk  10898  seq3f1olemqsum  10899  seq3f1olemstep  10900  seqf1oglem1  10905  seqf1oglem2  10906  fser0const  10921  expaddzaplem  10968  qsqeqor  11036  resq01  11044  expnbnd  11050  nn0ltexp2  11096  apexp1  11105  bcval  11136  bccmpl  11141  bcval5  11150  bcpasc  11153  bccl  11154  hashennnuni  11167  hashnncl  11183  fiubm  11220  hashfibc  11232  zfz1isolemiso  11236  lswex  11301  ccatsymb  11315  ccat1st1st  11354  fzowrddc  11364  swrd0g  11377  swrdsbslen  11383  swrdspsleq  11384  pfxclz  11396  pfxwrdsymbg  11407  swrdccatin1  11442  resqrexlemnm  11728  resqrexlemcvg  11729  resqrexlemoverl  11731  resqrexlemglsq  11732  leabs  11784  nn0abscl  11795  ltabs  11797  abslt  11798  fzomaxdif  11823  maxleim  11915  maxabslemval  11918  zmaxcl  11934  2zsupmax  11936  minmax  11940  2zinfmin  11953  xrmaxleim  11954  xrmaxifle  11956  xrmaxiflemab  11957  xrmaxiflemlub  11958  xrmaxiflemcom  11959  xrmaxiflemval  11960  xrmaxaddlem  11970  xrmaxadd  11971  xrminmax  11975  sumdc  12068  fzf1o  12086  sumrbdc  12090  summodclem3  12091  summodclem2a  12092  zsumdc  12095  isumss  12102  fisumss  12103  isumss2  12104  fsumcllem  12110  fsumadd  12117  fsumsplit  12118  fsumsplitsn  12121  sumsplitdc  12143  fisumrev2  12157  fsummulc2  12159  telfsumo  12177  fsumparts  12181  cvgratnnlemseq  12237  cvgratz  12243  fproddccvg  12283  prodrbdc  12285  zproddc  12290  prod1dc  12297  fprodssdc  12301  fprodmul  12302  fprodsplitdc  12307  fprodsplit  12308  fprodunsn  12315  fprodcllem  12317  sinltxirr  12472  fsumdvds  12553  dvdsle  12555  mod2eq1n2dvds  12590  bitsmod  12667  gcdsupex  12678  gcdsupcl  12679  gcdval  12680  gcddvds  12684  gcdcl  12687  gcd0id  12700  gcdneg  12703  bezoutlemmain  12719  bezoutlemzz  12723  bezoutlemaz  12724  bezoutlembz  12725  dfgcd3  12731  dfgcd2  12735  nninfctlemfo  12761  nn0seqcvgd  12763  eucalgf  12777  eucalginv  12778  dvdslcm  12791  lcmcl  12794  lcmneg  12796  lcmgcd  12800  lcmdvds  12801  lcmid  12802  mulgcddvds  12816  isprm5lem  12863  pw2dvdslemn  12887  sqrt2irrap  12902  phibndlem  12938  prm23ge5  12987  pclemdc  13011  pcxqcl  13035  pcge0  13036  pcdvdsb  13043  pceq0  13045  pcneg  13048  pcdvdstr  13050  pcgcd1  13051  pcgcd  13052  pc2dvds  13053  pcz  13055  pcprmpw2  13056  pcaddlem  13062  pcadd  13063  pcmpt  13066  pcmpt2  13067  pcprod  13069  fldivp1  13071  qexpz  13075  1arithlem4  13089  1arith  13090  4sqlem19  13132  ennnfonelemss  13245  ennnfonelemkh  13247  ennnfonelemhf1o  13248  ctiunctlemudc  13272  bassetsnn  13353  fvprif  13640  gsumfzz  13792  gsumwsubmcl  13793  gsumwmhm  13795  gsumfzcl  13796  mulgnn0p1  13934  mulgnn0subcl  13936  mulgsubcl  13937  mulgneg  13941  mulgz  13951  mulgnn0dir  13953  mulgdirlem  13954  mulgdir  13955  submmulg  13967  ghmmulg  14057  gsumfzreidx  14138  gsumfzsubmcl  14139  gsumfzmptfidmadd  14140  gsumfzmhm  14144  gsumsplit0  14147  lringuplu  14426  aprlring  14523  gsumfzfsum  14848  znf1o  14911  xblss2ps  15381  xblss2  15382  qtopbas  15499  dedekindeulemeu  15599  dedekindeu  15600  suplociccreex  15601  dedekindicclemeu  15608  dedekindicclemicc  15609  limcimolemlt  15641  cnplimclemle  15645  dvmptc  15694  reeff1o  15750  efltlemlt  15751  sin0pilem2  15759  coseq0negpitopi  15813  abssinper  15823  cos02pilt1  15828  logbgcd1irraplemexp  15945  lgslem4  15988  lgsneg  16009  lgsneg1  16010  lgsmod  16011  lgsdilem  16012  lgsdir2  16018  lgsdirprm  16019  lgsdir  16020  lgsdi  16022  lgsne0  16023  lgsdirnn0  16032  lgsdinn0  16033  gausslemma2dlem1a  16043  gausslemma2dlem1f1o  16045  gausslemma2dlem4  16049  lgseisenlem1  16055  lgsquad3  16069  2sqlem4  16103  2sqlem9  16109  eupth2lem3lem3fi  16577  eupth2lem3lem4fi  16580  eupth2lem3lem7fi  16581  nnsf  16895  nninfsellemsuc  16902  nnnninfex  16912  trilpolemclim  16932  trilpolemisumle  16934  trilpolemeq1  16936  trilpolemlt1  16937  trirec0  16940  apdifflemf  16942  apdifflemr  16943  apdiff  16944  iswomni0  16948  trimul0or  16957  nconstwlpolemgt0  16962  nconstwlpolem  16963  neapmkvlem  16965  gfsumval  16974  gsumgfsum  16978