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  6674  nnsucuniel  6772  dcdifsnid  6781  pw2f1odclem  7139  phpm  7172  fidifsnen  7177  dif1enen  7189  fin0  7194  fimax2gtrilemstep  7210  finexdc  7212  elssdc  7214  eqsndc  7215  en2eqpr  7219  fientri3  7227  unsnfidcex  7232  unsnfidcel  7233  undifdcss  7235  prfidceq  7240  tpfidceq  7242  fiintim  7243  ssfirab  7249  fidcenumlemrks  7276  fidcenumlemr  7278  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  9788  xnn0dcle  10222  xnn0letri  10223  z2ge  10246  xaddcom  10281  xnegdi  10288  xaddass  10289  xpncan  10291  xleadd1a  10293  xsubge0  10301  xlesubadd  10303  fztri3or  10461  fzm1  10525  fzneuz  10526  exfzdc  10677  zsupcllemstep  10680  infssuzex  10684  exbtwnzlemstep  10700  rebtwn2zlemstep  10705  xqltnle  10720  apbtwnz  10727  flaplt  10740  modifeq2int  10845  modsumfzodifsn  10855  iseqf1olemab  10961  iseqf1olemmo  10964  seq3f1olemqsumk  10971  seq3f1olemqsum  10972  seq3f1olemstep  10973  seqf1oglem1  10978  seqf1oglem2  10979  fser0const  10994  expaddzaplem  11041  qsqeqor  11109  resq01  11117  expnbnd  11123  nn0ltexp2  11170  apexp1  11179  bcval  11210  bccmpl  11215  bcval5  11224  bcpasc  11227  bccl  11228  hashennnuni  11241  hashnncl  11257  fiubm  11294  hashfibc  11306  hashf1  11310  zfz1isolemiso  11314  lswex  11379  ccatsymb  11393  ccat1st1st  11432  fzowrddc  11442  swrd0g  11455  swrdsbslen  11461  swrdspsleq  11462  pfxclz  11474  pfxwrdsymbg  11485  swrdccatin1  11520  resqrexlemnm  11807  resqrexlemcvg  11808  resqrexlemoverl  11810  resqrexlemglsq  11811  leabs  11863  qabscl  11866  nn0abscl  11875  ltabs  11877  abslt  11878  fzomaxdif  11903  maxleim  11995  maxabslemval  11998  zmaxcl  12014  2zsupmax  12016  minmax  12021  zmincl  12030  2zinfmin  12035  xrmaxleim  12036  xrmaxifle  12038  xrmaxiflemab  12039  xrmaxiflemlub  12040  xrmaxiflemcom  12041  xrmaxiflemval  12042  xrmaxaddlem  12052  xrmaxadd  12053  xrminmax  12057  sumdc  12150  fzf1o  12168  sumrbdc  12172  summodclem3  12173  summodclem2a  12174  zsumdc  12177  isumss  12184  fisumss  12185  isumss2  12186  fsumcllem  12192  fsumadd  12199  fsumsplit  12200  fsumsplitsn  12203  sumsplitdc  12225  fisumrev2  12239  fsummulc2  12241  telfsumo  12259  fsumparts  12263  cvgratnnlemseq  12319  cvgratz  12325  fproddccvg  12365  prodrbdc  12367  zproddc  12372  prod1dc  12379  fprodssdc  12383  fprodmul  12384  fprodsplitdc  12389  fprodsplit  12390  fprodunsn  12397  fprodcllem  12399  sinltxirr  12554  fsumdvds  12635  dvdsle  12637  mod2eq1n2dvds  12672  bitsmod  12749  gcdsupex  12760  gcdsupcl  12761  gcdval  12762  gcddvds  12766  gcdcl  12769  gcd0id  12782  gcdneg  12785  bezoutlemmain  12801  bezoutlemzz  12805  bezoutlemaz  12806  bezoutlembz  12807  dfgcd3  12813  dfgcd2  12817  nninfctlemfo  12843  nn0seqcvgd  12845  eucalgf  12859  eucalginv  12860  dvdslcm  12873  lcmcl  12876  lcmneg  12878  lcmgcd  12882  lcmdvds  12883  lcmid  12884  mulgcddvds  12898  prmdcz  12935  isprm5lem  12946  pwbdvdslemn  12970  sqrt2irrap  12986  sqrtrirr  13015  phibndlem  13024  prm23ge5  13073  pclemdc  13097  pcxqcl  13121  pcge0  13122  pcdvdsb  13129  pceq0  13131  pcneg  13134  pcdvdstr  13136  pcgcd1  13137  pcgcd  13138  pc2dvds  13139  pcz  13141  pcprmpw2  13142  pcaddlem  13148  pcadd  13149  pcmpt  13152  pcmpt2  13153  pcprod  13155  fldivp1  13157  qexpz  13161  1arithlem4  13175  1arith  13176  4sqlem19  13218  ennnfonelemss  13360  ennnfonelemkh  13362  ennnfonelemhf1o  13363  ctiunctlemudc  13387  bassetsnn  13468  fvprif  13724  gzsumwsubmcl  13861  gzsumwmhm  13863  gzsumcl  13864  mulgnn0p1  13996  mulgnn0subcl  13998  mulgsubcl  13999  mulgneg  14003  mulgz  14013  mulgnn0dir  14015  mulgdirlem  14016  mulgdir  14017  submmulg  14029  ghmmulg  14119  gzsumreidx  14232  gzsumsubmcl  14233  gzsummhm  14236  gzsumsplit0  14239  gsumvalfi  14243  gzsumgsum  14246  gsummptfidmsplit  14255  gsumresfi  14264  gsum2d2fi  14275  lringuplu  14613  aprlring  14710  znf1o  15096  xblss2ps  15642  xblss2  15643  qtopbas  15760  dedekindeulemeu  15860  dedekindeu  15861  suplociccreex  15862  dedekindicclemeu  15869  dedekindicclemicc  15870  limcimolemlt  15902  cnplimclemle  15906  dvmptc  15955  reeff1o  16011  efltlemlt  16012  efap1p  16017  sin0pilem2  16021  coseq0negpitopi  16075  abssinper  16085  cos02pilt1  16091  logdivlt  16136  logbgcd1irraplemexp  16216  birthdaylem2  16238  birthdaylem3  16239  ppiqp1le  16279  ppiqltx  16293  ppiqub  16305  chtqub  16308  bcmono  16316  bcmax  16317  bposlem3  16325  bposlem5  16327  bposlem6  16328  bpos  16332  lgslem4  16339  lgsneg  16360  lgsneg1  16361  lgsmod  16362  lgsdilem  16363  lgsdir2  16369  lgsdirprm  16370  lgsdir  16371  lgsdi  16373  lgsne0  16374  lgsdirnn0  16383  lgsdinn0  16384  gausslemma2dlem1a  16394  gausslemma2dlem1f1o  16396  gausslemma2dlem4  16400  lgseisenlem1  16406  lgsquad3  16420  2sqlem4  16454  2sqlem9  16460  eupth2lem3lem3fi  16928  eupth2lem3lem4fi  16931  eupth2lem3lem7fi  16932  dichmul0orlem3  16972  dichmul0orlem7  16976  nnsf  17266  nninfsellemsuc  17273  nnnninfex  17283  trilpolemclim  17304  trilpolemisumle  17306  trilpolemeq1  17308  trilpolemlt1  17309  trirec0  17312  apdifflemf  17314  apdifflemr  17315  apdiff  17316  iswomni0  17320  nconstwlpolemgt0  17333  nconstwlpolem  17334  neapmkvlem  17336