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  3556  ifcldadc  3586  ifeq1dadc  3587  ifeq2dadc  3588  ifbothdadc  3589  ifcldcd  3593  exmidn0m  4230  exmidsssn  4231  exmidundif  4235  exmidundifim  4236  ordtri2or2exmidlem  4558  reg2exmidlema  4566  nnpredcl  4655  frecabcl  6452  nnsucuniel  6548  dcdifsnid  6557  pw2f1odclem  6890  phpm  6921  fidifsnen  6926  dif1enen  6936  fin0  6941  fimax2gtrilemstep  6956  finexdc  6958  en2eqpr  6963  fientri3  6971  unsnfidcex  6976  unsnfidcel  6977  undifdcss  6979  fiintim  6985  ssfirab  6990  fidcenumlemrks  7012  fidcenumlemr  7014  omp1eomlem  7153  difinfsnlem  7158  difinfsn  7159  ctssdccl  7170  ctssdc  7172  enumct  7174  nninfninc  7182  nnnninf  7185  nnnninfeq  7187  nnnninfeq2  7188  nninfisol  7192  finomni  7199  ismkvnex  7214  nninfwlpoimlemg  7234  exmidfodomrlemeldju  7259  exmidfodomrlemreseldju  7260  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  exmidaclem  7268  exmidontriimlem3  7283  netap  7314  2omotaplemap  7317  mullocprlem  7630  recexprlemloc  7691  suplocsrlem  7868  btwnapz  9447  xnn0dcle  9868  xnn0letri  9869  z2ge  9892  xaddcom  9927  xnegdi  9934  xaddass  9935  xpncan  9937  xleadd1a  9939  xsubge0  9947  xlesubadd  9949  fztri3or  10105  fzm1  10166  fzneuz  10167  exfzdc  10307  exbtwnzlemstep  10316  rebtwn2zlemstep  10321  xqltnle  10336  apbtwnz  10343  modifeq2int  10457  modsumfzodifsn  10467  iseqf1olemab  10573  iseqf1olemmo  10576  seq3f1olemqsumk  10583  seq3f1olemqsum  10584  seq3f1olemstep  10585  seqf1oglem1  10590  seqf1oglem2  10591  fser0const  10606  expaddzaplem  10653  qsqeqor  10721  expnbnd  10734  nn0ltexp2  10780  apexp1  10789  bcval  10820  bccmpl  10825  bcval5  10834  bcpasc  10837  bccl  10838  hashennnuni  10850  hashnncl  10866  fiubm  10899  zfz1isolemiso  10910  resqrexlemnm  11162  resqrexlemcvg  11163  resqrexlemoverl  11165  resqrexlemglsq  11166  leabs  11218  nn0abscl  11229  ltabs  11231  abslt  11232  fzomaxdif  11257  maxleim  11349  maxabslemval  11352  zmaxcl  11368  2zsupmax  11369  minmax  11373  2zinfmin  11386  xrmaxleim  11387  xrmaxifle  11389  xrmaxiflemab  11390  xrmaxiflemlub  11391  xrmaxiflemcom  11392  xrmaxiflemval  11393  xrmaxaddlem  11403  xrmaxadd  11404  xrminmax  11408  sumdc  11501  sumrbdc  11522  summodclem3  11523  summodclem2a  11524  zsumdc  11527  isumss  11534  fisumss  11535  isumss2  11536  fsumcllem  11542  fsumadd  11549  fsumsplit  11550  fsumsplitsn  11553  sumsplitdc  11575  fisumrev2  11589  fsummulc2  11591  telfsumo  11609  fsumparts  11613  cvgratnnlemseq  11669  cvgratz  11675  fproddccvg  11715  prodrbdc  11717  zproddc  11722  prod1dc  11729  fprodssdc  11733  fprodmul  11734  fprodsplitdc  11739  fprodsplit  11740  fprodunsn  11747  fprodcllem  11749  sinltxirr  11904  dvdsle  11986  mod2eq1n2dvds  12020  zsupcllemstep  12082  infssuzex  12086  gcdsupex  12094  gcdsupcl  12095  gcdval  12096  gcddvds  12100  gcdcl  12103  gcd0id  12116  gcdneg  12119  bezoutlemmain  12135  bezoutlemzz  12139  bezoutlemaz  12140  bezoutlembz  12141  dfgcd3  12147  dfgcd2  12151  nninfctlemfo  12177  nn0seqcvgd  12179  eucalgf  12193  eucalginv  12194  dvdslcm  12207  lcmcl  12210  lcmneg  12212  lcmgcd  12216  lcmdvds  12217  lcmid  12218  mulgcddvds  12232  isprm5lem  12279  pw2dvdslemn  12303  sqrt2irrap  12318  phibndlem  12354  prm23ge5  12402  pclemdc  12426  pcxqcl  12450  pcge0  12451  pcdvdsb  12458  pceq0  12460  pcneg  12463  pcdvdstr  12465  pcgcd1  12466  pcgcd  12467  pc2dvds  12468  pcz  12470  pcprmpw2  12471  pcaddlem  12477  pcadd  12478  pcmpt  12481  pcmpt2  12482  pcprod  12484  fldivp1  12486  qexpz  12490  1arithlem4  12504  1arith  12505  4sqlem19  12547  ennnfonelemss  12567  ennnfonelemkh  12569  ennnfonelemhf1o  12570  ctiunctlemudc  12594  fvprif  12926  gsumfzz  13067  gsumwsubmcl  13068  gsumwmhm  13070  gsumfzcl  13071  mulgnn0p1  13203  mulgnn0subcl  13205  mulgsubcl  13206  mulgneg  13210  mulgz  13220  mulgnn0dir  13222  mulgdirlem  13223  mulgdir  13224  submmulg  13236  ghmmulg  13326  gsumfzreidx  13407  gsumfzsubmcl  13408  gsumfzmptfidmadd  13409  gsumfzmhm  13413  lringuplu  13692  gsumfzfsum  14076  znf1o  14139  xblss2ps  14572  xblss2  14573  qtopbas  14690  dedekindeulemeu  14776  dedekindeu  14777  suplociccreex  14778  dedekindicclemeu  14785  dedekindicclemicc  14786  limcimolemlt  14818  cnplimclemle  14822  reeff1o  14908  efltlemlt  14909  sin0pilem2  14917  coseq0negpitopi  14971  abssinper  14981  cos02pilt1  14986  logbgcd1irraplemexp  15100  lgslem4  15119  lgsneg  15140  lgsneg1  15141  lgsmod  15142  lgsdilem  15143  lgsdir2  15149  lgsdirprm  15150  lgsdir  15151  lgsdi  15153  lgsne0  15154  lgsdirnn0  15163  lgsdinn0  15164  gausslemma2dlem1a  15174  gausslemma2dlem1f1o  15176  gausslemma2dlem4  15180  lgseisenlem1  15186  2sqlem4  15205  2sqlem9  15211  nnsf  15495  nninfsellemsuc  15502  trilpolemclim  15526  trilpolemisumle  15528  trilpolemeq1  15530  trilpolemlt1  15531  trirec0  15534  apdifflemf  15536  apdifflemr  15537  apdiff  15538  iswomni0  15541  nconstwlpolemgt0  15554  nconstwlpolem  15555  neapmkvlem  15557