ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpjaodan Unicode version

Theorem mpjaodan 788
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
StepHypRef Expression
1 jaodan.3 . 2  |-  ( ph  ->  ( ps  \/  th ) )
2 jaodan.1 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
3 jaodan.2 . . 3  |-  ( (
ph  /\  th )  ->  ch )
42, 3jaodan 787 . 2  |-  ( (
ph  /\  ( ps  \/  th ) )  ->  ch )
51, 4mpdan 418 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    \/ wo 698
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 699
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  mpjao3dan  1286  dcun  3478  ifcldadc  3506  ifeq1dadc  3507  ifbothdadc  3508  ifcldcd  3512  exmidn0m  4132  exmidsssn  4133  exmidundif  4137  exmidundifim  4138  ordtri2or2exmidlem  4449  reg2exmidlema  4457  nnpredcl  4544  frecabcl  6304  nnsucuniel  6399  dcdifsnid  6408  phpm  6767  fidifsnen  6772  dif1enen  6782  fin0  6787  fimax2gtrilemstep  6802  finexdc  6804  en2eqpr  6809  fientri3  6811  unsnfidcex  6816  unsnfidcel  6817  undifdcss  6819  fiintim  6825  ssfirab  6830  fidcenumlemrks  6849  fidcenumlemr  6851  omp1eomlem  6987  difinfsnlem  6992  difinfsn  6993  ctssdccl  7004  ctssdc  7006  enumct  7008  finomni  7020  nnnninf  7031  ismkvnex  7037  exmidfodomrlemeldju  7072  exmidfodomrlemreseldju  7073  exmidfodomrlemr  7075  exmidfodomrlemrALT  7076  exmidaclem  7081  mullocprlem  7402  recexprlemloc  7463  suplocsrlem  7640  btwnapz  9205  z2ge  9639  xaddcom  9674  xnegdi  9681  xaddass  9682  xpncan  9684  xleadd1a  9686  xsubge0  9694  xlesubadd  9696  fztri3or  9850  fzm1  9911  fzneuz  9912  exfzdc  10048  exbtwnzlemstep  10056  rebtwn2zlemstep  10061  apbtwnz  10078  modifeq2int  10190  modsumfzodifsn  10200  iseqf1olemab  10293  iseqf1olemmo  10296  seq3f1olemqsumk  10303  seq3f1olemqsum  10304  seq3f1olemstep  10305  fser0const  10320  expaddzaplem  10367  expnbnd  10446  apexp1  10496  bcval  10527  bccmpl  10532  bcval5  10541  bcpasc  10544  bccl  10545  hashennnuni  10557  hashnncl  10574  zfz1isolemiso  10614  resqrexlemnm  10822  resqrexlemcvg  10823  resqrexlemoverl  10825  resqrexlemglsq  10826  leabs  10878  nn0abscl  10889  ltabs  10891  abslt  10892  fzomaxdif  10917  maxleim  11009  maxabslemval  11012  zmaxcl  11028  2zsupmax  11029  minmax  11033  xrmaxleim  11045  xrmaxifle  11047  xrmaxiflemab  11048  xrmaxiflemlub  11049  xrmaxiflemcom  11050  xrmaxiflemval  11051  xrmaxaddlem  11061  xrmaxadd  11062  xrminmax  11066  sumdc  11159  sumrbdc  11180  summodclem3  11181  summodclem2a  11182  zsumdc  11185  isumss  11192  fisumss  11193  isumss2  11194  fsumcllem  11200  fsumadd  11207  fsumsplit  11208  fsumsplitsn  11211  sumsplitdc  11233  fisumrev2  11247  fsummulc2  11249  telfsumo  11267  fsumparts  11271  cvgratnnlemseq  11327  cvgratz  11333  fproddccvg  11373  prodrbdc  11375  zproddc  11380  dvdsle  11578  mod2eq1n2dvds  11612  zsupcllemstep  11674  infssuzex  11678  gcdsupex  11682  gcdsupcl  11683  gcdval  11684  gcddvds  11688  gcdcl  11691  gcd0id  11703  gcdneg  11706  bezoutlemmain  11722  bezoutlemzz  11726  bezoutlemaz  11727  bezoutlembz  11728  dfgcd3  11734  dfgcd2  11738  nn0seqcvgd  11758  eucalgf  11772  eucalginv  11773  dvdslcm  11786  lcmcl  11789  lcmneg  11791  lcmgcd  11795  lcmdvds  11796  lcmid  11797  mulgcddvds  11811  pw2dvdslemn  11879  sqrt2irrap  11894  phibndlem  11928  ennnfonelemss  11959  ennnfonelemkh  11961  ennnfonelemhf1o  11962  ctiunctlemudc  11986  xblss2ps  12612  xblss2  12613  qtopbas  12730  dedekindeulemeu  12808  dedekindeu  12809  suplociccreex  12810  dedekindicclemeu  12817  dedekindicclemicc  12818  limcimolemlt  12841  cnplimclemle  12845  reeff1o  12902  efltlemlt  12903  sin0pilem2  12911  coseq0negpitopi  12965  abssinper  12975  cos02pilt1  12980  logbgcd1irraplemexp  13093  nnsf  13374  nninfalllemn  13377  nninfsellemsuc  13383  trilpolemclim  13404  trilpolemisumle  13406  trilpolemeq1  13408  trilpolemlt1  13409  trirec0  13412  apdifflemf  13414  apdifflemr  13415  apdiff  13416  neapmkvlem  13424
  Copyright terms: Public domain W3C validator