Theorem mpjaodan 810

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  mpjao3dan  1348  dcun  3637  ifcldadc  3670  ifeq1dadc  3671  ifeq2dadc  3672  ifeqdadc  3673  ifbothdadc  3674  ifcldcd  3678  2if2dc  3680  ifeqeqxdc  3687  exmidn0m  4338  exmidsssn  4339  exmidundif  4343  exmidundifim  4344  ordtri2or2exmidlem  4673  reg2exmidlema  4681  nnpredcl  4770  frecabcl  6670  nnsucuniel  6768  dcdifsnid  6777  pw2f1odclem  7134  phpm  7167  fidifsnen  7172  dif1enen  7184  fin0  7189  fimax2gtrilemstep  7205  finexdc  7207  elssdc  7209  eqsndc  7210  en2eqpr  7214  fientri3  7222  unsnfidcex  7227  unsnfidcel  7228  undifdcss  7230  prfidceq  7235  tpfidceq  7237  fiintim  7238  ssfirab  7244  fidcenumlemrks  7270  fidcenumlemr  7272  2omap  7319  omp1eomlem  7435  difinfsnlem  7440  difinfsn  7441  ctssdccl  7452  ctssdc  7454  enumct  7456  nninfninc  7464  nnnninf  7467  nnnninfeq  7469  nnnninfeq2  7470  nninfisol  7474  finomni  7481  ismkvnex  7496  nninfwlpoimlemg  7516  pr2cv1  7542  exmidfodomrlemeldju  7552  exmidfodomrlemreseldju  7553  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  exmidaclem  7565  exmidontriimlem3  7580  netap  7621  2omotaplemap  7624  mullocprlem  7938  recexprlemloc  7999  suplocsrlem  8176  btwnapz  9781  xnn0dcle  10215  xnn0letri  10216  z2ge  10239  xaddcom  10274  xnegdi  10281  xaddass  10282  xpncan  10284  xleadd1a  10286  xsubge0  10294  xlesubadd  10296  fztri3or  10454  fzm1  10518  fzneuz  10519  exfzdc  10670  zsupcllemstep  10673  infssuzex  10677  exbtwnzlemstep  10693  rebtwn2zlemstep  10698  xqltnle  10713  apbtwnz  10720  modifeq2int  10837  modsumfzodifsn  10847  iseqf1olemab  10953  iseqf1olemmo  10956  seq3f1olemqsumk  10963  seq3f1olemqsum  10964  seq3f1olemstep  10965  seqf1oglem1  10970  seqf1oglem2  10971  fser0const  10986  expaddzaplem  11033  qsqeqor  11101  resq01  11109  expnbnd  11115  nn0ltexp2  11162  apexp1  11171  bcval  11202  bccmpl  11207  bcval5  11216  bcpasc  11219  bccl  11220  hashennnuni  11233  hashnncl  11249  fiubm  11286  hashfibc  11298  hashf1  11302  zfz1isolemiso  11306  lswex  11371  ccatsymb  11385  ccat1st1st  11424  fzowrddc  11434  swrd0g  11447  swrdsbslen  11453  swrdspsleq  11454  pfxclz  11466  pfxwrdsymbg  11477  swrdccatin1  11512  resqrexlemnm  11799  resqrexlemcvg  11800  resqrexlemoverl  11802  resqrexlemglsq  11803  leabs  11855  qabscl  11858  nn0abscl  11867  ltabs  11869  abslt  11870  fzomaxdif  11895  maxleim  11987  maxabslemval  11990  zmaxcl  12006  2zsupmax  12008  minmax  12013  zmincl  12022  2zinfmin  12027  xrmaxleim  12028  xrmaxifle  12030  xrmaxiflemab  12031  xrmaxiflemlub  12032  xrmaxiflemcom  12033  xrmaxiflemval  12034  xrmaxaddlem  12044  xrmaxadd  12045  xrminmax  12049  sumdc  12142  fzf1o  12160  sumrbdc  12164  summodclem3  12165  summodclem2a  12166  zsumdc  12169  isumss  12176  fisumss  12177  isumss2  12178  fsumcllem  12184  fsumadd  12191  fsumsplit  12192  fsumsplitsn  12195  sumsplitdc  12217  fisumrev2  12231  fsummulc2  12233  telfsumo  12251  fsumparts  12255  cvgratnnlemseq  12311  cvgratz  12317  fproddccvg  12357  prodrbdc  12359  zproddc  12364  prod1dc  12371  fprodssdc  12375  fprodmul  12376  fprodsplitdc  12381  fprodsplit  12382  fprodunsn  12389  fprodcllem  12391  sinltxirr  12546  fsumdvds  12627  dvdsle  12629  mod2eq1n2dvds  12664  bitsmod  12741  gcdsupex  12752  gcdsupcl  12753  gcdval  12754  gcddvds  12758  gcdcl  12761  gcd0id  12774  gcdneg  12777  bezoutlemmain  12793  bezoutlemzz  12797  bezoutlemaz  12798  bezoutlembz  12799  dfgcd3  12805  dfgcd2  12809  nninfctlemfo  12835  nn0seqcvgd  12837  eucalgf  12851  eucalginv  12852  dvdslcm  12865  lcmcl  12868  lcmneg  12870  lcmgcd  12874  lcmdvds  12875  lcmid  12876  mulgcddvds  12890  prmdcz  12927  isprm5lem  12938  pwbdvdslemn  12962  sqrt2irrap  12978  sqrtrirr  13007  phibndlem  13016  prm23ge5  13065  pclemdc  13089  pcxqcl  13113  pcge0  13114  pcdvdsb  13121  pceq0  13123  pcneg  13126  pcdvdstr  13128  pcgcd1  13129  pcgcd  13130  pc2dvds  13131  pcz  13133  pcprmpw2  13134  pcaddlem  13140  pcadd  13141  pcmpt  13144  pcmpt2  13145  pcprod  13147  fldivp1  13149  qexpz  13153  1arithlem4  13167  1arith  13168  4sqlem19  13210  ennnfonelemss  13352  ennnfonelemkh  13354  ennnfonelemhf1o  13355  ctiunctlemudc  13379  bassetsnn  13460  fvprif  13715  gzsumwsubmcl  13852  gzsumwmhm  13854  gzsumcl  13855  mulgnn0p1  13987  mulgnn0subcl  13989  mulgsubcl  13990  mulgneg  13994  mulgz  14004  mulgnn0dir  14006  mulgdirlem  14007  mulgdir  14008  submmulg  14020  ghmmulg  14110  gzsumreidx  14192  gzsumsubmcl  14193  gzsummhm  14196  gzsumsplit0  14199  gsumvalfi  14203  gzsumgsum  14206  lringuplu  14554  aprlring  14651  znf1o  15037  xblss2ps  15557  xblss2  15558  qtopbas  15675  dedekindeulemeu  15775  dedekindeu  15776  suplociccreex  15777  dedekindicclemeu  15784  dedekindicclemicc  15785  limcimolemlt  15817  cnplimclemle  15821  dvmptc  15870  reeff1o  15926  efltlemlt  15927  efap1p  15932  sin0pilem2  15936  coseq0negpitopi  15990  abssinper  16000  cos02pilt1  16005  logdivlt  16049  logbgcd1irraplemexp  16126  birthdaylem2  16148  birthdaylem3  16149  ppiqp1le  16189  ppiqltx  16203  ppiqub  16215  chtqub  16218  bcmono  16226  bcmax  16227  bposlem3  16235  bposlem5  16237  lgslem4  16244  lgsneg  16265  lgsneg1  16266  lgsmod  16267  lgsdilem  16268  lgsdir2  16274  lgsdirprm  16275  lgsdir  16276  lgsdi  16278  lgsne0  16279  lgsdirnn0  16288  lgsdinn0  16289  gausslemma2dlem1a  16299  gausslemma2dlem1f1o  16301  gausslemma2dlem4  16305  lgseisenlem1  16311  lgsquad3  16325  2sqlem4  16359  2sqlem9  16365  eupth2lem3lem3fi  16833  eupth2lem3lem4fi  16836  eupth2lem3lem7fi  16837  dichmul0orlem3  16877  dichmul0orlem7  16881  nnsf  17170  nninfsellemsuc  17177  nnnninfex  17187  trilpolemclim  17207  trilpolemisumle  17209  trilpolemeq1  17211  trilpolemlt1  17212  trirec0  17215  apdifflemf  17217  apdifflemr  17218  apdiff  17219  iswomni0  17223  nconstwlpolemgt0  17236  nconstwlpolem  17237  neapmkvlem  17239