Theorem mpjaodan 770

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

Syntax hints:   → wi 4   ∧ wa 103   ∨ wo 680

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpjao3dan  1268  dcun  3439  ifcldadc  3467  ifeq1dadc  3468  ifbothdadc  3469  ifcldcd  3473  exmidn0m  4084  exmidsssn  4085  exmidundif  4089  exmidundifim  4090  ordtri2or2exmidlem  4401  reg2exmidlema  4409  nnpredcl  4496  frecabcl  6250  nnsucuniel  6345  dcdifsnid  6354  phpm  6712  fidifsnen  6717  dif1enen  6727  fin0  6732  fimax2gtrilemstep  6747  finexdc  6749  en2eqpr  6754  fientri3  6756  unsnfidcex  6761  unsnfidcel  6762  undifdcss  6764  fiintim  6770  ssfirab  6774  fidcenumlemrks  6793  fidcenumlemr  6795  omp1eomlem  6931  difinfsnlem  6936  difinfsn  6937  ctssdccl  6948  ctssdc  6950  enumct  6952  finomni  6962  nnnninf  6973  ismkvnex  6979  exmidfodomrlemeldju  7003  exmidfodomrlemreseldju  7004  exmidfodomrlemr  7006  exmidfodomrlemrALT  7007  exmidaclem  7012  mullocprlem  7323  recexprlemloc  7384  btwnapz  9082  z2ge  9499  xaddcom  9534  xnegdi  9541  xaddass  9542  xpncan  9544  xleadd1a  9546  xsubge0  9554  xlesubadd  9556  fztri3or  9709  fzm1  9770  fzneuz  9771  exfzdc  9907  exbtwnzlemstep  9915  rebtwn2zlemstep  9920  apbtwnz  9937  modifeq2int  10049  modsumfzodifsn  10059  iseqf1olemab  10152  iseqf1olemmo  10155  seq3f1olemqsumk  10162  seq3f1olemqsum  10163  seq3f1olemstep  10164  fser0const  10179  expaddzaplem  10226  expnbnd  10305  bcval  10385  bccmpl  10390  bcval5  10399  bcpasc  10402  bccl  10403  hashennnuni  10415  hashnncl  10432  zfz1isolemiso  10472  resqrexlemnm  10679  resqrexlemcvg  10680  resqrexlemoverl  10682  resqrexlemglsq  10683  leabs  10735  nn0abscl  10746  ltabs  10748  abslt  10749  fzomaxdif  10774  maxleim  10866  maxabslemval  10869  zmaxcl  10885  2zsupmax  10886  minmax  10890  xrmaxleim  10902  xrmaxifle  10904  xrmaxiflemab  10905  xrmaxiflemlub  10906  xrmaxiflemcom  10907  xrmaxiflemval  10908  xrmaxaddlem  10918  xrmaxadd  10919  xrminmax  10923  sumdc  11016  sumrbdc  11036  summodclem3  11038  summodclem2a  11039  zsumdc  11042  isumss  11049  fisumss  11050  isumss2  11051  fsumcllem  11057  fsumadd  11064  fsumsplit  11065  fsumsplitsn  11068  sumsplitdc  11090  fisumrev2  11104  fsummulc2  11106  telfsumo  11124  fsumparts  11128  cvgratnnlemseq  11184  cvgratz  11190  dvdsle  11387  mod2eq1n2dvds  11421  zsupcllemstep  11483  infssuzex  11487  gcdsupex  11491  gcdsupcl  11492  gcdval  11493  gcddvds  11497  gcdcl  11500  gcd0id  11512  gcdneg  11515  bezoutlemmain  11529  bezoutlemzz  11533  bezoutlemaz  11534  bezoutlembz  11535  dfgcd3  11541  dfgcd2  11545  nn0seqcvgd  11565  eucalgf  11579  eucalginv  11580  dvdslcm  11593  lcmcl  11596  lcmneg  11598  lcmgcd  11602  lcmdvds  11603  lcmid  11604  mulgcddvds  11618  pw2dvdslemn  11685  sqrt2irrap  11700  phibndlem  11734  ennnfonelemss  11765  ennnfonelemkh  11767  ennnfonelemhf1o  11768  ctiunctlemudc  11790  xblss2ps  12390  xblss2  12391  qtopbas  12508  limcimolemlt  12586  cnplimclemle  12590  nnsf  12883  nninfalllemn  12886  nninfsellemsuc  12892  trilpolemclim  12913  trilpolemisumle  12915  trilpolemeq1  12917  trilpolemlt1  12918