Theorem mpjaodan 753

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  mpjao3dan  1253  dcun  3420  ifcldadc  3448  ifeq1dadc  3449  ifbothdadc  3450  ifcldcd  3454  exmidn0m  4062  exmidsssn  4063  exmidundif  4067  exmidundifim  4068  ordtri2or2exmidlem  4379  reg2exmidlema  4387  nnpredcl  4474  frecabcl  6226  nnsucuniel  6321  dcdifsnid  6330  phpm  6688  fidifsnen  6693  dif1enen  6703  fin0  6708  fimax2gtrilemstep  6723  finexdc  6725  en2eqpr  6730  fientri3  6732  unsnfidcex  6737  unsnfidcel  6738  undifdcss  6740  fiintim  6746  ssfirab  6750  fidcenumlemrks  6769  fidcenumlemr  6771  omp1eomlem  6894  difinfsnlem  6899  difinfsn  6900  ctssdclemr  6911  ctssdc  6912  enumct  6914  finomni  6924  nnnninf  6935  exmidfodomrlemeldju  6964  exmidfodomrlemreseldju  6965  exmidfodomrlemr  6967  exmidfodomrlemrALT  6968  mullocprlem  7279  recexprlemloc  7340  btwnapz  9033  z2ge  9450  xaddcom  9485  xnegdi  9492  xaddass  9493  xpncan  9495  xleadd1a  9497  xsubge0  9505  xlesubadd  9507  fztri3or  9660  fzm1  9721  fzneuz  9722  exfzdc  9858  exbtwnzlemstep  9866  rebtwn2zlemstep  9871  apbtwnz  9888  modifeq2int  10000  modsumfzodifsn  10010  iseqf1olemab  10103  iseqf1olemmo  10106  seq3f1olemqsumk  10113  seq3f1olemqsum  10114  seq3f1olemstep  10115  fser0const  10130  expaddzaplem  10177  expnbnd  10256  bcval  10336  bccmpl  10341  bcval5  10350  bcpasc  10353  bccl  10354  hashennnuni  10366  hashnncl  10383  zfz1isolemiso  10423  resqrexlemnm  10630  resqrexlemcvg  10631  resqrexlemoverl  10633  resqrexlemglsq  10634  leabs  10686  nn0abscl  10697  ltabs  10699  abslt  10700  fzomaxdif  10725  maxleim  10817  maxabslemval  10820  zmaxcl  10835  2zsupmax  10836  minmax  10840  xrmaxleim  10852  xrmaxifle  10854  xrmaxiflemab  10855  xrmaxiflemlub  10856  xrmaxiflemcom  10857  xrmaxiflemval  10858  xrmaxaddlem  10868  xrmaxadd  10869  xrminmax  10873  sumdc  10966  sumrbdc  10986  summodclem3  10988  summodclem2a  10989  zsumdc  10992  isumss  10999  fisumss  11000  isumss2  11001  fsumcllem  11007  fsumadd  11014  fsumsplit  11015  fsumsplitsn  11018  sumsplitdc  11040  fisumrev2  11054  fsummulc2  11056  telfsumo  11074  fsumparts  11078  cvgratnnlemseq  11134  cvgratz  11140  dvdsle  11337  mod2eq1n2dvds  11371  zsupcllemstep  11433  infssuzex  11437  gcdsupex  11441  gcdsupcl  11442  gcdval  11443  gcddvds  11447  gcdcl  11450  gcd0id  11462  gcdneg  11465  bezoutlemmain  11479  bezoutlemzz  11483  bezoutlemaz  11484  bezoutlembz  11485  dfgcd3  11491  dfgcd2  11495  nn0seqcvgd  11515  eucalgf  11529  eucalginv  11530  dvdslcm  11543  lcmcl  11546  lcmneg  11548  lcmgcd  11552  lcmdvds  11553  lcmid  11554  mulgcddvds  11568  pw2dvdslemn  11635  sqrt2irrap  11650  phibndlem  11684  ennnfonelemss  11715  ennnfonelemkh  11717  ennnfonelemhf1o  11718  xblss2ps  12332  xblss2  12333  qtopbas  12444  limcimolemlt  12513  nnsf  12783  nninfalllemn  12786  nninfsellemsuc  12792  trilpolemclim  12813  trilpolemisumle  12815  trilpolemeq1  12817  trilpolemlt1  12818