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	|- ( ( ph /\ ps ) -> ch )
jaodan.2	|- ( ( ph /\ th ) -> ch )
jaodan.3	|- ( ph -> ( ps \/ th ) )

Assertion

Ref	Expression
mpjaodan	|- ( ph -> ch )

Proof of Theorem mpjaodan

Step	Hyp	Ref	Expression
1		jaodan.3	. 2 |- ( ph -> ( ps \/ th ) )
2		jaodan.1	. . 3 |- ( ( ph /\ ps ) -> ch )
3		jaodan.2	. . 3 |- ( ( ph /\ th ) -> ch )
4	2, 3	jaodan 809	. 2 |- ( ( ph /\ ( ps \/ th ) ) -> ch )
5	1, 4	mpdan 425	1 |- ( ph -> ch )

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  16044  logdivlt  16088  logbgcd1irraplemexp  16165  birthdaylem2  16187  birthdaylem3  16188  ppiqp1le  16228  ppiqltx  16242  ppiqub  16254  chtqub  16257  bcmono  16265  bcmax  16266  bposlem3  16274  bposlem5  16276  bposlem6  16277  bpos  16281  lgslem4  16288  lgsneg  16309  lgsneg1  16310  lgsmod  16311  lgsdilem  16312  lgsdir2  16318  lgsdirprm  16319  lgsdir  16320  lgsdi  16322  lgsne0  16323  lgsdirnn0  16332  lgsdinn0  16333  gausslemma2dlem1a  16343  gausslemma2dlem1f1o  16345  gausslemma2dlem4  16349  lgseisenlem1  16355  lgsquad3  16369  2sqlem4  16403  2sqlem9  16409  eupth2lem3lem3fi  16877  eupth2lem3lem4fi  16880  eupth2lem3lem7fi  16881  dichmul0orlem3  16921  dichmul0orlem7  16925  nnsf  17214  nninfsellemsuc  17221  nnnninfex  17231  trilpolemclim  17252  trilpolemisumle  17254  trilpolemeq1  17256  trilpolemlt1  17257  trirec0  17260  apdifflemf  17262  apdifflemr  17263  apdiff  17264  iswomni0  17268  nconstwlpolemgt0  17281  nconstwlpolem  17282  neapmkvlem  17284