Theorem mpjaodan 798

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

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

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 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  mpjao3dan  1307  dcun  3533  ifcldadc  3563  ifeq1dadc  3564  ifeq2dadc  3565  ifbothdadc  3566  ifcldcd  3570  exmidn0m  4201  exmidsssn  4202  exmidundif  4206  exmidundifim  4207  ordtri2or2exmidlem  4525  reg2exmidlema  4533  nnpredcl  4622  frecabcl  6399  nnsucuniel  6495  dcdifsnid  6504  phpm  6864  fidifsnen  6869  dif1enen  6879  fin0  6884  fimax2gtrilemstep  6899  finexdc  6901  en2eqpr  6906  fientri3  6913  unsnfidcex  6918  unsnfidcel  6919  undifdcss  6921  fiintim  6927  ssfirab  6932  fidcenumlemrks  6951  fidcenumlemr  6953  omp1eomlem  7092  difinfsnlem  7097  difinfsn  7098  ctssdccl  7109  ctssdc  7111  enumct  7113  nnnninf  7123  nnnninfeq  7125  nnnninfeq2  7126  nninfisol  7130  finomni  7137  ismkvnex  7152  nninfwlpoimlemg  7172  exmidfodomrlemeldju  7197  exmidfodomrlemreseldju  7198  exmidfodomrlemr  7200  exmidfodomrlemrALT  7201  exmidaclem  7206  exmidontriimlem3  7221  netap  7252  2omotaplemap  7255  mullocprlem  7568  recexprlemloc  7629  suplocsrlem  7806  btwnapz  9382  xnn0dcle  9801  xnn0letri  9802  z2ge  9825  xaddcom  9860  xnegdi  9867  xaddass  9868  xpncan  9870  xleadd1a  9872  xsubge0  9880  xlesubadd  9882  fztri3or  10038  fzm1  10099  fzneuz  10100  exfzdc  10239  exbtwnzlemstep  10247  rebtwn2zlemstep  10252  apbtwnz  10273  modifeq2int  10385  modsumfzodifsn  10395  iseqf1olemab  10488  iseqf1olemmo  10491  seq3f1olemqsumk  10498  seq3f1olemqsum  10499  seq3f1olemstep  10500  fser0const  10515  expaddzaplem  10562  qsqeqor  10630  expnbnd  10643  nn0ltexp2  10688  apexp1  10697  bcval  10728  bccmpl  10733  bcval5  10742  bcpasc  10745  bccl  10746  hashennnuni  10758  hashnncl  10774  fiubm  10807  zfz1isolemiso  10818  resqrexlemnm  11026  resqrexlemcvg  11027  resqrexlemoverl  11029  resqrexlemglsq  11030  leabs  11082  nn0abscl  11093  ltabs  11095  abslt  11096  fzomaxdif  11121  maxleim  11213  maxabslemval  11216  zmaxcl  11232  2zsupmax  11233  minmax  11237  2zinfmin  11250  xrmaxleim  11251  xrmaxifle  11253  xrmaxiflemab  11254  xrmaxiflemlub  11255  xrmaxiflemcom  11256  xrmaxiflemval  11257  xrmaxaddlem  11267  xrmaxadd  11268  xrminmax  11272  sumdc  11365  sumrbdc  11386  summodclem3  11387  summodclem2a  11388  zsumdc  11391  isumss  11398  fisumss  11399  isumss2  11400  fsumcllem  11406  fsumadd  11413  fsumsplit  11414  fsumsplitsn  11417  sumsplitdc  11439  fisumrev2  11453  fsummulc2  11455  telfsumo  11473  fsumparts  11477  cvgratnnlemseq  11533  cvgratz  11539  fproddccvg  11579  prodrbdc  11581  zproddc  11586  prod1dc  11593  fprodssdc  11597  fprodmul  11598  fprodsplitdc  11603  fprodsplit  11604  fprodunsn  11611  fprodcllem  11613  dvdsle  11849  mod2eq1n2dvds  11883  zsupcllemstep  11945  infssuzex  11949  gcdsupex  11957  gcdsupcl  11958  gcdval  11959  gcddvds  11963  gcdcl  11966  gcd0id  11979  gcdneg  11982  bezoutlemmain  11998  bezoutlemzz  12002  bezoutlemaz  12003  bezoutlembz  12004  dfgcd3  12010  dfgcd2  12014  nn0seqcvgd  12040  eucalgf  12054  eucalginv  12055  dvdslcm  12068  lcmcl  12071  lcmneg  12073  lcmgcd  12077  lcmdvds  12078  lcmid  12079  mulgcddvds  12093  isprm5lem  12140  pw2dvdslemn  12164  sqrt2irrap  12179  phibndlem  12215  prm23ge5  12263  pclemdc  12287  pcge0  12311  pcdvdsb  12318  pceq0  12320  pcneg  12323  pcdvdstr  12325  pcgcd1  12326  pcgcd  12327  pc2dvds  12328  pcz  12330  pcprmpw2  12331  pcaddlem  12337  pcadd  12338  pcmpt  12340  pcmpt2  12341  pcprod  12343  fldivp1  12345  qexpz  12349  1arithlem4  12363  1arith  12364  ennnfonelemss  12410  ennnfonelemkh  12412  ennnfonelemhf1o  12413  ctiunctlemudc  12437  fvprif  12761  mulgnn0p1  12993  mulgnn0subcl  12995  mulgsubcl  12996  mulgneg  13000  mulgz  13009  mulgnn0dir  13011  mulgdirlem  13012  mulgdir  13013  lringuplu  13335  xblss2ps  13874  xblss2  13875  qtopbas  13992  dedekindeulemeu  14070  dedekindeu  14071  suplociccreex  14072  dedekindicclemeu  14079  dedekindicclemicc  14080  limcimolemlt  14103  cnplimclemle  14107  reeff1o  14164  efltlemlt  14165  sin0pilem2  14173  coseq0negpitopi  14227  abssinper  14237  cos02pilt1  14242  logbgcd1irraplemexp  14356  lgslem4  14374  lgsneg  14395  lgsneg1  14396  lgsmod  14397  lgsdilem  14398  lgsdir2  14404  lgsdirprm  14405  lgsdir  14406  lgsdi  14408  lgsne0  14409  lgsdirnn0  14418  lgsdinn0  14419  lgseisenlem1  14420  2sqlem4  14435  2sqlem9  14441  nnsf  14724  nninfsellemsuc  14731  trilpolemclim  14754  trilpolemisumle  14756  trilpolemeq1  14758  trilpolemlt1  14759  trirec0  14762  apdifflemf  14764  apdifflemr  14765  apdiff  14766  iswomni0  14769  nconstwlpolemgt0  14781  nconstwlpolem  14782  neapmkvlem  14784