Theorem mpjaodan 806

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

Syntax hints:   -> wi 4   /\ wa 104   \/ wo 716

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjao3dan  1344  dcun  3606  ifcldadc  3639  ifeq1dadc  3640  ifeq2dadc  3641  ifeqdadc  3642  ifbothdadc  3643  ifcldcd  3647  2if2dc  3649  exmidn0m  4297  exmidsssn  4298  exmidundif  4302  exmidundifim  4303  ordtri2or2exmidlem  4630  reg2exmidlema  4638  nnpredcl  4727  frecabcl  6608  nnsucuniel  6706  dcdifsnid  6715  pw2f1odclem  7063  phpm  7095  fidifsnen  7100  dif1enen  7112  fin0  7117  fimax2gtrilemstep  7133  finexdc  7135  elssdc  7137  eqsndc  7138  en2eqpr  7142  fientri3  7150  unsnfidcex  7155  unsnfidcel  7156  undifdcss  7158  prfidceq  7163  tpfidceq  7165  fiintim  7166  ssfirab  7172  fidcenumlemrks  7195  fidcenumlemr  7197  omp1eomlem  7353  difinfsnlem  7358  difinfsn  7359  ctssdccl  7370  ctssdc  7372  enumct  7374  nninfninc  7382  nnnninf  7385  nnnninfeq  7387  nnnninfeq2  7388  nninfisol  7392  finomni  7399  ismkvnex  7414  nninfwlpoimlemg  7434  pr2cv1  7460  exmidfodomrlemeldju  7470  exmidfodomrlemreseldju  7471  exmidfodomrlemr  7473  exmidfodomrlemrALT  7474  exmidaclem  7483  exmidontriimlem3  7498  netap  7533  2omotaplemap  7536  mullocprlem  7850  recexprlemloc  7911  suplocsrlem  8088  btwnapz  9671  xnn0dcle  10098  xnn0letri  10099  z2ge  10122  xaddcom  10157  xnegdi  10164  xaddass  10165  xpncan  10167  xleadd1a  10169  xsubge0  10177  xlesubadd  10179  fztri3or  10336  fzm1  10397  fzneuz  10398  exfzdc  10549  zsupcllemstep  10552  infssuzex  10556  exbtwnzlemstep  10570  rebtwn2zlemstep  10575  xqltnle  10590  apbtwnz  10597  modifeq2int  10711  modsumfzodifsn  10721  iseqf1olemab  10827  iseqf1olemmo  10830  seq3f1olemqsumk  10837  seq3f1olemqsum  10838  seq3f1olemstep  10839  seqf1oglem1  10844  seqf1oglem2  10845  fser0const  10860  expaddzaplem  10907  qsqeqor  10975  expnbnd  10988  nn0ltexp2  11034  apexp1  11043  bcval  11074  bccmpl  11079  bcval5  11088  bcpasc  11091  bccl  11092  hashennnuni  11104  hashnncl  11120  fiubm  11155  zfz1isolemiso  11166  lswex  11231  ccatsymb  11245  ccat1st1st  11284  fzowrddc  11294  swrd0g  11307  swrdsbslen  11313  swrdspsleq  11314  pfxclz  11326  pfxwrdsymbg  11337  swrdccatin1  11372  resqrexlemnm  11658  resqrexlemcvg  11659  resqrexlemoverl  11661  resqrexlemglsq  11662  leabs  11714  nn0abscl  11725  ltabs  11727  abslt  11728  fzomaxdif  11753  maxleim  11845  maxabslemval  11848  zmaxcl  11864  2zsupmax  11866  minmax  11870  2zinfmin  11883  xrmaxleim  11884  xrmaxifle  11886  xrmaxiflemab  11887  xrmaxiflemlub  11888  xrmaxiflemcom  11889  xrmaxiflemval  11890  xrmaxaddlem  11900  xrmaxadd  11901  xrminmax  11905  sumdc  11998  fzf1o  12016  sumrbdc  12020  summodclem3  12021  summodclem2a  12022  zsumdc  12025  isumss  12032  fisumss  12033  isumss2  12034  fsumcllem  12040  fsumadd  12047  fsumsplit  12048  fsumsplitsn  12051  sumsplitdc  12073  fisumrev2  12087  fsummulc2  12089  telfsumo  12107  fsumparts  12111  cvgratnnlemseq  12167  cvgratz  12173  fproddccvg  12213  prodrbdc  12215  zproddc  12220  prod1dc  12227  fprodssdc  12231  fprodmul  12232  fprodsplitdc  12237  fprodsplit  12238  fprodunsn  12245  fprodcllem  12247  sinltxirr  12402  fsumdvds  12483  dvdsle  12485  mod2eq1n2dvds  12520  bitsmod  12597  gcdsupex  12608  gcdsupcl  12609  gcdval  12610  gcddvds  12614  gcdcl  12617  gcd0id  12630  gcdneg  12633  bezoutlemmain  12649  bezoutlemzz  12653  bezoutlemaz  12654  bezoutlembz  12655  dfgcd3  12661  dfgcd2  12665  nninfctlemfo  12691  nn0seqcvgd  12693  eucalgf  12707  eucalginv  12708  dvdslcm  12721  lcmcl  12724  lcmneg  12726  lcmgcd  12730  lcmdvds  12731  lcmid  12732  mulgcddvds  12746  isprm5lem  12793  pw2dvdslemn  12817  sqrt2irrap  12832  phibndlem  12868  prm23ge5  12917  pclemdc  12941  pcxqcl  12965  pcge0  12966  pcdvdsb  12973  pceq0  12975  pcneg  12978  pcdvdstr  12980  pcgcd1  12981  pcgcd  12982  pc2dvds  12983  pcz  12985  pcprmpw2  12986  pcaddlem  12992  pcadd  12993  pcmpt  12996  pcmpt2  12997  pcprod  12999  fldivp1  13001  qexpz  13005  1arithlem4  13019  1arith  13020  4sqlem19  13062  ennnfonelemss  13111  ennnfonelemkh  13113  ennnfonelemhf1o  13114  ctiunctlemudc  13138  bassetsnn  13219  fvprif  13506  gsumfzz  13658  gsumwsubmcl  13659  gsumwmhm  13661  gsumfzcl  13662  mulgnn0p1  13800  mulgnn0subcl  13802  mulgsubcl  13803  mulgneg  13807  mulgz  13817  mulgnn0dir  13819  mulgdirlem  13820  mulgdir  13821  submmulg  13833  ghmmulg  13923  gsumfzreidx  14004  gsumfzsubmcl  14005  gsumfzmptfidmadd  14006  gsumfzmhm  14010  gsumsplit0  14013  lringuplu  14291  gsumfzfsum  14684  znf1o  14747  xblss2ps  15215  xblss2  15216  qtopbas  15333  dedekindeulemeu  15433  dedekindeu  15434  suplociccreex  15435  dedekindicclemeu  15442  dedekindicclemicc  15443  limcimolemlt  15475  cnplimclemle  15479  dvmptc  15528  reeff1o  15584  efltlemlt  15585  sin0pilem2  15593  coseq0negpitopi  15647  abssinper  15657  cos02pilt1  15662  logbgcd1irraplemexp  15779  lgslem4  15822  lgsneg  15843  lgsneg1  15844  lgsmod  15845  lgsdilem  15846  lgsdir2  15852  lgsdirprm  15853  lgsdir  15854  lgsdi  15856  lgsne0  15857  lgsdirnn0  15866  lgsdinn0  15867  gausslemma2dlem1a  15877  gausslemma2dlem1f1o  15879  gausslemma2dlem4  15883  lgseisenlem1  15889  lgsquad3  15903  2sqlem4  15937  2sqlem9  15943  eupth2lem3lem3fi  16411  eupth2lem3lem4fi  16414  eupth2lem3lem7fi  16415  2omap  16715  nnsf  16731  nninfsellemsuc  16738  nnnninfex  16748  trilpolemclim  16768  trilpolemisumle  16770  trilpolemeq1  16772  trilpolemlt1  16773  trirec0  16776  apdifflemf  16778  apdifflemr  16779  apdiff  16780  iswomni0  16784  nconstwlpolemgt0  16797  nconstwlpolem  16798  neapmkvlem  16800  gfsumval  16809  gsumgfsum  16813