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  4285  exmidsssn  4286  exmidundif  4290  exmidundifim  4291  ordtri2or2exmidlem  4618  reg2exmidlema  4626  nnpredcl  4715  frecabcl  6551  nnsucuniel  6649  dcdifsnid  6658  pw2f1odclem  7003  phpm  7035  fidifsnen  7040  dif1enen  7050  fin0  7055  fimax2gtrilemstep  7070  finexdc  7072  en2eqpr  7077  fientri3  7085  unsnfidcex  7090  unsnfidcel  7091  undifdcss  7093  prfidceq  7098  tpfidceq  7100  fiintim  7101  ssfirab  7106  fidcenumlemrks  7128  fidcenumlemr  7130  omp1eomlem  7269  difinfsnlem  7274  difinfsn  7275  ctssdccl  7286  ctssdc  7288  enumct  7290  nninfninc  7298  nnnninf  7301  nnnninfeq  7303  nnnninfeq2  7304  nninfisol  7308  finomni  7315  ismkvnex  7330  nninfwlpoimlemg  7350  pr2cv1  7376  exmidfodomrlemeldju  7385  exmidfodomrlemreseldju  7386  exmidfodomrlemr  7388  exmidfodomrlemrALT  7389  exmidaclem  7398  exmidontriimlem3  7413  netap  7448  2omotaplemap  7451  mullocprlem  7765  recexprlemloc  7826  suplocsrlem  8003  btwnapz  9585  xnn0dcle  10006  xnn0letri  10007  z2ge  10030  xaddcom  10065  xnegdi  10072  xaddass  10073  xpncan  10075  xleadd1a  10077  xsubge0  10085  xlesubadd  10087  fztri3or  10243  fzm1  10304  fzneuz  10305  exfzdc  10454  zsupcllemstep  10457  infssuzex  10461  exbtwnzlemstep  10475  rebtwn2zlemstep  10480  xqltnle  10495  apbtwnz  10502  modifeq2int  10616  modsumfzodifsn  10626  iseqf1olemab  10732  iseqf1olemmo  10735  seq3f1olemqsumk  10742  seq3f1olemqsum  10743  seq3f1olemstep  10744  seqf1oglem1  10749  seqf1oglem2  10750  fser0const  10765  expaddzaplem  10812  qsqeqor  10880  expnbnd  10893  nn0ltexp2  10939  apexp1  10948  bcval  10979  bccmpl  10984  bcval5  10993  bcpasc  10996  bccl  10997  hashennnuni  11009  hashnncl  11025  fiubm  11058  zfz1isolemiso  11069  lswex  11131  ccatsymb  11145  ccat1st1st  11180  fzowrddc  11187  swrd0g  11200  swrdsbslen  11206  swrdspsleq  11207  pfxclz  11219  pfxwrdsymbg  11230  swrdccatin1  11265  resqrexlemnm  11537  resqrexlemcvg  11538  resqrexlemoverl  11540  resqrexlemglsq  11541  leabs  11593  nn0abscl  11604  ltabs  11606  abslt  11607  fzomaxdif  11632  maxleim  11724  maxabslemval  11727  zmaxcl  11743  2zsupmax  11745  minmax  11749  2zinfmin  11762  xrmaxleim  11763  xrmaxifle  11765  xrmaxiflemab  11766  xrmaxiflemlub  11767  xrmaxiflemcom  11768  xrmaxiflemval  11769  xrmaxaddlem  11779  xrmaxadd  11780  xrminmax  11784  sumdc  11877  sumrbdc  11898  summodclem3  11899  summodclem2a  11900  zsumdc  11903  isumss  11910  fisumss  11911  isumss2  11912  fsumcllem  11918  fsumadd  11925  fsumsplit  11926  fsumsplitsn  11929  sumsplitdc  11951  fisumrev2  11965  fsummulc2  11967  telfsumo  11985  fsumparts  11989  cvgratnnlemseq  12045  cvgratz  12051  fproddccvg  12091  prodrbdc  12093  zproddc  12098  prod1dc  12105  fprodssdc  12109  fprodmul  12110  fprodsplitdc  12115  fprodsplit  12116  fprodunsn  12123  fprodcllem  12125  sinltxirr  12280  fsumdvds  12361  dvdsle  12363  mod2eq1n2dvds  12398  bitsmod  12475  gcdsupex  12486  gcdsupcl  12487  gcdval  12488  gcddvds  12492  gcdcl  12495  gcd0id  12508  gcdneg  12511  bezoutlemmain  12527  bezoutlemzz  12531  bezoutlemaz  12532  bezoutlembz  12533  dfgcd3  12539  dfgcd2  12543  nninfctlemfo  12569  nn0seqcvgd  12571  eucalgf  12585  eucalginv  12586  dvdslcm  12599  lcmcl  12602  lcmneg  12604  lcmgcd  12608  lcmdvds  12609  lcmid  12610  mulgcddvds  12624  isprm5lem  12671  pw2dvdslemn  12695  sqrt2irrap  12710  phibndlem  12746  prm23ge5  12795  pclemdc  12819  pcxqcl  12843  pcge0  12844  pcdvdsb  12851  pceq0  12853  pcneg  12856  pcdvdstr  12858  pcgcd1  12859  pcgcd  12860  pc2dvds  12861  pcz  12863  pcprmpw2  12864  pcaddlem  12870  pcadd  12871  pcmpt  12874  pcmpt2  12875  pcprod  12877  fldivp1  12879  qexpz  12883  1arithlem4  12897  1arith  12898  4sqlem19  12940  ennnfonelemss  12989  ennnfonelemkh  12991  ennnfonelemhf1o  12992  ctiunctlemudc  13016  bassetsnn  13097  fvprif  13384  gsumfzz  13536  gsumwsubmcl  13537  gsumwmhm  13539  gsumfzcl  13540  mulgnn0p1  13678  mulgnn0subcl  13680  mulgsubcl  13681  mulgneg  13685  mulgz  13695  mulgnn0dir  13697  mulgdirlem  13698  mulgdir  13699  submmulg  13711  ghmmulg  13801  gsumfzreidx  13882  gsumfzsubmcl  13883  gsumfzmptfidmadd  13884  gsumfzmhm  13888  lringuplu  14168  gsumfzfsum  14560  znf1o  14623  xblss2ps  15086  xblss2  15087  qtopbas  15204  dedekindeulemeu  15304  dedekindeu  15305  suplociccreex  15306  dedekindicclemeu  15313  dedekindicclemicc  15314  limcimolemlt  15346  cnplimclemle  15350  dvmptc  15399  reeff1o  15455  efltlemlt  15456  sin0pilem2  15464  coseq0negpitopi  15518  abssinper  15528  cos02pilt1  15533  logbgcd1irraplemexp  15650  lgslem4  15690  lgsneg  15711  lgsneg1  15712  lgsmod  15713  lgsdilem  15714  lgsdir2  15720  lgsdirprm  15721  lgsdir  15722  lgsdi  15724  lgsne0  15725  lgsdirnn0  15734  lgsdinn0  15735  gausslemma2dlem1a  15745  gausslemma2dlem1f1o  15747  gausslemma2dlem4  15751  lgseisenlem1  15757  lgsquad3  15771  2sqlem4  15805  2sqlem9  15811  2omap  16388  nnsf  16401  nninfsellemsuc  16408  nnnninfex  16418  trilpolemclim  16434  trilpolemisumle  16436  trilpolemeq1  16438  trilpolemlt1  16439  trirec0  16442  apdifflemf  16444  apdifflemr  16445  apdiff  16446  iswomni0  16449  nconstwlpolemgt0  16462  nconstwlpolem  16463  neapmkvlem  16465