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  flaplt  10733  modifeq2int  10838  modsumfzodifsn  10848  iseqf1olemab  10954  iseqf1olemmo  10957  seq3f1olemqsumk  10964  seq3f1olemqsum  10965  seq3f1olemstep  10966  seqf1oglem1  10971  seqf1oglem2  10972  fser0const  10987  expaddzaplem  11034  qsqeqor  11102  resq01  11110  expnbnd  11116  nn0ltexp2  11163  apexp1  11172  bcval  11203  bccmpl  11208  bcval5  11217  bcpasc  11220  bccl  11221  hashennnuni  11234  hashnncl  11250  fiubm  11287  hashfibc  11299  hashf1  11303  zfz1isolemiso  11307  lswex  11372  ccatsymb  11386  ccat1st1st  11425  fzowrddc  11435  swrd0g  11448  swrdsbslen  11454  swrdspsleq  11455  pfxclz  11467  pfxwrdsymbg  11478  swrdccatin1  11513  resqrexlemnm  11800  resqrexlemcvg  11801  resqrexlemoverl  11803  resqrexlemglsq  11804  leabs  11856  qabscl  11859  nn0abscl  11868  ltabs  11870  abslt  11871  fzomaxdif  11896  maxleim  11988  maxabslemval  11991  zmaxcl  12007  2zsupmax  12009  minmax  12014  zmincl  12023  2zinfmin  12028  xrmaxleim  12029  xrmaxifle  12031  xrmaxiflemab  12032  xrmaxiflemlub  12033  xrmaxiflemcom  12034  xrmaxiflemval  12035  xrmaxaddlem  12045  xrmaxadd  12046  xrminmax  12050  sumdc  12143  fzf1o  12161  sumrbdc  12165  summodclem3  12166  summodclem2a  12167  zsumdc  12170  isumss  12177  fisumss  12178  isumss2  12179  fsumcllem  12185  fsumadd  12192  fsumsplit  12193  fsumsplitsn  12196  sumsplitdc  12218  fisumrev2  12232  fsummulc2  12234  telfsumo  12252  fsumparts  12256  cvgratnnlemseq  12312  cvgratz  12318  fproddccvg  12358  prodrbdc  12360  zproddc  12365  prod1dc  12372  fprodssdc  12376  fprodmul  12377  fprodsplitdc  12382  fprodsplit  12383  fprodunsn  12390  fprodcllem  12392  sinltxirr  12547  fsumdvds  12628  dvdsle  12630  mod2eq1n2dvds  12665  bitsmod  12742  gcdsupex  12753  gcdsupcl  12754  gcdval  12755  gcddvds  12759  gcdcl  12762  gcd0id  12775  gcdneg  12778  bezoutlemmain  12794  bezoutlemzz  12798  bezoutlemaz  12799  bezoutlembz  12800  dfgcd3  12806  dfgcd2  12810  nninfctlemfo  12836  nn0seqcvgd  12838  eucalgf  12852  eucalginv  12853  dvdslcm  12866  lcmcl  12869  lcmneg  12871  lcmgcd  12875  lcmdvds  12876  lcmid  12877  mulgcddvds  12891  prmdcz  12928  isprm5lem  12939  pwbdvdslemn  12963  sqrt2irrap  12979  sqrtrirr  13008  phibndlem  13017  prm23ge5  13066  pclemdc  13090  pcxqcl  13114  pcge0  13115  pcdvdsb  13122  pceq0  13124  pcneg  13127  pcdvdstr  13129  pcgcd1  13130  pcgcd  13131  pc2dvds  13132  pcz  13134  pcprmpw2  13135  pcaddlem  13141  pcadd  13142  pcmpt  13145  pcmpt2  13146  pcprod  13148  fldivp1  13150  qexpz  13154  1arithlem4  13168  1arith  13169  4sqlem19  13211  ennnfonelemss  13353  ennnfonelemkh  13355  ennnfonelemhf1o  13356  ctiunctlemudc  13380  bassetsnn  13461  fvprif  13717  gzsumwsubmcl  13854  gzsumwmhm  13856  gzsumcl  13857  mulgnn0p1  13989  mulgnn0subcl  13991  mulgsubcl  13992  mulgneg  13996  mulgz  14006  mulgnn0dir  14008  mulgdirlem  14009  mulgdir  14010  submmulg  14022  ghmmulg  14112  gzsumreidx  14225  gzsumsubmcl  14226  gzsummhm  14229  gzsumsplit0  14232  gsumvalfi  14236  gzsumgsum  14239  lringuplu  14587  aprlring  14684  znf1o  15070  xblss2ps  15596  xblss2  15597  qtopbas  15714  dedekindeulemeu  15814  dedekindeu  15815  suplociccreex  15816  dedekindicclemeu  15823  dedekindicclemicc  15824  limcimolemlt  15856  cnplimclemle  15860  dvmptc  15909  reeff1o  15965  efltlemlt  15966  efap1p  15971  sin0pilem2  15975  coseq0negpitopi  16029  abssinper  16039  cos02pilt1  16045  logdivlt  16090  logbgcd1irraplemexp  16170  birthdaylem2  16192  birthdaylem3  16193  ppiqp1le  16233  ppiqltx  16247  ppiqub  16259  chtqub  16262  bcmono  16270  bcmax  16271  bposlem3  16279  bposlem5  16281  bposlem6  16282  bpos  16286  lgslem4  16293  lgsneg  16314  lgsneg1  16315  lgsmod  16316  lgsdilem  16317  lgsdir2  16323  lgsdirprm  16324  lgsdir  16325  lgsdi  16327  lgsne0  16328  lgsdirnn0  16337  lgsdinn0  16338  gausslemma2dlem1a  16348  gausslemma2dlem1f1o  16350  gausslemma2dlem4  16354  lgseisenlem1  16360  lgsquad3  16374  2sqlem4  16408  2sqlem9  16414  eupth2lem3lem3fi  16882  eupth2lem3lem4fi  16885  eupth2lem3lem7fi  16886  dichmul0orlem3  16926  dichmul0orlem7  16930  nnsf  17219  nninfsellemsuc  17226  nnnninfex  17236  trilpolemclim  17257  trilpolemisumle  17259  trilpolemeq1  17261  trilpolemlt1  17262  trirec0  17265  apdifflemf  17267  apdifflemr  17268  apdiff  17269  iswomni0  17273  nconstwlpolemgt0  17286  nconstwlpolem  17287  neapmkvlem  17289