Theorem mpjaodan 793

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

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

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 704

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpjao3dan  1302  dcun  3524  ifcldadc  3554  ifeq1dadc  3555  ifbothdadc  3556  ifcldcd  3560  exmidn0m  4185  exmidsssn  4186  exmidundif  4190  exmidundifim  4191  ordtri2or2exmidlem  4508  reg2exmidlema  4516  nnpredcl  4605  frecabcl  6375  nnsucuniel  6471  dcdifsnid  6480  phpm  6839  fidifsnen  6844  dif1enen  6854  fin0  6859  fimax2gtrilemstep  6874  finexdc  6876  en2eqpr  6881  fientri3  6888  unsnfidcex  6893  unsnfidcel  6894  undifdcss  6896  fiintim  6902  ssfirab  6907  fidcenumlemrks  6926  fidcenumlemr  6928  omp1eomlem  7067  difinfsnlem  7072  difinfsn  7073  ctssdccl  7084  ctssdc  7086  enumct  7088  nnnninf  7098  nnnninfeq  7100  nnnninfeq2  7101  nninfisol  7105  finomni  7112  ismkvnex  7127  exmidfodomrlemeldju  7163  exmidfodomrlemreseldju  7164  exmidfodomrlemr  7166  exmidfodomrlemrALT  7167  exmidaclem  7172  exmidontriimlem3  7187  mullocprlem  7519  recexprlemloc  7580  suplocsrlem  7757  btwnapz  9329  xnn0dcle  9746  xnn0letri  9747  z2ge  9770  xaddcom  9805  xnegdi  9812  xaddass  9813  xpncan  9815  xleadd1a  9817  xsubge0  9825  xlesubadd  9827  fztri3or  9982  fzm1  10043  fzneuz  10044  exfzdc  10183  exbtwnzlemstep  10191  rebtwn2zlemstep  10196  apbtwnz  10217  modifeq2int  10329  modsumfzodifsn  10339  iseqf1olemab  10432  iseqf1olemmo  10435  seq3f1olemqsumk  10442  seq3f1olemqsum  10443  seq3f1olemstep  10444  fser0const  10459  expaddzaplem  10506  qsqeqor  10573  expnbnd  10586  nn0ltexp2  10631  apexp1  10639  bcval  10670  bccmpl  10675  bcval5  10684  bcpasc  10687  bccl  10688  hashennnuni  10700  hashnncl  10717  fiubm  10750  zfz1isolemiso  10761  resqrexlemnm  10969  resqrexlemcvg  10970  resqrexlemoverl  10972  resqrexlemglsq  10973  leabs  11025  nn0abscl  11036  ltabs  11038  abslt  11039  fzomaxdif  11064  maxleim  11156  maxabslemval  11159  zmaxcl  11175  2zsupmax  11176  minmax  11180  2zinfmin  11193  xrmaxleim  11194  xrmaxifle  11196  xrmaxiflemab  11197  xrmaxiflemlub  11198  xrmaxiflemcom  11199  xrmaxiflemval  11200  xrmaxaddlem  11210  xrmaxadd  11211  xrminmax  11215  sumdc  11308  sumrbdc  11329  summodclem3  11330  summodclem2a  11331  zsumdc  11334  isumss  11341  fisumss  11342  isumss2  11343  fsumcllem  11349  fsumadd  11356  fsumsplit  11357  fsumsplitsn  11360  sumsplitdc  11382  fisumrev2  11396  fsummulc2  11398  telfsumo  11416  fsumparts  11420  cvgratnnlemseq  11476  cvgratz  11482  fproddccvg  11522  prodrbdc  11524  zproddc  11529  prod1dc  11536  fprodssdc  11540  fprodmul  11541  fprodsplitdc  11546  fprodsplit  11547  fprodunsn  11554  fprodcllem  11556  dvdsle  11791  mod2eq1n2dvds  11825  zsupcllemstep  11887  infssuzex  11891  gcdsupex  11899  gcdsupcl  11900  gcdval  11901  gcddvds  11905  gcdcl  11908  gcd0id  11921  gcdneg  11924  bezoutlemmain  11940  bezoutlemzz  11944  bezoutlemaz  11945  bezoutlembz  11946  dfgcd3  11952  dfgcd2  11956  nn0seqcvgd  11982  eucalgf  11996  eucalginv  11997  dvdslcm  12010  lcmcl  12013  lcmneg  12015  lcmgcd  12019  lcmdvds  12020  lcmid  12021  mulgcddvds  12035  isprm5lem  12082  pw2dvdslemn  12106  sqrt2irrap  12121  phibndlem  12157  prm23ge5  12205  pclemdc  12229  pcge0  12253  pcdvdsb  12260  pceq0  12262  pcneg  12265  pcdvdstr  12267  pcgcd1  12268  pcgcd  12269  pc2dvds  12270  pcz  12272  pcprmpw2  12273  pcaddlem  12279  pcadd  12280  pcmpt  12282  pcmpt2  12283  pcprod  12285  fldivp1  12287  qexpz  12291  1arithlem4  12305  1arith  12306  ennnfonelemss  12352  ennnfonelemkh  12354  ennnfonelemhf1o  12355  ctiunctlemudc  12379  xblss2ps  13157  xblss2  13158  qtopbas  13275  dedekindeulemeu  13353  dedekindeu  13354  suplociccreex  13355  dedekindicclemeu  13362  dedekindicclemicc  13363  limcimolemlt  13386  cnplimclemle  13390  reeff1o  13447  efltlemlt  13448  sin0pilem2  13456  coseq0negpitopi  13510  abssinper  13520  cos02pilt1  13525  logbgcd1irraplemexp  13639  lgslem4  13657  lgsneg  13678  lgsneg1  13679  lgsmod  13680  lgsdilem  13681  lgsdir2  13687  lgsdirprm  13688  lgsdir  13689  lgsdi  13691  lgsne0  13692  lgsdirnn0  13701  lgsdinn0  13702  2sqlem4  13707  2sqlem9  13713  nnsf  13998  nninfsellemsuc  14005  trilpolemclim  14028  trilpolemisumle  14030  trilpolemeq1  14032  trilpolemlt1  14033  trirec0  14036  apdifflemf  14038  apdifflemr  14039  apdiff  14040  iswomni0  14043  nconstwlpolemgt0  14055  nconstwlpolem  14056  neapmkvlem  14058