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  3621  ifcldadc  3654  ifeq1dadc  3655  ifeq2dadc  3656  ifeqdadc  3657  ifbothdadc  3658  ifcldcd  3662  2if2dc  3664  exmidn0m  4316  exmidsssn  4317  exmidundif  4321  exmidundifim  4322  ordtri2or2exmidlem  4650  reg2exmidlema  4658  nnpredcl  4747  frecabcl  6632  nnsucuniel  6730  dcdifsnid  6739  pw2f1odclem  7089  phpm  7122  fidifsnen  7127  dif1enen  7139  fin0  7144  fimax2gtrilemstep  7160  finexdc  7162  elssdc  7164  eqsndc  7165  en2eqpr  7169  fientri3  7177  unsnfidcex  7182  unsnfidcel  7183  undifdcss  7185  prfidceq  7190  tpfidceq  7192  fiintim  7193  ssfirab  7199  fidcenumlemrks  7225  fidcenumlemr  7227  2omap  7271  omp1eomlem  7387  difinfsnlem  7392  difinfsn  7393  ctssdccl  7404  ctssdc  7406  enumct  7408  nninfninc  7416  nnnninf  7419  nnnninfeq  7421  nnnninfeq2  7422  nninfisol  7426  finomni  7433  ismkvnex  7448  nninfwlpoimlemg  7468  pr2cv1  7494  exmidfodomrlemeldju  7504  exmidfodomrlemreseldju  7505  exmidfodomrlemr  7507  exmidfodomrlemrALT  7508  exmidaclem  7517  exmidontriimlem3  7532  netap  7570  2omotaplemap  7573  mullocprlem  7887  recexprlemloc  7948  suplocsrlem  8125  btwnapz  9711  xnn0dcle  10138  xnn0letri  10139  z2ge  10162  xaddcom  10197  xnegdi  10204  xaddass  10205  xpncan  10207  xleadd1a  10209  xsubge0  10217  xlesubadd  10219  fztri3or  10376  fzm1  10438  fzneuz  10439  exfzdc  10590  zsupcllemstep  10593  infssuzex  10597  exbtwnzlemstep  10611  rebtwn2zlemstep  10616  xqltnle  10631  apbtwnz  10638  modifeq2int  10752  modsumfzodifsn  10762  iseqf1olemab  10868  iseqf1olemmo  10871  seq3f1olemqsumk  10878  seq3f1olemqsum  10879  seq3f1olemstep  10880  seqf1oglem1  10885  seqf1oglem2  10886  fser0const  10901  expaddzaplem  10948  qsqeqor  11016  expnbnd  11029  nn0ltexp2  11075  apexp1  11084  bcval  11115  bccmpl  11120  bcval5  11129  bcpasc  11132  bccl  11133  hashennnuni  11146  hashnncl  11162  fiubm  11199  hashfibc  11211  zfz1isolemiso  11215  lswex  11280  ccatsymb  11294  ccat1st1st  11333  fzowrddc  11343  swrd0g  11356  swrdsbslen  11362  swrdspsleq  11363  pfxclz  11375  pfxwrdsymbg  11386  swrdccatin1  11421  resqrexlemnm  11707  resqrexlemcvg  11708  resqrexlemoverl  11710  resqrexlemglsq  11711  leabs  11763  nn0abscl  11774  ltabs  11776  abslt  11777  fzomaxdif  11802  maxleim  11894  maxabslemval  11897  zmaxcl  11913  2zsupmax  11915  minmax  11919  2zinfmin  11932  xrmaxleim  11933  xrmaxifle  11935  xrmaxiflemab  11936  xrmaxiflemlub  11937  xrmaxiflemcom  11938  xrmaxiflemval  11939  xrmaxaddlem  11949  xrmaxadd  11950  xrminmax  11954  sumdc  12047  fzf1o  12065  sumrbdc  12069  summodclem3  12070  summodclem2a  12071  zsumdc  12074  isumss  12081  fisumss  12082  isumss2  12083  fsumcllem  12089  fsumadd  12096  fsumsplit  12097  fsumsplitsn  12100  sumsplitdc  12122  fisumrev2  12136  fsummulc2  12138  telfsumo  12156  fsumparts  12160  cvgratnnlemseq  12216  cvgratz  12222  fproddccvg  12262  prodrbdc  12264  zproddc  12269  prod1dc  12276  fprodssdc  12280  fprodmul  12281  fprodsplitdc  12286  fprodsplit  12287  fprodunsn  12294  fprodcllem  12296  sinltxirr  12451  fsumdvds  12532  dvdsle  12534  mod2eq1n2dvds  12569  bitsmod  12646  gcdsupex  12657  gcdsupcl  12658  gcdval  12659  gcddvds  12663  gcdcl  12666  gcd0id  12679  gcdneg  12682  bezoutlemmain  12698  bezoutlemzz  12702  bezoutlemaz  12703  bezoutlembz  12704  dfgcd3  12710  dfgcd2  12714  nninfctlemfo  12740  nn0seqcvgd  12742  eucalgf  12756  eucalginv  12757  dvdslcm  12770  lcmcl  12773  lcmneg  12775  lcmgcd  12779  lcmdvds  12780  lcmid  12781  mulgcddvds  12795  isprm5lem  12842  pw2dvdslemn  12866  sqrt2irrap  12881  phibndlem  12917  prm23ge5  12966  pclemdc  12990  pcxqcl  13014  pcge0  13015  pcdvdsb  13022  pceq0  13024  pcneg  13027  pcdvdstr  13029  pcgcd1  13030  pcgcd  13031  pc2dvds  13032  pcz  13034  pcprmpw2  13035  pcaddlem  13041  pcadd  13042  pcmpt  13045  pcmpt2  13046  pcprod  13048  fldivp1  13050  qexpz  13054  1arithlem4  13068  1arith  13069  4sqlem19  13111  ennnfonelemss  13178  ennnfonelemkh  13180  ennnfonelemhf1o  13181  ctiunctlemudc  13205  bassetsnn  13286  fvprif  13573  gsumfzz  13725  gsumwsubmcl  13726  gsumwmhm  13728  gsumfzcl  13729  mulgnn0p1  13867  mulgnn0subcl  13869  mulgsubcl  13870  mulgneg  13874  mulgz  13884  mulgnn0dir  13886  mulgdirlem  13887  mulgdir  13888  submmulg  13900  ghmmulg  13990  gsumfzreidx  14071  gsumfzsubmcl  14072  gsumfzmptfidmadd  14073  gsumfzmhm  14077  gsumsplit0  14080  lringuplu  14358  aprlring  14451  gsumfzfsum  14753  znf1o  14816  xblss2ps  15286  xblss2  15287  qtopbas  15404  dedekindeulemeu  15504  dedekindeu  15505  suplociccreex  15506  dedekindicclemeu  15513  dedekindicclemicc  15514  limcimolemlt  15546  cnplimclemle  15550  dvmptc  15599  reeff1o  15655  efltlemlt  15656  sin0pilem2  15664  coseq0negpitopi  15718  abssinper  15728  cos02pilt1  15733  logbgcd1irraplemexp  15850  lgslem4  15893  lgsneg  15914  lgsneg1  15915  lgsmod  15916  lgsdilem  15917  lgsdir2  15923  lgsdirprm  15924  lgsdir  15925  lgsdi  15927  lgsne0  15928  lgsdirnn0  15937  lgsdinn0  15938  gausslemma2dlem1a  15948  gausslemma2dlem1f1o  15950  gausslemma2dlem4  15954  lgseisenlem1  15960  lgsquad3  15974  2sqlem4  16008  2sqlem9  16014  eupth2lem3lem3fi  16482  eupth2lem3lem4fi  16485  eupth2lem3lem7fi  16486  nnsf  16800  nninfsellemsuc  16807  nnnninfex  16817  trilpolemclim  16837  trilpolemisumle  16839  trilpolemeq1  16841  trilpolemlt1  16842  trirec0  16845  apdifflemf  16847  apdifflemr  16848  apdiff  16849  iswomni0  16853  trimul0or  16862  nconstwlpolemgt0  16867  nconstwlpolem  16868  neapmkvlem  16870  gfsumval  16879  gsumgfsum  16883