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  3606  ifcldadc  3639  ifeq1dadc  3640  ifeq2dadc  3641  ifeqdadc  3642  ifbothdadc  3643  ifcldcd  3647  2if2dc  3649  exmidn0m  4297  exmidsssn  4298  exmidundif  4302  exmidundifim  4303  ordtri2or2exmidlem  4630  reg2exmidlema  4638  nnpredcl  4727  frecabcl  6608  nnsucuniel  6706  dcdifsnid  6715  pw2f1odclem  7063  phpm  7095  fidifsnen  7100  dif1enen  7112  fin0  7117  fimax2gtrilemstep  7133  finexdc  7135  elssdc  7137  eqsndc  7138  en2eqpr  7142  fientri3  7150  unsnfidcex  7155  unsnfidcel  7156  undifdcss  7158  prfidceq  7163  tpfidceq  7165  fiintim  7166  ssfirab  7172  fidcenumlemrks  7195  fidcenumlemr  7197  omp1eomlem  7336  difinfsnlem  7341  difinfsn  7342  ctssdccl  7353  ctssdc  7355  enumct  7357  nninfninc  7365  nnnninf  7368  nnnninfeq  7370  nnnninfeq2  7371  nninfisol  7375  finomni  7382  ismkvnex  7397  nninfwlpoimlemg  7417  pr2cv1  7443  exmidfodomrlemeldju  7453  exmidfodomrlemreseldju  7454  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  exmidaclem  7466  exmidontriimlem3  7481  netap  7516  2omotaplemap  7519  mullocprlem  7833  recexprlemloc  7894  suplocsrlem  8071  btwnapz  9653  xnn0dcle  10080  xnn0letri  10081  z2ge  10104  xaddcom  10139  xnegdi  10146  xaddass  10147  xpncan  10149  xleadd1a  10151  xsubge0  10159  xlesubadd  10161  fztri3or  10317  fzm1  10378  fzneuz  10379  exfzdc  10530  zsupcllemstep  10533  infssuzex  10537  exbtwnzlemstep  10551  rebtwn2zlemstep  10556  xqltnle  10571  apbtwnz  10578  modifeq2int  10692  modsumfzodifsn  10702  iseqf1olemab  10808  iseqf1olemmo  10811  seq3f1olemqsumk  10818  seq3f1olemqsum  10819  seq3f1olemstep  10820  seqf1oglem1  10825  seqf1oglem2  10826  fser0const  10841  expaddzaplem  10888  qsqeqor  10956  expnbnd  10969  nn0ltexp2  11015  apexp1  11024  bcval  11055  bccmpl  11060  bcval5  11069  bcpasc  11072  bccl  11073  hashennnuni  11085  hashnncl  11101  fiubm  11136  zfz1isolemiso  11147  lswex  11212  ccatsymb  11226  ccat1st1st  11265  fzowrddc  11275  swrd0g  11288  swrdsbslen  11294  swrdspsleq  11295  pfxclz  11307  pfxwrdsymbg  11318  swrdccatin1  11353  resqrexlemnm  11639  resqrexlemcvg  11640  resqrexlemoverl  11642  resqrexlemglsq  11643  leabs  11695  nn0abscl  11706  ltabs  11708  abslt  11709  fzomaxdif  11734  maxleim  11826  maxabslemval  11829  zmaxcl  11845  2zsupmax  11847  minmax  11851  2zinfmin  11864  xrmaxleim  11865  xrmaxifle  11867  xrmaxiflemab  11868  xrmaxiflemlub  11869  xrmaxiflemcom  11870  xrmaxiflemval  11871  xrmaxaddlem  11881  xrmaxadd  11882  xrminmax  11886  sumdc  11979  fzf1o  11997  sumrbdc  12001  summodclem3  12002  summodclem2a  12003  zsumdc  12006  isumss  12013  fisumss  12014  isumss2  12015  fsumcllem  12021  fsumadd  12028  fsumsplit  12029  fsumsplitsn  12032  sumsplitdc  12054  fisumrev2  12068  fsummulc2  12070  telfsumo  12088  fsumparts  12092  cvgratnnlemseq  12148  cvgratz  12154  fproddccvg  12194  prodrbdc  12196  zproddc  12201  prod1dc  12208  fprodssdc  12212  fprodmul  12213  fprodsplitdc  12218  fprodsplit  12219  fprodunsn  12226  fprodcllem  12228  sinltxirr  12383  fsumdvds  12464  dvdsle  12466  mod2eq1n2dvds  12501  bitsmod  12578  gcdsupex  12589  gcdsupcl  12590  gcdval  12591  gcddvds  12595  gcdcl  12598  gcd0id  12611  gcdneg  12614  bezoutlemmain  12630  bezoutlemzz  12634  bezoutlemaz  12635  bezoutlembz  12636  dfgcd3  12642  dfgcd2  12646  nninfctlemfo  12672  nn0seqcvgd  12674  eucalgf  12688  eucalginv  12689  dvdslcm  12702  lcmcl  12705  lcmneg  12707  lcmgcd  12711  lcmdvds  12712  lcmid  12713  mulgcddvds  12727  isprm5lem  12774  pw2dvdslemn  12798  sqrt2irrap  12813  phibndlem  12849  prm23ge5  12898  pclemdc  12922  pcxqcl  12946  pcge0  12947  pcdvdsb  12954  pceq0  12956  pcneg  12959  pcdvdstr  12961  pcgcd1  12962  pcgcd  12963  pc2dvds  12964  pcz  12966  pcprmpw2  12967  pcaddlem  12973  pcadd  12974  pcmpt  12977  pcmpt2  12978  pcprod  12980  fldivp1  12982  qexpz  12986  1arithlem4  13000  1arith  13001  4sqlem19  13043  ennnfonelemss  13092  ennnfonelemkh  13094  ennnfonelemhf1o  13095  ctiunctlemudc  13119  bassetsnn  13200  fvprif  13487  gsumfzz  13639  gsumwsubmcl  13640  gsumwmhm  13642  gsumfzcl  13643  mulgnn0p1  13781  mulgnn0subcl  13783  mulgsubcl  13784  mulgneg  13788  mulgz  13798  mulgnn0dir  13800  mulgdirlem  13801  mulgdir  13802  submmulg  13814  ghmmulg  13904  gsumfzreidx  13985  gsumfzsubmcl  13986  gsumfzmptfidmadd  13987  gsumfzmhm  13991  gsumsplit0  13994  lringuplu  14272  gsumfzfsum  14664  znf1o  14727  xblss2ps  15195  xblss2  15196  qtopbas  15313  dedekindeulemeu  15413  dedekindeu  15414  suplociccreex  15415  dedekindicclemeu  15422  dedekindicclemicc  15423  limcimolemlt  15455  cnplimclemle  15459  dvmptc  15508  reeff1o  15564  efltlemlt  15565  sin0pilem2  15573  coseq0negpitopi  15627  abssinper  15637  cos02pilt1  15642  logbgcd1irraplemexp  15759  lgslem4  15802  lgsneg  15823  lgsneg1  15824  lgsmod  15825  lgsdilem  15826  lgsdir2  15832  lgsdirprm  15833  lgsdir  15834  lgsdi  15836  lgsne0  15837  lgsdirnn0  15846  lgsdinn0  15847  gausslemma2dlem1a  15857  gausslemma2dlem1f1o  15859  gausslemma2dlem4  15863  lgseisenlem1  15869  lgsquad3  15883  2sqlem4  15917  2sqlem9  15923  eupth2lem3lem3fi  16391  eupth2lem3lem4fi  16394  eupth2lem3lem7fi  16395  2omap  16695  nnsf  16711  nninfsellemsuc  16718  nnnninfex  16728  trilpolemclim  16748  trilpolemisumle  16750  trilpolemeq1  16752  trilpolemlt1  16753  trirec0  16756  apdifflemf  16758  apdifflemr  16759  apdiff  16760  iswomni0  16764  nconstwlpolemgt0  16777  nconstwlpolem  16778  neapmkvlem  16780  gfsumval  16789  gsumgfsum  16793