Theorem mpjaodan 787

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 786	. 2 |- ( ( ph /\ ( ps \/ th ) ) -> ch )
5	1, 4	mpdan 417	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ wa 103   \/ wo 697

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpjao3dan  1285  dcun  3473  ifcldadc  3501  ifeq1dadc  3502  ifbothdadc  3503  ifcldcd  3507  exmidn0m  4124  exmidsssn  4125  exmidundif  4129  exmidundifim  4130  ordtri2or2exmidlem  4441  reg2exmidlema  4449  nnpredcl  4536  frecabcl  6296  nnsucuniel  6391  dcdifsnid  6400  phpm  6759  fidifsnen  6764  dif1enen  6774  fin0  6779  fimax2gtrilemstep  6794  finexdc  6796  en2eqpr  6801  fientri3  6803  unsnfidcex  6808  unsnfidcel  6809  undifdcss  6811  fiintim  6817  ssfirab  6822  fidcenumlemrks  6841  fidcenumlemr  6843  omp1eomlem  6979  difinfsnlem  6984  difinfsn  6985  ctssdccl  6996  ctssdc  6998  enumct  7000  finomni  7012  nnnninf  7023  ismkvnex  7029  exmidfodomrlemeldju  7055  exmidfodomrlemreseldju  7056  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  exmidaclem  7064  mullocprlem  7378  recexprlemloc  7439  suplocsrlem  7616  btwnapz  9181  z2ge  9609  xaddcom  9644  xnegdi  9651  xaddass  9652  xpncan  9654  xleadd1a  9656  xsubge0  9664  xlesubadd  9666  fztri3or  9819  fzm1  9880  fzneuz  9881  exfzdc  10017  exbtwnzlemstep  10025  rebtwn2zlemstep  10030  apbtwnz  10047  modifeq2int  10159  modsumfzodifsn  10169  iseqf1olemab  10262  iseqf1olemmo  10265  seq3f1olemqsumk  10272  seq3f1olemqsum  10273  seq3f1olemstep  10274  fser0const  10289  expaddzaplem  10336  expnbnd  10415  bcval  10495  bccmpl  10500  bcval5  10509  bcpasc  10512  bccl  10513  hashennnuni  10525  hashnncl  10542  zfz1isolemiso  10582  resqrexlemnm  10790  resqrexlemcvg  10791  resqrexlemoverl  10793  resqrexlemglsq  10794  leabs  10846  nn0abscl  10857  ltabs  10859  abslt  10860  fzomaxdif  10885  maxleim  10977  maxabslemval  10980  zmaxcl  10996  2zsupmax  10997  minmax  11001  xrmaxleim  11013  xrmaxifle  11015  xrmaxiflemab  11016  xrmaxiflemlub  11017  xrmaxiflemcom  11018  xrmaxiflemval  11019  xrmaxaddlem  11029  xrmaxadd  11030  xrminmax  11034  sumdc  11127  sumrbdc  11148  summodclem3  11149  summodclem2a  11150  zsumdc  11153  isumss  11160  fisumss  11161  isumss2  11162  fsumcllem  11168  fsumadd  11175  fsumsplit  11176  fsumsplitsn  11179  sumsplitdc  11201  fisumrev2  11215  fsummulc2  11217  telfsumo  11235  fsumparts  11239  cvgratnnlemseq  11295  cvgratz  11301  fproddccvg  11341  prodrbdc  11343  dvdsle  11542  mod2eq1n2dvds  11576  zsupcllemstep  11638  infssuzex  11642  gcdsupex  11646  gcdsupcl  11647  gcdval  11648  gcddvds  11652  gcdcl  11655  gcd0id  11667  gcdneg  11670  bezoutlemmain  11686  bezoutlemzz  11690  bezoutlemaz  11691  bezoutlembz  11692  dfgcd3  11698  dfgcd2  11702  nn0seqcvgd  11722  eucalgf  11736  eucalginv  11737  dvdslcm  11750  lcmcl  11753  lcmneg  11755  lcmgcd  11759  lcmdvds  11760  lcmid  11761  mulgcddvds  11775  pw2dvdslemn  11843  sqrt2irrap  11858  phibndlem  11892  ennnfonelemss  11923  ennnfonelemkh  11925  ennnfonelemhf1o  11926  ctiunctlemudc  11950  xblss2ps  12573  xblss2  12574  qtopbas  12691  dedekindeulemeu  12769  dedekindeu  12770  suplociccreex  12771  dedekindicclemeu  12778  dedekindicclemicc  12779  limcimolemlt  12802  cnplimclemle  12806  sin0pilem2  12863  coseq0negpitopi  12917  abssinper  12927  cos02pilt1  12932  nnsf  13199  nninfalllemn  13202  nninfsellemsuc  13208  trilpolemclim  13229  trilpolemisumle  13231  trilpolemeq1  13233  trilpolemlt1  13234