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  4286  exmidsssn  4287  exmidundif  4291  exmidundifim  4292  ordtri2or2exmidlem  4619  reg2exmidlema  4627  nnpredcl  4716  frecabcl  6556  nnsucuniel  6654  dcdifsnid  6663  pw2f1odclem  7008  phpm  7040  fidifsnen  7045  dif1enen  7055  fin0  7060  fimax2gtrilemstep  7076  finexdc  7078  elssdc  7080  eqsndc  7081  en2eqpr  7085  fientri3  7093  unsnfidcex  7098  unsnfidcel  7099  undifdcss  7101  prfidceq  7106  tpfidceq  7108  fiintim  7109  ssfirab  7114  fidcenumlemrks  7136  fidcenumlemr  7138  omp1eomlem  7277  difinfsnlem  7282  difinfsn  7283  ctssdccl  7294  ctssdc  7296  enumct  7298  nninfninc  7306  nnnninf  7309  nnnninfeq  7311  nnnninfeq2  7312  nninfisol  7316  finomni  7323  ismkvnex  7338  nninfwlpoimlemg  7358  pr2cv1  7384  exmidfodomrlemeldju  7393  exmidfodomrlemreseldju  7394  exmidfodomrlemr  7396  exmidfodomrlemrALT  7397  exmidaclem  7406  exmidontriimlem3  7421  netap  7456  2omotaplemap  7459  mullocprlem  7773  recexprlemloc  7834  suplocsrlem  8011  btwnapz  9593  xnn0dcle  10015  xnn0letri  10016  z2ge  10039  xaddcom  10074  xnegdi  10081  xaddass  10082  xpncan  10084  xleadd1a  10086  xsubge0  10094  xlesubadd  10096  fztri3or  10252  fzm1  10313  fzneuz  10314  exfzdc  10463  zsupcllemstep  10466  infssuzex  10470  exbtwnzlemstep  10484  rebtwn2zlemstep  10489  xqltnle  10504  apbtwnz  10511  modifeq2int  10625  modsumfzodifsn  10635  iseqf1olemab  10741  iseqf1olemmo  10744  seq3f1olemqsumk  10751  seq3f1olemqsum  10752  seq3f1olemstep  10753  seqf1oglem1  10758  seqf1oglem2  10759  fser0const  10774  expaddzaplem  10821  qsqeqor  10889  expnbnd  10902  nn0ltexp2  10948  apexp1  10957  bcval  10988  bccmpl  10993  bcval5  11002  bcpasc  11005  bccl  11006  hashennnuni  11018  hashnncl  11034  fiubm  11068  zfz1isolemiso  11079  lswex  11141  ccatsymb  11155  ccat1st1st  11193  fzowrddc  11200  swrd0g  11213  swrdsbslen  11219  swrdspsleq  11220  pfxclz  11232  pfxwrdsymbg  11243  swrdccatin1  11278  resqrexlemnm  11550  resqrexlemcvg  11551  resqrexlemoverl  11553  resqrexlemglsq  11554  leabs  11606  nn0abscl  11617  ltabs  11619  abslt  11620  fzomaxdif  11645  maxleim  11737  maxabslemval  11740  zmaxcl  11756  2zsupmax  11758  minmax  11762  2zinfmin  11775  xrmaxleim  11776  xrmaxifle  11778  xrmaxiflemab  11779  xrmaxiflemlub  11780  xrmaxiflemcom  11781  xrmaxiflemval  11782  xrmaxaddlem  11792  xrmaxadd  11793  xrminmax  11797  sumdc  11890  sumrbdc  11911  summodclem3  11912  summodclem2a  11913  zsumdc  11916  isumss  11923  fisumss  11924  isumss2  11925  fsumcllem  11931  fsumadd  11938  fsumsplit  11939  fsumsplitsn  11942  sumsplitdc  11964  fisumrev2  11978  fsummulc2  11980  telfsumo  11998  fsumparts  12002  cvgratnnlemseq  12058  cvgratz  12064  fproddccvg  12104  prodrbdc  12106  zproddc  12111  prod1dc  12118  fprodssdc  12122  fprodmul  12123  fprodsplitdc  12128  fprodsplit  12129  fprodunsn  12136  fprodcllem  12138  sinltxirr  12293  fsumdvds  12374  dvdsle  12376  mod2eq1n2dvds  12411  bitsmod  12488  gcdsupex  12499  gcdsupcl  12500  gcdval  12501  gcddvds  12505  gcdcl  12508  gcd0id  12521  gcdneg  12524  bezoutlemmain  12540  bezoutlemzz  12544  bezoutlemaz  12545  bezoutlembz  12546  dfgcd3  12552  dfgcd2  12556  nninfctlemfo  12582  nn0seqcvgd  12584  eucalgf  12598  eucalginv  12599  dvdslcm  12612  lcmcl  12615  lcmneg  12617  lcmgcd  12621  lcmdvds  12622  lcmid  12623  mulgcddvds  12637  isprm5lem  12684  pw2dvdslemn  12708  sqrt2irrap  12723  phibndlem  12759  prm23ge5  12808  pclemdc  12832  pcxqcl  12856  pcge0  12857  pcdvdsb  12864  pceq0  12866  pcneg  12869  pcdvdstr  12871  pcgcd1  12872  pcgcd  12873  pc2dvds  12874  pcz  12876  pcprmpw2  12877  pcaddlem  12883  pcadd  12884  pcmpt  12887  pcmpt2  12888  pcprod  12890  fldivp1  12892  qexpz  12896  1arithlem4  12910  1arith  12911  4sqlem19  12953  ennnfonelemss  13002  ennnfonelemkh  13004  ennnfonelemhf1o  13005  ctiunctlemudc  13029  bassetsnn  13110  fvprif  13397  gsumfzz  13549  gsumwsubmcl  13550  gsumwmhm  13552  gsumfzcl  13553  mulgnn0p1  13691  mulgnn0subcl  13693  mulgsubcl  13694  mulgneg  13698  mulgz  13708  mulgnn0dir  13710  mulgdirlem  13711  mulgdir  13712  submmulg  13724  ghmmulg  13814  gsumfzreidx  13895  gsumfzsubmcl  13896  gsumfzmptfidmadd  13897  gsumfzmhm  13901  lringuplu  14181  gsumfzfsum  14573  znf1o  14636  xblss2ps  15099  xblss2  15100  qtopbas  15217  dedekindeulemeu  15317  dedekindeu  15318  suplociccreex  15319  dedekindicclemeu  15326  dedekindicclemicc  15327  limcimolemlt  15359  cnplimclemle  15363  dvmptc  15412  reeff1o  15468  efltlemlt  15469  sin0pilem2  15477  coseq0negpitopi  15531  abssinper  15541  cos02pilt1  15546  logbgcd1irraplemexp  15663  lgslem4  15703  lgsneg  15724  lgsneg1  15725  lgsmod  15726  lgsdilem  15727  lgsdir2  15733  lgsdirprm  15734  lgsdir  15735  lgsdi  15737  lgsne0  15738  lgsdirnn0  15747  lgsdinn0  15748  gausslemma2dlem1a  15758  gausslemma2dlem1f1o  15760  gausslemma2dlem4  15764  lgseisenlem1  15770  lgsquad3  15784  2sqlem4  15818  2sqlem9  15824  2omap  16472  nnsf  16485  nninfsellemsuc  16492  nnnninfex  16502  trilpolemclim  16518  trilpolemisumle  16520  trilpolemeq1  16522  trilpolemlt1  16523  trirec0  16526  apdifflemf  16528  apdifflemr  16529  apdiff  16530  iswomni0  16533  nconstwlpolemgt0  16546  nconstwlpolem  16547  neapmkvlem  16549