Theorem mpjaodan 798

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

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

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 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjao3dan  1307  dcun  3535  ifcldadc  3565  ifeq1dadc  3566  ifeq2dadc  3567  ifbothdadc  3568  ifcldcd  3572  exmidn0m  4203  exmidsssn  4204  exmidundif  4208  exmidundifim  4209  ordtri2or2exmidlem  4527  reg2exmidlema  4535  nnpredcl  4624  frecabcl  6402  nnsucuniel  6498  dcdifsnid  6507  phpm  6867  fidifsnen  6872  dif1enen  6882  fin0  6887  fimax2gtrilemstep  6902  finexdc  6904  en2eqpr  6909  fientri3  6916  unsnfidcex  6921  unsnfidcel  6922  undifdcss  6924  fiintim  6930  ssfirab  6935  fidcenumlemrks  6954  fidcenumlemr  6956  omp1eomlem  7095  difinfsnlem  7100  difinfsn  7101  ctssdccl  7112  ctssdc  7114  enumct  7116  nnnninf  7126  nnnninfeq  7128  nnnninfeq2  7129  nninfisol  7133  finomni  7140  ismkvnex  7155  nninfwlpoimlemg  7175  exmidfodomrlemeldju  7200  exmidfodomrlemreseldju  7201  exmidfodomrlemr  7203  exmidfodomrlemrALT  7204  exmidaclem  7209  exmidontriimlem3  7224  netap  7255  2omotaplemap  7258  mullocprlem  7571  recexprlemloc  7632  suplocsrlem  7809  btwnapz  9385  xnn0dcle  9804  xnn0letri  9805  z2ge  9828  xaddcom  9863  xnegdi  9870  xaddass  9871  xpncan  9873  xleadd1a  9875  xsubge0  9883  xlesubadd  9885  fztri3or  10041  fzm1  10102  fzneuz  10103  exfzdc  10242  exbtwnzlemstep  10250  rebtwn2zlemstep  10255  apbtwnz  10276  modifeq2int  10388  modsumfzodifsn  10398  iseqf1olemab  10491  iseqf1olemmo  10494  seq3f1olemqsumk  10501  seq3f1olemqsum  10502  seq3f1olemstep  10503  fser0const  10518  expaddzaplem  10565  qsqeqor  10633  expnbnd  10646  nn0ltexp2  10691  apexp1  10700  bcval  10731  bccmpl  10736  bcval5  10745  bcpasc  10748  bccl  10749  hashennnuni  10761  hashnncl  10777  fiubm  10810  zfz1isolemiso  10821  resqrexlemnm  11029  resqrexlemcvg  11030  resqrexlemoverl  11032  resqrexlemglsq  11033  leabs  11085  nn0abscl  11096  ltabs  11098  abslt  11099  fzomaxdif  11124  maxleim  11216  maxabslemval  11219  zmaxcl  11235  2zsupmax  11236  minmax  11240  2zinfmin  11253  xrmaxleim  11254  xrmaxifle  11256  xrmaxiflemab  11257  xrmaxiflemlub  11258  xrmaxiflemcom  11259  xrmaxiflemval  11260  xrmaxaddlem  11270  xrmaxadd  11271  xrminmax  11275  sumdc  11368  sumrbdc  11389  summodclem3  11390  summodclem2a  11391  zsumdc  11394  isumss  11401  fisumss  11402  isumss2  11403  fsumcllem  11409  fsumadd  11416  fsumsplit  11417  fsumsplitsn  11420  sumsplitdc  11442  fisumrev2  11456  fsummulc2  11458  telfsumo  11476  fsumparts  11480  cvgratnnlemseq  11536  cvgratz  11542  fproddccvg  11582  prodrbdc  11584  zproddc  11589  prod1dc  11596  fprodssdc  11600  fprodmul  11601  fprodsplitdc  11606  fprodsplit  11607  fprodunsn  11614  fprodcllem  11616  dvdsle  11852  mod2eq1n2dvds  11886  zsupcllemstep  11948  infssuzex  11952  gcdsupex  11960  gcdsupcl  11961  gcdval  11962  gcddvds  11966  gcdcl  11969  gcd0id  11982  gcdneg  11985  bezoutlemmain  12001  bezoutlemzz  12005  bezoutlemaz  12006  bezoutlembz  12007  dfgcd3  12013  dfgcd2  12017  nn0seqcvgd  12043  eucalgf  12057  eucalginv  12058  dvdslcm  12071  lcmcl  12074  lcmneg  12076  lcmgcd  12080  lcmdvds  12081  lcmid  12082  mulgcddvds  12096  isprm5lem  12143  pw2dvdslemn  12167  sqrt2irrap  12182  phibndlem  12218  prm23ge5  12266  pclemdc  12290  pcge0  12314  pcdvdsb  12321  pceq0  12323  pcneg  12326  pcdvdstr  12328  pcgcd1  12329  pcgcd  12330  pc2dvds  12331  pcz  12333  pcprmpw2  12334  pcaddlem  12340  pcadd  12341  pcmpt  12343  pcmpt2  12344  pcprod  12346  fldivp1  12348  qexpz  12352  1arithlem4  12366  1arith  12367  ennnfonelemss  12413  ennnfonelemkh  12415  ennnfonelemhf1o  12416  ctiunctlemudc  12440  fvprif  12767  mulgnn0p1  12999  mulgnn0subcl  13001  mulgsubcl  13002  mulgneg  13006  mulgz  13016  mulgnn0dir  13018  mulgdirlem  13019  mulgdir  13020  lringuplu  13342  xblss2ps  13989  xblss2  13990  qtopbas  14107  dedekindeulemeu  14185  dedekindeu  14186  suplociccreex  14187  dedekindicclemeu  14194  dedekindicclemicc  14195  limcimolemlt  14218  cnplimclemle  14222  reeff1o  14279  efltlemlt  14280  sin0pilem2  14288  coseq0negpitopi  14342  abssinper  14352  cos02pilt1  14357  logbgcd1irraplemexp  14471  lgslem4  14489  lgsneg  14510  lgsneg1  14511  lgsmod  14512  lgsdilem  14513  lgsdir2  14519  lgsdirprm  14520  lgsdir  14521  lgsdi  14523  lgsne0  14524  lgsdirnn0  14533  lgsdinn0  14534  lgseisenlem1  14535  2sqlem4  14550  2sqlem9  14556  nnsf  14839  nninfsellemsuc  14846  trilpolemclim  14869  trilpolemisumle  14871  trilpolemeq1  14873  trilpolemlt1  14874  trirec0  14877  apdifflemf  14879  apdifflemr  14880  apdiff  14881  iswomni0  14884  nconstwlpolemgt0  14897  nconstwlpolem  14898  neapmkvlem  14900