Theorem mpjaodan 803

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

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

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjao3dan  1341  dcun  3601  ifcldadc  3632  ifeq1dadc  3633  ifeq2dadc  3634  ifeqdadc  3635  ifbothdadc  3636  ifcldcd  3640  2if2dc  3642  exmidn0m  4284  exmidsssn  4285  exmidundif  4289  exmidundifim  4290  ordtri2or2exmidlem  4615  reg2exmidlema  4623  nnpredcl  4712  frecabcl  6535  nnsucuniel  6631  dcdifsnid  6640  pw2f1odclem  6983  phpm  7015  fidifsnen  7020  dif1enen  7030  fin0  7035  fimax2gtrilemstep  7050  finexdc  7052  en2eqpr  7057  fientri3  7065  unsnfidcex  7070  unsnfidcel  7071  undifdcss  7073  prfidceq  7078  tpfidceq  7080  fiintim  7081  ssfirab  7086  fidcenumlemrks  7108  fidcenumlemr  7110  omp1eomlem  7249  difinfsnlem  7254  difinfsn  7255  ctssdccl  7266  ctssdc  7268  enumct  7270  nninfninc  7278  nnnninf  7281  nnnninfeq  7283  nnnninfeq2  7284  nninfisol  7288  finomni  7295  ismkvnex  7310  nninfwlpoimlemg  7330  pr2cv1  7356  exmidfodomrlemeldju  7365  exmidfodomrlemreseldju  7366  exmidfodomrlemr  7368  exmidfodomrlemrALT  7369  exmidaclem  7378  exmidontriimlem3  7393  netap  7428  2omotaplemap  7431  mullocprlem  7745  recexprlemloc  7806  suplocsrlem  7983  btwnapz  9565  xnn0dcle  9986  xnn0letri  9987  z2ge  10010  xaddcom  10045  xnegdi  10052  xaddass  10053  xpncan  10055  xleadd1a  10057  xsubge0  10065  xlesubadd  10067  fztri3or  10223  fzm1  10284  fzneuz  10285  exfzdc  10433  zsupcllemstep  10436  infssuzex  10440  exbtwnzlemstep  10454  rebtwn2zlemstep  10459  xqltnle  10474  apbtwnz  10481  modifeq2int  10595  modsumfzodifsn  10605  iseqf1olemab  10711  iseqf1olemmo  10714  seq3f1olemqsumk  10721  seq3f1olemqsum  10722  seq3f1olemstep  10723  seqf1oglem1  10728  seqf1oglem2  10729  fser0const  10744  expaddzaplem  10791  qsqeqor  10859  expnbnd  10872  nn0ltexp2  10918  apexp1  10927  bcval  10958  bccmpl  10963  bcval5  10972  bcpasc  10975  bccl  10976  hashennnuni  10988  hashnncl  11004  fiubm  11037  zfz1isolemiso  11048  lswex  11109  ccatsymb  11123  ccat1st1st  11158  fzowrddc  11165  swrd0g  11178  swrdsbslen  11184  swrdspsleq  11185  pfxclz  11197  pfxwrdsymbg  11208  swrdccatin1  11243  resqrexlemnm  11515  resqrexlemcvg  11516  resqrexlemoverl  11518  resqrexlemglsq  11519  leabs  11571  nn0abscl  11582  ltabs  11584  abslt  11585  fzomaxdif  11610  maxleim  11702  maxabslemval  11705  zmaxcl  11721  2zsupmax  11723  minmax  11727  2zinfmin  11740  xrmaxleim  11741  xrmaxifle  11743  xrmaxiflemab  11744  xrmaxiflemlub  11745  xrmaxiflemcom  11746  xrmaxiflemval  11747  xrmaxaddlem  11757  xrmaxadd  11758  xrminmax  11762  sumdc  11855  sumrbdc  11876  summodclem3  11877  summodclem2a  11878  zsumdc  11881  isumss  11888  fisumss  11889  isumss2  11890  fsumcllem  11896  fsumadd  11903  fsumsplit  11904  fsumsplitsn  11907  sumsplitdc  11929  fisumrev2  11943  fsummulc2  11945  telfsumo  11963  fsumparts  11967  cvgratnnlemseq  12023  cvgratz  12029  fproddccvg  12069  prodrbdc  12071  zproddc  12076  prod1dc  12083  fprodssdc  12087  fprodmul  12088  fprodsplitdc  12093  fprodsplit  12094  fprodunsn  12101  fprodcllem  12103  sinltxirr  12258  fsumdvds  12339  dvdsle  12341  mod2eq1n2dvds  12376  bitsmod  12453  gcdsupex  12464  gcdsupcl  12465  gcdval  12466  gcddvds  12470  gcdcl  12473  gcd0id  12486  gcdneg  12489  bezoutlemmain  12505  bezoutlemzz  12509  bezoutlemaz  12510  bezoutlembz  12511  dfgcd3  12517  dfgcd2  12521  nninfctlemfo  12547  nn0seqcvgd  12549  eucalgf  12563  eucalginv  12564  dvdslcm  12577  lcmcl  12580  lcmneg  12582  lcmgcd  12586  lcmdvds  12587  lcmid  12588  mulgcddvds  12602  isprm5lem  12649  pw2dvdslemn  12673  sqrt2irrap  12688  phibndlem  12724  prm23ge5  12773  pclemdc  12797  pcxqcl  12821  pcge0  12822  pcdvdsb  12829  pceq0  12831  pcneg  12834  pcdvdstr  12836  pcgcd1  12837  pcgcd  12838  pc2dvds  12839  pcz  12841  pcprmpw2  12842  pcaddlem  12848  pcadd  12849  pcmpt  12852  pcmpt2  12853  pcprod  12855  fldivp1  12857  qexpz  12861  1arithlem4  12875  1arith  12876  4sqlem19  12918  ennnfonelemss  12967  ennnfonelemkh  12969  ennnfonelemhf1o  12970  ctiunctlemudc  12994  bassetsnn  13075  fvprif  13362  gsumfzz  13514  gsumwsubmcl  13515  gsumwmhm  13517  gsumfzcl  13518  mulgnn0p1  13656  mulgnn0subcl  13658  mulgsubcl  13659  mulgneg  13663  mulgz  13673  mulgnn0dir  13675  mulgdirlem  13676  mulgdir  13677  submmulg  13689  ghmmulg  13779  gsumfzreidx  13860  gsumfzsubmcl  13861  gsumfzmptfidmadd  13862  gsumfzmhm  13866  lringuplu  14145  gsumfzfsum  14537  znf1o  14600  xblss2ps  15063  xblss2  15064  qtopbas  15181  dedekindeulemeu  15281  dedekindeu  15282  suplociccreex  15283  dedekindicclemeu  15290  dedekindicclemicc  15291  limcimolemlt  15323  cnplimclemle  15327  dvmptc  15376  reeff1o  15432  efltlemlt  15433  sin0pilem2  15441  coseq0negpitopi  15495  abssinper  15505  cos02pilt1  15510  logbgcd1irraplemexp  15627  lgslem4  15667  lgsneg  15688  lgsneg1  15689  lgsmod  15690  lgsdilem  15691  lgsdir2  15697  lgsdirprm  15698  lgsdir  15699  lgsdi  15701  lgsne0  15702  lgsdirnn0  15711  lgsdinn0  15712  gausslemma2dlem1a  15722  gausslemma2dlem1f1o  15724  gausslemma2dlem4  15728  lgseisenlem1  15734  lgsquad3  15748  2sqlem4  15782  2sqlem9  15788  2omap  16290  nnsf  16302  nninfsellemsuc  16309  nnnninfex  16319  trilpolemclim  16335  trilpolemisumle  16337  trilpolemeq1  16339  trilpolemlt1  16340  trirec0  16343  apdifflemf  16345  apdifflemr  16346  apdiff  16347  iswomni0  16350  nconstwlpolemgt0  16363  nconstwlpolem  16364  neapmkvlem  16366