Theorem mpjaodan 806

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

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

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjao3dan  1344  dcun  3618  ifcldadc  3651  ifeq1dadc  3652  ifeq2dadc  3653  ifeqdadc  3654  ifbothdadc  3655  ifcldcd  3659  2if2dc  3661  exmidn0m  4313  exmidsssn  4314  exmidundif  4318  exmidundifim  4319  ordtri2or2exmidlem  4647  reg2exmidlema  4655  nnpredcl  4744  frecabcl  6629  nnsucuniel  6727  dcdifsnid  6736  pw2f1odclem  7086  phpm  7119  fidifsnen  7124  dif1enen  7136  fin0  7141  fimax2gtrilemstep  7157  finexdc  7159  elssdc  7161  eqsndc  7162  en2eqpr  7166  fientri3  7174  unsnfidcex  7179  unsnfidcel  7180  undifdcss  7182  prfidceq  7187  tpfidceq  7189  fiintim  7190  ssfirab  7196  fidcenumlemrks  7222  fidcenumlemr  7224  2omap  7268  omp1eomlem  7384  difinfsnlem  7389  difinfsn  7390  ctssdccl  7401  ctssdc  7403  enumct  7405  nninfninc  7413  nnnninf  7416  nnnninfeq  7418  nnnninfeq2  7419  nninfisol  7423  finomni  7430  ismkvnex  7445  nninfwlpoimlemg  7465  pr2cv1  7491  exmidfodomrlemeldju  7501  exmidfodomrlemreseldju  7502  exmidfodomrlemr  7504  exmidfodomrlemrALT  7505  exmidaclem  7514  exmidontriimlem3  7529  netap  7567  2omotaplemap  7570  mullocprlem  7884  recexprlemloc  7945  suplocsrlem  8122  btwnapz  9707  xnn0dcle  10134  xnn0letri  10135  z2ge  10158  xaddcom  10193  xnegdi  10200  xaddass  10201  xpncan  10203  xleadd1a  10205  xsubge0  10213  xlesubadd  10215  fztri3or  10372  fzm1  10433  fzneuz  10434  exfzdc  10585  zsupcllemstep  10588  infssuzex  10592  exbtwnzlemstep  10606  rebtwn2zlemstep  10611  xqltnle  10626  apbtwnz  10633  modifeq2int  10747  modsumfzodifsn  10757  iseqf1olemab  10863  iseqf1olemmo  10866  seq3f1olemqsumk  10873  seq3f1olemqsum  10874  seq3f1olemstep  10875  seqf1oglem1  10880  seqf1oglem2  10881  fser0const  10896  expaddzaplem  10943  qsqeqor  11011  expnbnd  11024  nn0ltexp2  11070  apexp1  11079  bcval  11110  bccmpl  11115  bcval5  11124  bcpasc  11127  bccl  11128  hashennnuni  11140  hashnncl  11156  fiubm  11191  hashfibc  11203  zfz1isolemiso  11207  lswex  11272  ccatsymb  11286  ccat1st1st  11325  fzowrddc  11335  swrd0g  11348  swrdsbslen  11354  swrdspsleq  11355  pfxclz  11367  pfxwrdsymbg  11378  swrdccatin1  11413  resqrexlemnm  11699  resqrexlemcvg  11700  resqrexlemoverl  11702  resqrexlemglsq  11703  leabs  11755  nn0abscl  11766  ltabs  11768  abslt  11769  fzomaxdif  11794  maxleim  11886  maxabslemval  11889  zmaxcl  11905  2zsupmax  11907  minmax  11911  2zinfmin  11924  xrmaxleim  11925  xrmaxifle  11927  xrmaxiflemab  11928  xrmaxiflemlub  11929  xrmaxiflemcom  11930  xrmaxiflemval  11931  xrmaxaddlem  11941  xrmaxadd  11942  xrminmax  11946  sumdc  12039  fzf1o  12057  sumrbdc  12061  summodclem3  12062  summodclem2a  12063  zsumdc  12066  isumss  12073  fisumss  12074  isumss2  12075  fsumcllem  12081  fsumadd  12088  fsumsplit  12089  fsumsplitsn  12092  sumsplitdc  12114  fisumrev2  12128  fsummulc2  12130  telfsumo  12148  fsumparts  12152  cvgratnnlemseq  12208  cvgratz  12214  fproddccvg  12254  prodrbdc  12256  zproddc  12261  prod1dc  12268  fprodssdc  12272  fprodmul  12273  fprodsplitdc  12278  fprodsplit  12279  fprodunsn  12286  fprodcllem  12288  sinltxirr  12443  fsumdvds  12524  dvdsle  12526  mod2eq1n2dvds  12561  bitsmod  12638  gcdsupex  12649  gcdsupcl  12650  gcdval  12651  gcddvds  12655  gcdcl  12658  gcd0id  12671  gcdneg  12674  bezoutlemmain  12690  bezoutlemzz  12694  bezoutlemaz  12695  bezoutlembz  12696  dfgcd3  12702  dfgcd2  12706  nninfctlemfo  12732  nn0seqcvgd  12734  eucalgf  12748  eucalginv  12749  dvdslcm  12762  lcmcl  12765  lcmneg  12767  lcmgcd  12771  lcmdvds  12772  lcmid  12773  mulgcddvds  12787  isprm5lem  12834  pw2dvdslemn  12858  sqrt2irrap  12873  phibndlem  12909  prm23ge5  12958  pclemdc  12982  pcxqcl  13006  pcge0  13007  pcdvdsb  13014  pceq0  13016  pcneg  13019  pcdvdstr  13021  pcgcd1  13022  pcgcd  13023  pc2dvds  13024  pcz  13026  pcprmpw2  13027  pcaddlem  13033  pcadd  13034  pcmpt  13037  pcmpt2  13038  pcprod  13040  fldivp1  13042  qexpz  13046  1arithlem4  13060  1arith  13061  4sqlem19  13103  ennnfonelemss  13153  ennnfonelemkh  13155  ennnfonelemhf1o  13156  ctiunctlemudc  13180  bassetsnn  13261  fvprif  13548  gsumfzz  13700  gsumwsubmcl  13701  gsumwmhm  13703  gsumfzcl  13704  mulgnn0p1  13842  mulgnn0subcl  13844  mulgsubcl  13845  mulgneg  13849  mulgz  13859  mulgnn0dir  13861  mulgdirlem  13862  mulgdir  13863  submmulg  13875  ghmmulg  13965  gsumfzreidx  14046  gsumfzsubmcl  14047  gsumfzmptfidmadd  14048  gsumfzmhm  14052  gsumsplit0  14055  lringuplu  14333  aprlring  14426  gsumfzfsum  14728  znf1o  14791  xblss2ps  15261  xblss2  15262  qtopbas  15379  dedekindeulemeu  15479  dedekindeu  15480  suplociccreex  15481  dedekindicclemeu  15488  dedekindicclemicc  15489  limcimolemlt  15521  cnplimclemle  15525  dvmptc  15574  reeff1o  15630  efltlemlt  15631  sin0pilem2  15639  coseq0negpitopi  15693  abssinper  15703  cos02pilt1  15708  logbgcd1irraplemexp  15825  lgslem4  15868  lgsneg  15889  lgsneg1  15890  lgsmod  15891  lgsdilem  15892  lgsdir2  15898  lgsdirprm  15899  lgsdir  15900  lgsdi  15902  lgsne0  15903  lgsdirnn0  15912  lgsdinn0  15913  gausslemma2dlem1a  15923  gausslemma2dlem1f1o  15925  gausslemma2dlem4  15929  lgseisenlem1  15935  lgsquad3  15949  2sqlem4  15983  2sqlem9  15989  eupth2lem3lem3fi  16457  eupth2lem3lem4fi  16460  eupth2lem3lem7fi  16461  nnsf  16775  nninfsellemsuc  16782  nnnninfex  16792  trilpolemclim  16812  trilpolemisumle  16814  trilpolemeq1  16816  trilpolemlt1  16817  trirec0  16820  apdifflemf  16822  apdifflemr  16823  apdiff  16824  iswomni0  16828  nconstwlpolemgt0  16841  nconstwlpolem  16842  neapmkvlem  16844  gfsumval  16853  gsumgfsum  16857