Theorem mpjaodan 799

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

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

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjao3dan  1318  dcun  3557  ifcldadc  3587  ifeq1dadc  3588  ifeq2dadc  3589  ifbothdadc  3590  ifcldcd  3594  exmidn0m  4231  exmidsssn  4232  exmidundif  4236  exmidundifim  4237  ordtri2or2exmidlem  4559  reg2exmidlema  4567  nnpredcl  4656  frecabcl  6454  nnsucuniel  6550  dcdifsnid  6559  pw2f1odclem  6892  phpm  6923  fidifsnen  6928  dif1enen  6938  fin0  6943  fimax2gtrilemstep  6958  finexdc  6960  en2eqpr  6965  fientri3  6973  unsnfidcex  6978  unsnfidcel  6979  undifdcss  6981  fiintim  6987  ssfirab  6992  fidcenumlemrks  7014  fidcenumlemr  7016  omp1eomlem  7155  difinfsnlem  7160  difinfsn  7161  ctssdccl  7172  ctssdc  7174  enumct  7176  nninfninc  7184  nnnninf  7187  nnnninfeq  7189  nnnninfeq2  7190  nninfisol  7194  finomni  7201  ismkvnex  7216  nninfwlpoimlemg  7236  exmidfodomrlemeldju  7261  exmidfodomrlemreseldju  7262  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  exmidaclem  7270  exmidontriimlem3  7285  netap  7316  2omotaplemap  7319  mullocprlem  7632  recexprlemloc  7693  suplocsrlem  7870  btwnapz  9450  xnn0dcle  9871  xnn0letri  9872  z2ge  9895  xaddcom  9930  xnegdi  9937  xaddass  9938  xpncan  9940  xleadd1a  9942  xsubge0  9950  xlesubadd  9952  fztri3or  10108  fzm1  10169  fzneuz  10170  exfzdc  10310  exbtwnzlemstep  10319  rebtwn2zlemstep  10324  xqltnle  10339  apbtwnz  10346  modifeq2int  10460  modsumfzodifsn  10470  iseqf1olemab  10576  iseqf1olemmo  10579  seq3f1olemqsumk  10586  seq3f1olemqsum  10587  seq3f1olemstep  10588  seqf1oglem1  10593  seqf1oglem2  10594  fser0const  10609  expaddzaplem  10656  qsqeqor  10724  expnbnd  10737  nn0ltexp2  10783  apexp1  10792  bcval  10823  bccmpl  10828  bcval5  10837  bcpasc  10840  bccl  10841  hashennnuni  10853  hashnncl  10869  fiubm  10902  zfz1isolemiso  10913  resqrexlemnm  11165  resqrexlemcvg  11166  resqrexlemoverl  11168  resqrexlemglsq  11169  leabs  11221  nn0abscl  11232  ltabs  11234  abslt  11235  fzomaxdif  11260  maxleim  11352  maxabslemval  11355  zmaxcl  11371  2zsupmax  11372  minmax  11376  2zinfmin  11389  xrmaxleim  11390  xrmaxifle  11392  xrmaxiflemab  11393  xrmaxiflemlub  11394  xrmaxiflemcom  11395  xrmaxiflemval  11396  xrmaxaddlem  11406  xrmaxadd  11407  xrminmax  11411  sumdc  11504  sumrbdc  11525  summodclem3  11526  summodclem2a  11527  zsumdc  11530  isumss  11537  fisumss  11538  isumss2  11539  fsumcllem  11545  fsumadd  11552  fsumsplit  11553  fsumsplitsn  11556  sumsplitdc  11578  fisumrev2  11592  fsummulc2  11594  telfsumo  11612  fsumparts  11616  cvgratnnlemseq  11672  cvgratz  11678  fproddccvg  11718  prodrbdc  11720  zproddc  11725  prod1dc  11732  fprodssdc  11736  fprodmul  11737  fprodsplitdc  11742  fprodsplit  11743  fprodunsn  11750  fprodcllem  11752  sinltxirr  11907  dvdsle  11989  mod2eq1n2dvds  12023  zsupcllemstep  12085  infssuzex  12089  gcdsupex  12097  gcdsupcl  12098  gcdval  12099  gcddvds  12103  gcdcl  12106  gcd0id  12119  gcdneg  12122  bezoutlemmain  12138  bezoutlemzz  12142  bezoutlemaz  12143  bezoutlembz  12144  dfgcd3  12150  dfgcd2  12154  nninfctlemfo  12180  nn0seqcvgd  12182  eucalgf  12196  eucalginv  12197  dvdslcm  12210  lcmcl  12213  lcmneg  12215  lcmgcd  12219  lcmdvds  12220  lcmid  12221  mulgcddvds  12235  isprm5lem  12282  pw2dvdslemn  12306  sqrt2irrap  12321  phibndlem  12357  prm23ge5  12405  pclemdc  12429  pcxqcl  12453  pcge0  12454  pcdvdsb  12461  pceq0  12463  pcneg  12466  pcdvdstr  12468  pcgcd1  12469  pcgcd  12470  pc2dvds  12471  pcz  12473  pcprmpw2  12474  pcaddlem  12480  pcadd  12481  pcmpt  12484  pcmpt2  12485  pcprod  12487  fldivp1  12489  qexpz  12493  1arithlem4  12507  1arith  12508  4sqlem19  12550  ennnfonelemss  12570  ennnfonelemkh  12572  ennnfonelemhf1o  12573  ctiunctlemudc  12597  fvprif  12929  gsumfzz  13070  gsumwsubmcl  13071  gsumwmhm  13073  gsumfzcl  13074  mulgnn0p1  13206  mulgnn0subcl  13208  mulgsubcl  13209  mulgneg  13213  mulgz  13223  mulgnn0dir  13225  mulgdirlem  13226  mulgdir  13227  submmulg  13239  ghmmulg  13329  gsumfzreidx  13410  gsumfzsubmcl  13411  gsumfzmptfidmadd  13412  gsumfzmhm  13416  lringuplu  13695  gsumfzfsum  14087  znf1o  14150  xblss2ps  14583  xblss2  14584  qtopbas  14701  dedekindeulemeu  14801  dedekindeu  14802  suplociccreex  14803  dedekindicclemeu  14810  dedekindicclemicc  14811  limcimolemlt  14843  cnplimclemle  14847  dvmptc  14896  reeff1o  14949  efltlemlt  14950  sin0pilem2  14958  coseq0negpitopi  15012  abssinper  15022  cos02pilt1  15027  logbgcd1irraplemexp  15141  lgslem4  15160  lgsneg  15181  lgsneg1  15182  lgsmod  15183  lgsdilem  15184  lgsdir2  15190  lgsdirprm  15191  lgsdir  15192  lgsdi  15194  lgsne0  15195  lgsdirnn0  15204  lgsdinn0  15205  gausslemma2dlem1a  15215  gausslemma2dlem1f1o  15217  gausslemma2dlem4  15221  lgseisenlem1  15227  lgsquad3  15241  2sqlem4  15275  2sqlem9  15281  nnsf  15565  nninfsellemsuc  15572  trilpolemclim  15596  trilpolemisumle  15598  trilpolemeq1  15600  trilpolemlt1  15601  trirec0  15604  apdifflemf  15606  apdifflemr  15607  apdiff  15608  iswomni0  15611  nconstwlpolemgt0  15624  nconstwlpolem  15625  neapmkvlem  15627