Theorem mpjaodan 788

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

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

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 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpjao3dan  1296  dcun  3514  ifcldadc  3544  ifeq1dadc  3545  ifbothdadc  3546  ifcldcd  3550  exmidn0m  4174  exmidsssn  4175  exmidundif  4179  exmidundifim  4180  ordtri2or2exmidlem  4497  reg2exmidlema  4505  nnpredcl  4594  frecabcl  6358  nnsucuniel  6454  dcdifsnid  6463  phpm  6822  fidifsnen  6827  dif1enen  6837  fin0  6842  fimax2gtrilemstep  6857  finexdc  6859  en2eqpr  6864  fientri3  6871  unsnfidcex  6876  unsnfidcel  6877  undifdcss  6879  fiintim  6885  ssfirab  6890  fidcenumlemrks  6909  fidcenumlemr  6911  omp1eomlem  7050  difinfsnlem  7055  difinfsn  7056  ctssdccl  7067  ctssdc  7069  enumct  7071  nnnninf  7081  nnnninfeq  7083  nnnninfeq2  7084  nninfisol  7088  finomni  7095  ismkvnex  7110  exmidfodomrlemeldju  7146  exmidfodomrlemreseldju  7147  exmidfodomrlemr  7149  exmidfodomrlemrALT  7150  exmidaclem  7155  exmidontriimlem3  7170  mullocprlem  7502  recexprlemloc  7563  suplocsrlem  7740  btwnapz  9312  xnn0dcle  9729  xnn0letri  9730  z2ge  9753  xaddcom  9788  xnegdi  9795  xaddass  9796  xpncan  9798  xleadd1a  9800  xsubge0  9808  xlesubadd  9810  fztri3or  9964  fzm1  10025  fzneuz  10026  exfzdc  10165  exbtwnzlemstep  10173  rebtwn2zlemstep  10178  apbtwnz  10199  modifeq2int  10311  modsumfzodifsn  10321  iseqf1olemab  10414  iseqf1olemmo  10417  seq3f1olemqsumk  10424  seq3f1olemqsum  10425  seq3f1olemstep  10426  fser0const  10441  expaddzaplem  10488  expnbnd  10567  nn0ltexp2  10612  apexp1  10620  bcval  10651  bccmpl  10656  bcval5  10665  bcpasc  10668  bccl  10669  hashennnuni  10681  hashnncl  10698  zfz1isolemiso  10738  resqrexlemnm  10946  resqrexlemcvg  10947  resqrexlemoverl  10949  resqrexlemglsq  10950  leabs  11002  nn0abscl  11013  ltabs  11015  abslt  11016  fzomaxdif  11041  maxleim  11133  maxabslemval  11136  zmaxcl  11152  2zsupmax  11153  minmax  11157  2zinfmin  11170  xrmaxleim  11171  xrmaxifle  11173  xrmaxiflemab  11174  xrmaxiflemlub  11175  xrmaxiflemcom  11176  xrmaxiflemval  11177  xrmaxaddlem  11187  xrmaxadd  11188  xrminmax  11192  sumdc  11285  sumrbdc  11306  summodclem3  11307  summodclem2a  11308  zsumdc  11311  isumss  11318  fisumss  11319  isumss2  11320  fsumcllem  11326  fsumadd  11333  fsumsplit  11334  fsumsplitsn  11337  sumsplitdc  11359  fisumrev2  11373  fsummulc2  11375  telfsumo  11393  fsumparts  11397  cvgratnnlemseq  11453  cvgratz  11459  fproddccvg  11499  prodrbdc  11501  zproddc  11506  prod1dc  11513  fprodssdc  11517  fprodmul  11518  fprodsplitdc  11523  fprodsplit  11524  fprodunsn  11531  fprodcllem  11533  dvdsle  11767  mod2eq1n2dvds  11801  zsupcllemstep  11863  infssuzex  11867  gcdsupex  11875  gcdsupcl  11876  gcdval  11877  gcddvds  11881  gcdcl  11884  gcd0id  11897  gcdneg  11900  bezoutlemmain  11916  bezoutlemzz  11920  bezoutlemaz  11921  bezoutlembz  11922  dfgcd3  11928  dfgcd2  11932  nn0seqcvgd  11952  eucalgf  11966  eucalginv  11967  dvdslcm  11980  lcmcl  11983  lcmneg  11985  lcmgcd  11989  lcmdvds  11990  lcmid  11991  mulgcddvds  12005  pw2dvdslemn  12074  sqrt2irrap  12089  phibndlem  12125  prm23ge5  12173  pclemdc  12197  pcge0  12221  pcdvdsb  12228  pceq0  12230  pcneg  12233  pcdvdstr  12235  pcgcd1  12236  pcgcd  12237  pc2dvds  12238  pcz  12240  pcprmpw2  12241  pcaddlem  12247  pcadd  12248  pcmpt  12250  pcmpt2  12251  pcprod  12253  fldivp1  12255  qexpz  12259  ennnfonelemss  12280  ennnfonelemkh  12282  ennnfonelemhf1o  12283  ctiunctlemudc  12307  xblss2ps  12945  xblss2  12946  qtopbas  13063  dedekindeulemeu  13141  dedekindeu  13142  suplociccreex  13143  dedekindicclemeu  13150  dedekindicclemicc  13151  limcimolemlt  13174  cnplimclemle  13178  reeff1o  13235  efltlemlt  13236  sin0pilem2  13244  coseq0negpitopi  13298  abssinper  13308  cos02pilt1  13313  logbgcd1irraplemexp  13427  nnsf  13719  nninfsellemsuc  13726  trilpolemclim  13749  trilpolemisumle  13751  trilpolemeq1  13753  trilpolemlt1  13754  trirec0  13757  apdifflemf  13759  apdifflemr  13760  apdiff  13761  iswomni0  13764  nconstwlpolemgt0  13776  nconstwlpolem  13777  neapmkvlem  13779