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

Theorem exlimddv 1854
Description: Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.)
Hypotheses
Ref Expression
exlimddv.1  |-  ( ph  ->  E. x ps )
exlimddv.2  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
exlimddv  |-  ( ph  ->  ch )
Distinct variable groups:    ch, x    ph, x
Allowed substitution hint:    ps( x)

Proof of Theorem exlimddv
StepHypRef Expression
1 exlimddv.1 . 2  |-  ( ph  ->  E. x ps )
2 exlimddv.2 . . . 4  |-  ( (
ph  /\  ps )  ->  ch )
32ex 114 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
43exlimdv 1775 . 2  |-  ( ph  ->  ( E. x ps 
->  ch ) )
51, 4mpd 13 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103   E.wex 1453
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia3 107  ax-5 1408  ax-gen 1410  ax-ie2 1455  ax-17 1491
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  fvmptdv2  5478  tfrlemi14d  6198  tfrexlem  6199  tfr1onlemres  6214  tfrcllemres  6227  tfrcldm  6228  erref  6417  xpdom2  6693  dom0  6700  xpen  6707  mapdom1g  6709  phplem4dom  6724  phplem4on  6729  fidceq  6731  dif1en  6741  fin0  6747  fin0or  6748  isinfinf  6759  infm  6766  en2eqpr  6769  fiuni  6834  supelti  6857  djudom  6946  difinfsn  6953  enomnilem  6978  exmidfodomrlemim  7025  exmidaclem  7032  genpml  7293  genpmu  7294  ltexprlemm  7376  ltexprlemfl  7385  ltexprlemfu  7387  suplocsr  7585  axpre-suploc  7678  eqord1  8213  nn1suc  8703  seq3f1oleml  10231  zfz1isolem1  10538  ennnfonelemim  11848  exmidunben  11850  enctlem  11856  ctiunct  11864  unct  11865  lmff  12329  txcn  12355  suplociccreex  12682  suplociccex  12683  subctctexmid  13092  exmidsbthrlem  13113  sbthom  13117
  Copyright terms: Public domain W3C validator