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  3531  ifcldadc  3561  ifeq1dadc  3562  ifbothdadc  3563  ifcldcd  3567  exmidn0m  4196  exmidsssn  4197  exmidundif  4201  exmidundifim  4202  ordtri2or2exmidlem  4519  reg2exmidlema  4527  nnpredcl  4616  frecabcl  6390  nnsucuniel  6486  dcdifsnid  6495  phpm  6855  fidifsnen  6860  dif1enen  6870  fin0  6875  fimax2gtrilemstep  6890  finexdc  6892  en2eqpr  6897  fientri3  6904  unsnfidcex  6909  unsnfidcel  6910  undifdcss  6912  fiintim  6918  ssfirab  6923  fidcenumlemrks  6942  fidcenumlemr  6944  omp1eomlem  7083  difinfsnlem  7088  difinfsn  7089  ctssdccl  7100  ctssdc  7102  enumct  7104  nnnninf  7114  nnnninfeq  7116  nnnninfeq2  7117  nninfisol  7121  finomni  7128  ismkvnex  7143  nninfwlpoimlemg  7163  exmidfodomrlemeldju  7188  exmidfodomrlemreseldju  7189  exmidfodomrlemr  7191  exmidfodomrlemrALT  7192  exmidaclem  7197  exmidontriimlem3  7212  mullocprlem  7544  recexprlemloc  7605  suplocsrlem  7782  btwnapz  9356  xnn0dcle  9773  xnn0letri  9774  z2ge  9797  xaddcom  9832  xnegdi  9839  xaddass  9840  xpncan  9842  xleadd1a  9844  xsubge0  9852  xlesubadd  9854  fztri3or  10009  fzm1  10070  fzneuz  10071  exfzdc  10210  exbtwnzlemstep  10218  rebtwn2zlemstep  10223  apbtwnz  10244  modifeq2int  10356  modsumfzodifsn  10366  iseqf1olemab  10459  iseqf1olemmo  10462  seq3f1olemqsumk  10469  seq3f1olemqsum  10470  seq3f1olemstep  10471  fser0const  10486  expaddzaplem  10533  qsqeqor  10600  expnbnd  10613  nn0ltexp2  10658  apexp1  10666  bcval  10697  bccmpl  10702  bcval5  10711  bcpasc  10714  bccl  10715  hashennnuni  10727  hashnncl  10743  fiubm  10776  zfz1isolemiso  10787  resqrexlemnm  10995  resqrexlemcvg  10996  resqrexlemoverl  10998  resqrexlemglsq  10999  leabs  11051  nn0abscl  11062  ltabs  11064  abslt  11065  fzomaxdif  11090  maxleim  11182  maxabslemval  11185  zmaxcl  11201  2zsupmax  11202  minmax  11206  2zinfmin  11219  xrmaxleim  11220  xrmaxifle  11222  xrmaxiflemab  11223  xrmaxiflemlub  11224  xrmaxiflemcom  11225  xrmaxiflemval  11226  xrmaxaddlem  11236  xrmaxadd  11237  xrminmax  11241  sumdc  11334  sumrbdc  11355  summodclem3  11356  summodclem2a  11357  zsumdc  11360  isumss  11367  fisumss  11368  isumss2  11369  fsumcllem  11375  fsumadd  11382  fsumsplit  11383  fsumsplitsn  11386  sumsplitdc  11408  fisumrev2  11422  fsummulc2  11424  telfsumo  11442  fsumparts  11446  cvgratnnlemseq  11502  cvgratz  11508  fproddccvg  11548  prodrbdc  11550  zproddc  11555  prod1dc  11562  fprodssdc  11566  fprodmul  11567  fprodsplitdc  11572  fprodsplit  11573  fprodunsn  11580  fprodcllem  11582  dvdsle  11817  mod2eq1n2dvds  11851  zsupcllemstep  11913  infssuzex  11917  gcdsupex  11925  gcdsupcl  11926  gcdval  11927  gcddvds  11931  gcdcl  11934  gcd0id  11947  gcdneg  11950  bezoutlemmain  11966  bezoutlemzz  11970  bezoutlemaz  11971  bezoutlembz  11972  dfgcd3  11978  dfgcd2  11982  nn0seqcvgd  12008  eucalgf  12022  eucalginv  12023  dvdslcm  12036  lcmcl  12039  lcmneg  12041  lcmgcd  12045  lcmdvds  12046  lcmid  12047  mulgcddvds  12061  isprm5lem  12108  pw2dvdslemn  12132  sqrt2irrap  12147  phibndlem  12183  prm23ge5  12231  pclemdc  12255  pcge0  12279  pcdvdsb  12286  pceq0  12288  pcneg  12291  pcdvdstr  12293  pcgcd1  12294  pcgcd  12295  pc2dvds  12296  pcz  12298  pcprmpw2  12299  pcaddlem  12305  pcadd  12306  pcmpt  12308  pcmpt2  12309  pcprod  12311  fldivp1  12313  qexpz  12317  1arithlem4  12331  1arith  12332  ennnfonelemss  12378  ennnfonelemkh  12380  ennnfonelemhf1o  12381  ctiunctlemudc  12405  mulgnn0p1  12855  mulgnn0subcl  12857  mulgsubcl  12858  mulgneg  12862  mulgz  12871  mulgnn0dir  12873  mulgdirlem  12874  mulgdir  12875  xblss2ps  13475  xblss2  13476  qtopbas  13593  dedekindeulemeu  13671  dedekindeu  13672  suplociccreex  13673  dedekindicclemeu  13680  dedekindicclemicc  13681  limcimolemlt  13704  cnplimclemle  13708  reeff1o  13765  efltlemlt  13766  sin0pilem2  13774  coseq0negpitopi  13828  abssinper  13838  cos02pilt1  13843  logbgcd1irraplemexp  13957  lgslem4  13975  lgsneg  13996  lgsneg1  13997  lgsmod  13998  lgsdilem  13999  lgsdir2  14005  lgsdirprm  14006  lgsdir  14007  lgsdi  14009  lgsne0  14010  lgsdirnn0  14019  lgsdinn0  14020  2sqlem4  14025  2sqlem9  14031  nnsf  14315  nninfsellemsuc  14322  trilpolemclim  14345  trilpolemisumle  14347  trilpolemeq1  14349  trilpolemlt1  14350  trirec0  14353  apdifflemf  14355  apdifflemr  14356  apdiff  14357  iswomni0  14360  nconstwlpolemgt0  14372  nconstwlpolem  14373  neapmkvlem  14375