Theorem mpjaodan 805

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

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

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 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjao3dan  1343  dcun  3604  ifcldadc  3635  ifeq1dadc  3636  ifeq2dadc  3637  ifeqdadc  3638  ifbothdadc  3639  ifcldcd  3643  2if2dc  3645  exmidn0m  4291  exmidsssn  4292  exmidundif  4296  exmidundifim  4297  ordtri2or2exmidlem  4624  reg2exmidlema  4632  nnpredcl  4721  frecabcl  6565  nnsucuniel  6663  dcdifsnid  6672  pw2f1odclem  7020  phpm  7052  fidifsnen  7057  dif1enen  7069  fin0  7074  fimax2gtrilemstep  7090  finexdc  7092  elssdc  7094  eqsndc  7095  en2eqpr  7099  fientri3  7107  unsnfidcex  7112  unsnfidcel  7113  undifdcss  7115  prfidceq  7120  tpfidceq  7122  fiintim  7123  ssfirab  7129  fidcenumlemrks  7152  fidcenumlemr  7154  omp1eomlem  7293  difinfsnlem  7298  difinfsn  7299  ctssdccl  7310  ctssdc  7312  enumct  7314  nninfninc  7322  nnnninf  7325  nnnninfeq  7327  nnnninfeq2  7328  nninfisol  7332  finomni  7339  ismkvnex  7354  nninfwlpoimlemg  7374  pr2cv1  7400  exmidfodomrlemeldju  7410  exmidfodomrlemreseldju  7411  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  exmidaclem  7423  exmidontriimlem3  7438  netap  7473  2omotaplemap  7476  mullocprlem  7790  recexprlemloc  7851  suplocsrlem  8028  btwnapz  9610  xnn0dcle  10037  xnn0letri  10038  z2ge  10061  xaddcom  10096  xnegdi  10103  xaddass  10104  xpncan  10106  xleadd1a  10108  xsubge0  10116  xlesubadd  10118  fztri3or  10274  fzm1  10335  fzneuz  10336  exfzdc  10487  zsupcllemstep  10490  infssuzex  10494  exbtwnzlemstep  10508  rebtwn2zlemstep  10513  xqltnle  10528  apbtwnz  10535  modifeq2int  10649  modsumfzodifsn  10659  iseqf1olemab  10765  iseqf1olemmo  10768  seq3f1olemqsumk  10775  seq3f1olemqsum  10776  seq3f1olemstep  10777  seqf1oglem1  10782  seqf1oglem2  10783  fser0const  10798  expaddzaplem  10845  qsqeqor  10913  expnbnd  10926  nn0ltexp2  10972  apexp1  10981  bcval  11012  bccmpl  11017  bcval5  11026  bcpasc  11029  bccl  11030  hashennnuni  11042  hashnncl  11058  fiubm  11093  zfz1isolemiso  11104  lswex  11169  ccatsymb  11183  ccat1st1st  11222  fzowrddc  11232  swrd0g  11245  swrdsbslen  11251  swrdspsleq  11252  pfxclz  11264  pfxwrdsymbg  11275  swrdccatin1  11310  resqrexlemnm  11583  resqrexlemcvg  11584  resqrexlemoverl  11586  resqrexlemglsq  11587  leabs  11639  nn0abscl  11650  ltabs  11652  abslt  11653  fzomaxdif  11678  maxleim  11770  maxabslemval  11773  zmaxcl  11789  2zsupmax  11791  minmax  11795  2zinfmin  11808  xrmaxleim  11809  xrmaxifle  11811  xrmaxiflemab  11812  xrmaxiflemlub  11813  xrmaxiflemcom  11814  xrmaxiflemval  11815  xrmaxaddlem  11825  xrmaxadd  11826  xrminmax  11830  sumdc  11923  fzf1o  11941  sumrbdc  11945  summodclem3  11946  summodclem2a  11947  zsumdc  11950  isumss  11957  fisumss  11958  isumss2  11959  fsumcllem  11965  fsumadd  11972  fsumsplit  11973  fsumsplitsn  11976  sumsplitdc  11998  fisumrev2  12012  fsummulc2  12014  telfsumo  12032  fsumparts  12036  cvgratnnlemseq  12092  cvgratz  12098  fproddccvg  12138  prodrbdc  12140  zproddc  12145  prod1dc  12152  fprodssdc  12156  fprodmul  12157  fprodsplitdc  12162  fprodsplit  12163  fprodunsn  12170  fprodcllem  12172  sinltxirr  12327  fsumdvds  12408  dvdsle  12410  mod2eq1n2dvds  12445  bitsmod  12522  gcdsupex  12533  gcdsupcl  12534  gcdval  12535  gcddvds  12539  gcdcl  12542  gcd0id  12555  gcdneg  12558  bezoutlemmain  12574  bezoutlemzz  12578  bezoutlemaz  12579  bezoutlembz  12580  dfgcd3  12586  dfgcd2  12590  nninfctlemfo  12616  nn0seqcvgd  12618  eucalgf  12632  eucalginv  12633  dvdslcm  12646  lcmcl  12649  lcmneg  12651  lcmgcd  12655  lcmdvds  12656  lcmid  12657  mulgcddvds  12671  isprm5lem  12718  pw2dvdslemn  12742  sqrt2irrap  12757  phibndlem  12793  prm23ge5  12842  pclemdc  12866  pcxqcl  12890  pcge0  12891  pcdvdsb  12898  pceq0  12900  pcneg  12903  pcdvdstr  12905  pcgcd1  12906  pcgcd  12907  pc2dvds  12908  pcz  12910  pcprmpw2  12911  pcaddlem  12917  pcadd  12918  pcmpt  12921  pcmpt2  12922  pcprod  12924  fldivp1  12926  qexpz  12930  1arithlem4  12944  1arith  12945  4sqlem19  12987  ennnfonelemss  13036  ennnfonelemkh  13038  ennnfonelemhf1o  13039  ctiunctlemudc  13063  bassetsnn  13144  fvprif  13431  gsumfzz  13583  gsumwsubmcl  13584  gsumwmhm  13586  gsumfzcl  13587  mulgnn0p1  13725  mulgnn0subcl  13727  mulgsubcl  13728  mulgneg  13732  mulgz  13742  mulgnn0dir  13744  mulgdirlem  13745  mulgdir  13746  submmulg  13758  ghmmulg  13848  gsumfzreidx  13929  gsumfzsubmcl  13930  gsumfzmptfidmadd  13931  gsumfzmhm  13935  gsumsplit0  13938  lringuplu  14216  gsumfzfsum  14608  znf1o  14671  xblss2ps  15134  xblss2  15135  qtopbas  15252  dedekindeulemeu  15352  dedekindeu  15353  suplociccreex  15354  dedekindicclemeu  15361  dedekindicclemicc  15362  limcimolemlt  15394  cnplimclemle  15398  dvmptc  15447  reeff1o  15503  efltlemlt  15504  sin0pilem2  15512  coseq0negpitopi  15566  abssinper  15576  cos02pilt1  15581  logbgcd1irraplemexp  15698  lgslem4  15738  lgsneg  15759  lgsneg1  15760  lgsmod  15761  lgsdilem  15762  lgsdir2  15768  lgsdirprm  15769  lgsdir  15770  lgsdi  15772  lgsne0  15773  lgsdirnn0  15782  lgsdinn0  15783  gausslemma2dlem1a  15793  gausslemma2dlem1f1o  15795  gausslemma2dlem4  15799  lgseisenlem1  15805  lgsquad3  15819  2sqlem4  15853  2sqlem9  15859  eupth2lem3lem3fi  16327  eupth2lem3lem4fi  16330  eupth2lem3lem7fi  16331  2omap  16620  nnsf  16633  nninfsellemsuc  16640  nnnninfex  16650  trilpolemclim  16666  trilpolemisumle  16668  trilpolemeq1  16670  trilpolemlt1  16671  trirec0  16674  apdifflemf  16676  apdifflemr  16677  apdiff  16678  iswomni0  16681  nconstwlpolemgt0  16694  nconstwlpolem  16695  neapmkvlem  16697  gfsumval  16706  gsumgfsum  16710