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  9729  xnn0dcle  10157  xnn0letri  10158  z2ge  10181  xaddcom  10216  xnegdi  10223  xaddass  10224  xpncan  10226  xleadd1a  10228  xsubge0  10236  xlesubadd  10238  fztri3or  10396  fzm1  10459  fzneuz  10460  exfzdc  10611  zsupcllemstep  10614  infssuzex  10618  exbtwnzlemstep  10634  rebtwn2zlemstep  10639  xqltnle  10654  apbtwnz  10661  modifeq2int  10775  modsumfzodifsn  10785  iseqf1olemab  10891  iseqf1olemmo  10894  seq3f1olemqsumk  10901  seq3f1olemqsum  10902  seq3f1olemstep  10903  seqf1oglem1  10908  seqf1oglem2  10909  fser0const  10924  expaddzaplem  10971  qsqeqor  11039  resq01  11047  expnbnd  11053  nn0ltexp2  11099  apexp1  11108  bcval  11139  bccmpl  11144  bcval5  11153  bcpasc  11156  bccl  11157  hashennnuni  11170  hashnncl  11186  fiubm  11223  hashfibc  11235  zfz1isolemiso  11239  lswex  11304  ccatsymb  11318  ccat1st1st  11357  fzowrddc  11367  swrd0g  11380  swrdsbslen  11386  swrdspsleq  11387  pfxclz  11399  pfxwrdsymbg  11410  swrdccatin1  11445  resqrexlemnm  11732  resqrexlemcvg  11733  resqrexlemoverl  11735  resqrexlemglsq  11736  leabs  11788  nn0abscl  11799  ltabs  11801  abslt  11802  fzomaxdif  11827  maxleim  11919  maxabslemval  11922  zmaxcl  11938  2zsupmax  11940  minmax  11944  2zinfmin  11957  xrmaxleim  11958  xrmaxifle  11960  xrmaxiflemab  11961  xrmaxiflemlub  11962  xrmaxiflemcom  11963  xrmaxiflemval  11964  xrmaxaddlem  11974  xrmaxadd  11975  xrminmax  11979  sumdc  12072  fzf1o  12090  sumrbdc  12094  summodclem3  12095  summodclem2a  12096  zsumdc  12099  isumss  12106  fisumss  12107  isumss2  12108  fsumcllem  12114  fsumadd  12121  fsumsplit  12122  fsumsplitsn  12125  sumsplitdc  12147  fisumrev2  12161  fsummulc2  12163  telfsumo  12181  fsumparts  12185  cvgratnnlemseq  12241  cvgratz  12247  fproddccvg  12287  prodrbdc  12289  zproddc  12294  prod1dc  12301  fprodssdc  12305  fprodmul  12306  fprodsplitdc  12311  fprodsplit  12312  fprodunsn  12319  fprodcllem  12321  sinltxirr  12476  fsumdvds  12557  dvdsle  12559  mod2eq1n2dvds  12594  bitsmod  12671  gcdsupex  12682  gcdsupcl  12683  gcdval  12684  gcddvds  12688  gcdcl  12691  gcd0id  12704  gcdneg  12707  bezoutlemmain  12723  bezoutlemzz  12727  bezoutlemaz  12728  bezoutlembz  12729  dfgcd3  12735  dfgcd2  12739  nninfctlemfo  12765  nn0seqcvgd  12767  eucalgf  12781  eucalginv  12782  dvdslcm  12795  lcmcl  12798  lcmneg  12800  lcmgcd  12804  lcmdvds  12805  lcmid  12806  mulgcddvds  12820  isprm5lem  12867  pw2dvdslemn  12891  sqrt2irrap  12906  phibndlem  12942  prm23ge5  12991  pclemdc  13015  pcxqcl  13039  pcge0  13040  pcdvdsb  13047  pceq0  13049  pcneg  13052  pcdvdstr  13054  pcgcd1  13055  pcgcd  13056  pc2dvds  13057  pcz  13059  pcprmpw2  13060  pcaddlem  13066  pcadd  13067  pcmpt  13070  pcmpt2  13071  pcprod  13073  fldivp1  13075  qexpz  13079  1arithlem4  13093  1arith  13094  4sqlem19  13136  ennnfonelemss  13249  ennnfonelemkh  13251  ennnfonelemhf1o  13252  ctiunctlemudc  13276  bassetsnn  13357  fvprif  13611  gsumfzz  13754  gsumwsubmcl  13755  gsumwmhm  13757  gsumfzcl  13758  mulgnn0p1  13890  mulgnn0subcl  13892  mulgsubcl  13893  mulgneg  13897  mulgz  13907  mulgnn0dir  13909  mulgdirlem  13910  mulgdir  13911  submmulg  13923  ghmmulg  14013  gsumfzreidx  14094  gsumfzsubmcl  14095  gsumfzmptfidmadd  14096  gsumfzmhm  14100  gsumsplit0  14103  gfsumval  14106  gsumgfsum  14110  lringuplu  14445  aprlring  14542  gsumfzfsum  14866  znf1o  14929  xblss2ps  15399  xblss2  15400  qtopbas  15517  dedekindeulemeu  15617  dedekindeu  15618  suplociccreex  15619  dedekindicclemeu  15626  dedekindicclemicc  15627  limcimolemlt  15659  cnplimclemle  15663  dvmptc  15712  reeff1o  15768  efltlemlt  15769  sin0pilem2  15777  coseq0negpitopi  15831  abssinper  15841  cos02pilt1  15846  logbgcd1irraplemexp  15963  lgslem4  16006  lgsneg  16027  lgsneg1  16028  lgsmod  16029  lgsdilem  16030  lgsdir2  16036  lgsdirprm  16037  lgsdir  16038  lgsdi  16040  lgsne0  16041  lgsdirnn0  16050  lgsdinn0  16051  gausslemma2dlem1a  16061  gausslemma2dlem1f1o  16063  gausslemma2dlem4  16067  lgseisenlem1  16073  lgsquad3  16087  2sqlem4  16121  2sqlem9  16127  eupth2lem3lem3fi  16595  eupth2lem3lem4fi  16598  eupth2lem3lem7fi  16599  dichmul0orlem3  16639  dichmul0orlem7  16643  nnsf  16923  nninfsellemsuc  16930  nnnninfex  16940  trilpolemclim  16960  trilpolemisumle  16962  trilpolemeq1  16964  trilpolemlt1  16965  trirec0  16968  apdifflemf  16970  apdifflemr  16971  apdiff  16972  iswomni0  16976  nconstwlpolemgt0  16989  nconstwlpolem  16990  neapmkvlem  16992