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 )

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

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 721

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjao3dan  1348  dcun  3634  ifcldadc  3667  ifeq1dadc  3668  ifeq2dadc  3669  ifeqdadc  3670  ifbothdadc  3671  ifcldcd  3675  2if2dc  3677  ifeqeqxdc  3684  exmidn0m  4333  exmidsssn  4334  exmidundif  4338  exmidundifim  4339  ordtri2or2exmidlem  4668  reg2exmidlema  4676  nnpredcl  4765  frecabcl  6660  nnsucuniel  6758  dcdifsnid  6767  pw2f1odclem  7124  phpm  7157  fidifsnen  7162  dif1enen  7174  fin0  7179  fimax2gtrilemstep  7195  finexdc  7197  elssdc  7199  eqsndc  7200  en2eqpr  7204  fientri3  7212  unsnfidcex  7217  unsnfidcel  7218  undifdcss  7220  prfidceq  7225  tpfidceq  7227  fiintim  7228  ssfirab  7234  fidcenumlemrks  7260  fidcenumlemr  7262  2omap  7308  omp1eomlem  7424  difinfsnlem  7429  difinfsn  7430  ctssdccl  7441  ctssdc  7443  enumct  7445  nninfninc  7453  nnnninf  7456  nnnninfeq  7458  nnnninfeq2  7459  nninfisol  7463  finomni  7470  ismkvnex  7485  nninfwlpoimlemg  7505  pr2cv1  7531  exmidfodomrlemeldju  7541  exmidfodomrlemreseldju  7542  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  exmidaclem  7554  exmidontriimlem3  7569  netap  7610  2omotaplemap  7613  mullocprlem  7927  recexprlemloc  7988  suplocsrlem  8165  btwnapz  9755  xnn0dcle  10183  xnn0letri  10184  z2ge  10207  xaddcom  10242  xnegdi  10249  xaddass  10250  xpncan  10252  xleadd1a  10254  xsubge0  10262  xlesubadd  10264  fztri3or  10422  fzm1  10485  fzneuz  10486  exfzdc  10637  zsupcllemstep  10640  infssuzex  10644  exbtwnzlemstep  10660  rebtwn2zlemstep  10665  xqltnle  10680  apbtwnz  10687  modifeq2int  10801  modsumfzodifsn  10811  iseqf1olemab  10917  iseqf1olemmo  10920  seq3f1olemqsumk  10927  seq3f1olemqsum  10928  seq3f1olemstep  10929  seqf1oglem1  10934  seqf1oglem2  10935  fser0const  10950  expaddzaplem  10997  qsqeqor  11065  resq01  11073  expnbnd  11079  nn0ltexp2  11125  apexp1  11134  bcval  11165  bccmpl  11170  bcval5  11179  bcpasc  11182  bccl  11183  hashennnuni  11196  hashnncl  11212  fiubm  11249  hashfibc  11261  hashf1  11265  zfz1isolemiso  11269  lswex  11334  ccatsymb  11348  ccat1st1st  11387  fzowrddc  11397  swrd0g  11410  swrdsbslen  11416  swrdspsleq  11417  pfxclz  11429  pfxwrdsymbg  11440  swrdccatin1  11475  resqrexlemnm  11762  resqrexlemcvg  11763  resqrexlemoverl  11765  resqrexlemglsq  11766  leabs  11818  nn0abscl  11829  ltabs  11831  abslt  11832  fzomaxdif  11857  maxleim  11949  maxabslemval  11952  zmaxcl  11968  2zsupmax  11970  minmax  11974  2zinfmin  11987  xrmaxleim  11988  xrmaxifle  11990  xrmaxiflemab  11991  xrmaxiflemlub  11992  xrmaxiflemcom  11993  xrmaxiflemval  11994  xrmaxaddlem  12004  xrmaxadd  12005  xrminmax  12009  sumdc  12102  fzf1o  12120  sumrbdc  12124  summodclem3  12125  summodclem2a  12126  zsumdc  12129  isumss  12136  fisumss  12137  isumss2  12138  fsumcllem  12144  fsumadd  12151  fsumsplit  12152  fsumsplitsn  12155  sumsplitdc  12177  fisumrev2  12191  fsummulc2  12193  telfsumo  12211  fsumparts  12215  cvgratnnlemseq  12271  cvgratz  12277  fproddccvg  12317  prodrbdc  12319  zproddc  12324  prod1dc  12331  fprodssdc  12335  fprodmul  12336  fprodsplitdc  12341  fprodsplit  12342  fprodunsn  12349  fprodcllem  12351  sinltxirr  12506  fsumdvds  12587  dvdsle  12589  mod2eq1n2dvds  12624  bitsmod  12701  gcdsupex  12712  gcdsupcl  12713  gcdval  12714  gcddvds  12718  gcdcl  12721  gcd0id  12734  gcdneg  12737  bezoutlemmain  12753  bezoutlemzz  12757  bezoutlemaz  12758  bezoutlembz  12759  dfgcd3  12765  dfgcd2  12769  nninfctlemfo  12795  nn0seqcvgd  12797  eucalgf  12811  eucalginv  12812  dvdslcm  12825  lcmcl  12828  lcmneg  12830  lcmgcd  12834  lcmdvds  12835  lcmid  12836  mulgcddvds  12850  isprm5lem  12897  pw2dvdslemn  12921  sqrt2irrap  12936  phibndlem  12972  prm23ge5  13021  pclemdc  13045  pcxqcl  13069  pcge0  13070  pcdvdsb  13077  pceq0  13079  pcneg  13082  pcdvdstr  13084  pcgcd1  13085  pcgcd  13086  pc2dvds  13087  pcz  13089  pcprmpw2  13090  pcaddlem  13096  pcadd  13097  pcmpt  13100  pcmpt2  13101  pcprod  13103  fldivp1  13105  qexpz  13109  1arithlem4  13123  1arith  13124  4sqlem19  13166  ennnfonelemss  13279  ennnfonelemkh  13281  ennnfonelemhf1o  13282  ctiunctlemudc  13306  bassetsnn  13387  fvprif  13641  gzsumwsubmcl  13778  gzsumwmhm  13780  gzsumcl  13781  mulgnn0p1  13913  mulgnn0subcl  13915  mulgsubcl  13916  mulgneg  13920  mulgz  13930  mulgnn0dir  13932  mulgdirlem  13933  mulgdir  13934  submmulg  13946  ghmmulg  14036  gzsumreidx  14118  gzsumsubmcl  14119  gzsummhm  14122  gzsumsplit0  14125  gsumvalfi  14129  gzsumgsum  14132  lringuplu  14476  aprlring  14573  znf1o  14958  xblss2ps  15428  xblss2  15429  qtopbas  15546  dedekindeulemeu  15646  dedekindeu  15647  suplociccreex  15648  dedekindicclemeu  15655  dedekindicclemicc  15656  limcimolemlt  15688  cnplimclemle  15692  dvmptc  15741  reeff1o  15797  efltlemlt  15798  sin0pilem2  15806  coseq0negpitopi  15860  abssinper  15870  cos02pilt1  15875  logbgcd1irraplemexp  15993  lgslem4  16036  lgsneg  16057  lgsneg1  16058  lgsmod  16059  lgsdilem  16060  lgsdir2  16066  lgsdirprm  16067  lgsdir  16068  lgsdi  16070  lgsne0  16071  lgsdirnn0  16080  lgsdinn0  16081  gausslemma2dlem1a  16091  gausslemma2dlem1f1o  16093  gausslemma2dlem4  16097  lgseisenlem1  16103  lgsquad3  16117  2sqlem4  16151  2sqlem9  16157  eupth2lem3lem3fi  16625  eupth2lem3lem4fi  16628  eupth2lem3lem7fi  16629  dichmul0orlem3  16669  dichmul0orlem7  16673  nnsf  16953  nninfsellemsuc  16960  nnnninfex  16970  trilpolemclim  16990  trilpolemisumle  16992  trilpolemeq1  16994  trilpolemlt1  16995  trirec0  16998  apdifflemf  17000  apdifflemr  17001  apdiff  17002  iswomni0  17006  nconstwlpolemgt0  17019  nconstwlpolem  17020  neapmkvlem  17022