Theorem mpjaodan 745

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

Syntax hints:   -> wi 4   /\ wa 102   \/ wo 662

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  mpjao3dan  1241  ifcldadc  3406  ifeq1dadc  3407  ifbothdadc  3408  ifcldcd  3412  exmidundif  4008  ordtri2or2exmidlem  4314  reg2exmidlema  4322  frecabcl  6112  nnsucuniel  6204  dcdifsnid  6211  phpm  6527  fidifsnen  6532  dif1enen  6542  fin0  6547  fimax2gtrilemstep  6562  finexdc  6564  en2eqpr  6569  fientri3  6571  unsnfidcex  6576  unsnfidcel  6577  undifdcss  6579  ssfirab  6587  finomni  6733  nnnninf  6743  exmidfodomrlemeldju  6762  exmidfodomrlemreseldju  6763  exmidfodomrlemr  6765  exmidfodomrlemrALT  6766  mullocprlem  7066  recexprlemloc  7127  z2ge  9213  fztri3or  9378  fzm1  9437  fzneuz  9438  exfzdc  9572  exbtwnzlemstep  9580  rebtwn2zlemstep  9585  apbtwnz  9602  modifeq2int  9714  modsumfzodifsn  9724  iseqf1olemab  9815  iseqf1olemmo  9818  iseqf1olemqsumk  9825  iseqf1olemqsum  9826  iseqf1olemstep  9827  fser0const  9842  expaddzaplem  9889  expnbnd  9966  bcval  10046  bccmpl  10051  ibcval5  10060  bcpasc  10063  bccl  10064  hashennnuni  10076  hashnncl  10093  zfz1isolemiso  10133  resqrexlemnm  10339  resqrexlemcvg  10340  resqrexlemoverl  10342  resqrexlemglsq  10343  leabs  10395  nn0abscl  10406  ltabs  10408  abslt  10409  fzomaxdif  10434  maxleim  10526  maxabslemval  10529  minmax  10547  sumdc  10630  isumrb  10650  isummolem3  10652  isummolem2a  10653  zisum  10656  isumss  10662  dvdsle  10712  mod2eq1n2dvds  10746  zsupcllemstep  10808  infssuzex  10812  gcdsupex  10816  gcdsupcl  10817  gcdval  10818  gcddvds  10822  gcdcl  10825  gcd0id  10837  gcdneg  10840  bezoutlemmain  10854  bezoutlemzz  10858  bezoutlemaz  10859  bezoutlembz  10860  dfgcd3  10866  dfgcd2  10870  nn0seqcvgd  10890  eucalgf  10904  eucalginv  10905  dvdslcm  10918  lcmcl  10921  lcmneg  10923  lcmgcd  10927  lcmdvds  10928  lcmid  10929  mulgcddvds  10943  pw2dvdslemn  11010  sqrt2irrap  11025  phibndlem  11059  nnpredcl  11320  nnsf  11325  nninfalllemn  11328  nninfsellemsuc  11334