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 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  mpjao3dan  1348  dcun  3637  ifcldadc  3670  ifeq1dadc  3671  ifeq2dadc  3672  ifeqdadc  3673  ifbothdadc  3674  ifcldcd  3678  2if2dc  3680  ifeqeqxdc  3687  exmidn0m  4338  exmidsssn  4339  exmidundif  4343  exmidundifim  4344  ordtri2or2exmidlem  4673  reg2exmidlema  4681  nnpredcl  4770  frecabcl  6670  nnsucuniel  6768  dcdifsnid  6777  pw2f1odclem  7134  phpm  7167  fidifsnen  7172  dif1enen  7184  fin0  7189  fimax2gtrilemstep  7205  finexdc  7207  elssdc  7209  eqsndc  7210  en2eqpr  7214  fientri3  7222  unsnfidcex  7227  unsnfidcel  7228  undifdcss  7230  prfidceq  7235  tpfidceq  7237  fiintim  7238  ssfirab  7244  fidcenumlemrks  7270  fidcenumlemr  7272  2omap  7318  omp1eomlem  7434  difinfsnlem  7439  difinfsn  7440  ctssdccl  7451  ctssdc  7453  enumct  7455  nninfninc  7463  nnnninf  7466  nnnninfeq  7468  nnnninfeq2  7469  nninfisol  7473  finomni  7480  ismkvnex  7495  nninfwlpoimlemg  7515  pr2cv1  7541  exmidfodomrlemeldju  7551  exmidfodomrlemreseldju  7552  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  exmidaclem  7564  exmidontriimlem3  7579  netap  7620  2omotaplemap  7623  mullocprlem  7937  recexprlemloc  7998  suplocsrlem  8175  btwnapz  9778  xnn0dcle  10206  xnn0letri  10207  z2ge  10230  xaddcom  10265  xnegdi  10272  xaddass  10273  xpncan  10275  xleadd1a  10277  xsubge0  10285  xlesubadd  10287  fztri3or  10445  fzm1  10509  fzneuz  10510  exfzdc  10661  zsupcllemstep  10664  infssuzex  10668  exbtwnzlemstep  10684  rebtwn2zlemstep  10689  xqltnle  10704  apbtwnz  10711  modifeq2int  10825  modsumfzodifsn  10835  iseqf1olemab  10941  iseqf1olemmo  10944  seq3f1olemqsumk  10951  seq3f1olemqsum  10952  seq3f1olemstep  10953  seqf1oglem1  10958  seqf1oglem2  10959  fser0const  10974  expaddzaplem  11021  qsqeqor  11089  resq01  11097  expnbnd  11103  nn0ltexp2  11149  apexp1  11158  bcval  11189  bccmpl  11194  bcval5  11203  bcpasc  11206  bccl  11207  hashennnuni  11220  hashnncl  11236  fiubm  11273  hashfibc  11285  hashf1  11289  zfz1isolemiso  11293  lswex  11358  ccatsymb  11372  ccat1st1st  11411  fzowrddc  11421  swrd0g  11434  swrdsbslen  11440  swrdspsleq  11441  pfxclz  11453  pfxwrdsymbg  11464  swrdccatin1  11499  resqrexlemnm  11786  resqrexlemcvg  11787  resqrexlemoverl  11789  resqrexlemglsq  11790  leabs  11842  nn0abscl  11853  ltabs  11855  abslt  11856  fzomaxdif  11881  maxleim  11973  maxabslemval  11976  zmaxcl  11992  2zsupmax  11994  minmax  11998  2zinfmin  12011  xrmaxleim  12012  xrmaxifle  12014  xrmaxiflemab  12015  xrmaxiflemlub  12016  xrmaxiflemcom  12017  xrmaxiflemval  12018  xrmaxaddlem  12028  xrmaxadd  12029  xrminmax  12033  sumdc  12126  fzf1o  12144  sumrbdc  12148  summodclem3  12149  summodclem2a  12150  zsumdc  12153  isumss  12160  fisumss  12161  isumss2  12162  fsumcllem  12168  fsumadd  12175  fsumsplit  12176  fsumsplitsn  12179  sumsplitdc  12201  fisumrev2  12215  fsummulc2  12217  telfsumo  12235  fsumparts  12239  cvgratnnlemseq  12295  cvgratz  12301  fproddccvg  12341  prodrbdc  12343  zproddc  12348  prod1dc  12355  fprodssdc  12359  fprodmul  12360  fprodsplitdc  12365  fprodsplit  12366  fprodunsn  12373  fprodcllem  12375  sinltxirr  12530  fsumdvds  12611  dvdsle  12613  mod2eq1n2dvds  12648  bitsmod  12725  gcdsupex  12736  gcdsupcl  12737  gcdval  12738  gcddvds  12742  gcdcl  12745  gcd0id  12758  gcdneg  12761  bezoutlemmain  12777  bezoutlemzz  12781  bezoutlemaz  12782  bezoutlembz  12783  dfgcd3  12789  dfgcd2  12793  nninfctlemfo  12819  nn0seqcvgd  12821  eucalgf  12835  eucalginv  12836  dvdslcm  12849  lcmcl  12852  lcmneg  12854  lcmgcd  12858  lcmdvds  12859  lcmid  12860  mulgcddvds  12874  isprm5lem  12921  pw2dvdslemn  12945  sqrt2irrap  12960  phibndlem  12996  prm23ge5  13045  pclemdc  13069  pcxqcl  13093  pcge0  13094  pcdvdsb  13101  pceq0  13103  pcneg  13106  pcdvdstr  13108  pcgcd1  13109  pcgcd  13110  pc2dvds  13111  pcz  13113  pcprmpw2  13114  pcaddlem  13120  pcadd  13121  pcmpt  13124  pcmpt2  13125  pcprod  13127  fldivp1  13129  qexpz  13133  1arithlem4  13147  1arith  13148  4sqlem19  13190  ennnfonelemss  13303  ennnfonelemkh  13305  ennnfonelemhf1o  13306  ctiunctlemudc  13330  bassetsnn  13411  fvprif  13666  gzsumwsubmcl  13803  gzsumwmhm  13805  gzsumcl  13806  mulgnn0p1  13938  mulgnn0subcl  13940  mulgsubcl  13941  mulgneg  13945  mulgz  13955  mulgnn0dir  13957  mulgdirlem  13958  mulgdir  13959  submmulg  13971  ghmmulg  14061  gzsumreidx  14143  gzsumsubmcl  14144  gzsummhm  14147  gzsumsplit0  14150  gsumvalfi  14154  gzsumgsum  14157  lringuplu  14505  aprlring  14602  znf1o  14988  xblss2ps  15507  xblss2  15508  qtopbas  15625  dedekindeulemeu  15725  dedekindeu  15726  suplociccreex  15727  dedekindicclemeu  15734  dedekindicclemicc  15735  limcimolemlt  15767  cnplimclemle  15771  dvmptc  15820  reeff1o  15876  efltlemlt  15877  efap1p  15882  sin0pilem2  15886  coseq0negpitopi  15940  abssinper  15950  cos02pilt1  15955  logdivlt  15999  logbgcd1irraplemexp  16076  birthdaylem2  16094  birthdaylem3  16095  bcmono  16124  bcmax  16125  lgslem4  16134  lgsneg  16155  lgsneg1  16156  lgsmod  16157  lgsdilem  16158  lgsdir2  16164  lgsdirprm  16165  lgsdir  16166  lgsdi  16168  lgsne0  16169  lgsdirnn0  16178  lgsdinn0  16179  gausslemma2dlem1a  16189  gausslemma2dlem1f1o  16191  gausslemma2dlem4  16195  lgseisenlem1  16201  lgsquad3  16215  2sqlem4  16249  2sqlem9  16255  eupth2lem3lem3fi  16723  eupth2lem3lem4fi  16726  eupth2lem3lem7fi  16727  dichmul0orlem3  16767  dichmul0orlem7  16771  nnsf  17060  nninfsellemsuc  17067  nnnninfex  17077  trilpolemclim  17097  trilpolemisumle  17099  trilpolemeq1  17101  trilpolemlt1  17102  trirec0  17105  apdifflemf  17107  apdifflemr  17108  apdiff  17109  iswomni0  17113  nconstwlpolemgt0  17126  nconstwlpolem  17127  neapmkvlem  17129