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  sn0disj  4127  exmidn0m  4340  exmidsssn  4341  exmidundif  4345  exmidundifim  4346  ordtri2or2exmidlem  4675  reg2exmidlema  4683  nnpredcl  4772  frecabcl  6675  nnsucuniel  6773  dcdifsnid  6782  pw2f1odclem  7140  phpm  7173  fidifsnen  7178  dif1enen  7190  fin0  7195  fimax2gtrilemstep  7211  finexdc  7213  elssdc  7215  eqsndc  7216  en2eqpr  7220  fientri3  7228  unsnfidcex  7233  unsnfidcel  7234  undifdcss  7236  prfidceq  7241  tpfidceq  7243  fiintim  7244  ssfirab  7250  fidcenumlemrks  7277  fidcenumlemr  7279  2omap  7325  omp1eomlem  7441  difinfsnlem  7446  difinfsn  7447  ctssdccl  7458  ctssdc  7460  enumct  7462  nninfninc  7470  nnnninf  7473  nnnninfeq  7475  nnnninfeq2  7476  nninfisol  7480  finomni  7487  ismkvnex  7502  nninfwlpoimlemg  7522  pr2cv1  7548  exmidfodomrlemeldju  7558  exmidfodomrlemreseldju  7559  exmidfodomrlemr  7561  exmidfodomrlemrALT  7562  exmidaclem  7571  exmidontriimlem3  7586  netap  7627  2omotaplemap  7630  mullocprlem  7944  recexprlemloc  8005  suplocsrlem  8182  btwnapz  9787  xnn0dcle  10221  xnn0letri  10222  z2ge  10245  xaddcom  10280  xnegdi  10287  xaddass  10288  xpncan  10290  xleadd1a  10292  xsubge0  10300  xlesubadd  10302  fztri3or  10460  fzm1  10524  fzneuz  10525  exfzdc  10676  zsupcllemstep  10679  infssuzex  10683  exbtwnzlemstep  10699  rebtwn2zlemstep  10704  xqltnle  10719  apbtwnz  10726  flaplt  10739  modifeq2int  10844  modsumfzodifsn  10854  iseqf1olemab  10960  iseqf1olemmo  10963  seq3f1olemqsumk  10970  seq3f1olemqsum  10971  seq3f1olemstep  10972  seqf1oglem1  10977  seqf1oglem2  10978  fser0const  10993  expaddzaplem  11040  qsqeqor  11108  resq01  11116  expnbnd  11122  nn0ltexp2  11169  apexp1  11178  bcval  11209  bccmpl  11214  bcval5  11223  bcpasc  11226  bccl  11227  hashennnuni  11240  hashnncl  11256  fiubm  11293  hashfibc  11305  hashf1  11309  zfz1isolemiso  11313  lswex  11378  ccatsymb  11392  ccat1st1st  11431  fzowrddc  11441  swrd0g  11454  swrdsbslen  11460  swrdspsleq  11461  pfxclz  11473  pfxwrdsymbg  11484  swrdccatin1  11519  resqrexlemnm  11806  resqrexlemcvg  11807  resqrexlemoverl  11809  resqrexlemglsq  11810  leabs  11862  qabscl  11865  nn0abscl  11874  ltabs  11876  abslt  11877  fzomaxdif  11902  maxleim  11994  maxabslemval  11997  zmaxcl  12013  2zsupmax  12015  minmax  12020  zmincl  12029  2zinfmin  12034  xrmaxleim  12035  xrmaxifle  12037  xrmaxiflemab  12038  xrmaxiflemlub  12039  xrmaxiflemcom  12040  xrmaxiflemval  12041  xrmaxaddlem  12051  xrmaxadd  12052  xrminmax  12056  sumdc  12149  fzf1o  12167  sumrbdc  12171  summodclem3  12172  summodclem2a  12173  zsumdc  12176  isumss  12183  fisumss  12184  isumss2  12185  fsumcllem  12191  fsumadd  12198  fsumsplit  12199  fsumsplitsn  12202  sumsplitdc  12224  fisumrev2  12238  fsummulc2  12240  telfsumo  12258  fsumparts  12262  cvgratnnlemseq  12318  cvgratz  12324  fproddccvg  12364  prodrbdc  12366  zproddc  12371  prod1dc  12378  fprodssdc  12382  fprodmul  12383  fprodsplitdc  12388  fprodsplit  12389  fprodunsn  12396  fprodcllem  12398  sinltxirr  12553  fsumdvds  12634  dvdsle  12636  mod2eq1n2dvds  12671  bitsmod  12748  gcdsupex  12759  gcdsupcl  12760  gcdval  12761  gcddvds  12765  gcdcl  12768  gcd0id  12781  gcdneg  12784  bezoutlemmain  12800  bezoutlemzz  12804  bezoutlemaz  12805  bezoutlembz  12806  dfgcd3  12812  dfgcd2  12816  nninfctlemfo  12842  nn0seqcvgd  12844  eucalgf  12858  eucalginv  12859  dvdslcm  12872  lcmcl  12875  lcmneg  12877  lcmgcd  12881  lcmdvds  12882  lcmid  12883  mulgcddvds  12897  prmdcz  12934  isprm5lem  12945  pwbdvdslemn  12969  sqrt2irrap  12985  sqrtrirr  13014  phibndlem  13023  prm23ge5  13072  pclemdc  13096  pcxqcl  13120  pcge0  13121  pcdvdsb  13128  pceq0  13130  pcneg  13133  pcdvdstr  13135  pcgcd1  13136  pcgcd  13137  pc2dvds  13138  pcz  13140  pcprmpw2  13141  pcaddlem  13147  pcadd  13148  pcmpt  13151  pcmpt2  13152  pcprod  13154  fldivp1  13156  qexpz  13160  1arithlem4  13174  1arith  13175  4sqlem19  13217  ennnfonelemss  13359  ennnfonelemkh  13361  ennnfonelemhf1o  13362  ctiunctlemudc  13386  bassetsnn  13467  fvprif  13723  gzsumwsubmcl  13860  gzsumwmhm  13862  gzsumcl  13863  mulgnn0p1  13995  mulgnn0subcl  13997  mulgsubcl  13998  mulgneg  14002  mulgz  14012  mulgnn0dir  14014  mulgdirlem  14015  mulgdir  14016  submmulg  14028  ghmmulg  14118  gzsumreidx  14231  gzsumsubmcl  14232  gzsummhm  14235  gzsumsplit0  14238  gsumvalfi  14242  gzsumgsum  14245  gsummptfidmsplit  14254  gsumresfi  14263  gsum2d2fi  14274  lringuplu  14612  aprlring  14709  znf1o  15095  mplsubrglemcl  15249  xblss2ps  15663  xblss2  15664  qtopbas  15781  dedekindeulemeu  15881  dedekindeu  15882  suplociccreex  15883  dedekindicclemeu  15890  dedekindicclemicc  15891  limcimolemlt  15923  cnplimclemle  15927  dvmptc  15976  reeff1o  16032  efltlemlt  16033  efap1p  16038  sin0pilem2  16042  coseq0negpitopi  16096  abssinper  16106  cos02pilt1  16112  logdivlt  16157  logbgcd1irraplemexp  16237  birthdaylem2  16259  birthdaylem3  16260  ppiqp1le  16300  ppiqltx  16314  ppiqub  16326  chtqub  16329  bcmono  16337  bcmax  16338  bposlem3  16346  bposlem5  16348  bposlem6  16349  bpos  16353  lgslem4  16360  lgsneg  16381  lgsneg1  16382  lgsmod  16383  lgsdilem  16384  lgsdir2  16390  lgsdirprm  16391  lgsdir  16392  lgsdi  16394  lgsne0  16395  lgsdirnn0  16404  lgsdinn0  16405  gausslemma2dlem1a  16415  gausslemma2dlem1f1o  16417  gausslemma2dlem4  16421  lgseisenlem1  16427  lgsquad3  16441  2sqlem4  16475  2sqlem9  16481  eupth2lem3lem3fi  16949  eupth2lem3lem4fi  16952  eupth2lem3lem7fi  16953  dichmul0orlem3  16993  dichmul0orlem7  16997  nnsf  17287  nninfsellemsuc  17294  nnnninfex  17304  trilpolemclim  17325  trilpolemisumle  17327  trilpolemeq1  17329  trilpolemlt1  17330  trirec0  17333  apdifflemf  17335  apdifflemr  17336  apdiff  17337  iswomni0  17341  nconstwlpolemgt0  17354  nconstwlpolem  17355  neapmkvlem  17357