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

Theorem eximdv 1860
Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.)
Hypothesis
Ref Expression
alimdv.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
eximdv  |-  ( ph  ->  ( E. x ps 
->  E. x ch )
)
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)

Proof of Theorem eximdv
StepHypRef Expression
1 ax-17 1506 . 2  |-  ( ph  ->  A. x ph )
2 alimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2eximdh 1591 1  |-  ( ph  ->  ( E. x ps 
->  E. x ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1472
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-5 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-17 1506  ax-ial 1514
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  2eximdv  1862  reximdv2  2556  cgsexg  2747  spc3egv  2804  euind  2899  ssel  3122  reupick  3391  reximdva0m  3409  uniss  3794  eusvnfb  4415  coss1  4742  coss2  4743  dmss  4786  dmcosseq  4858  funssres  5213  imain  5253  brprcneu  5462  fv3  5492  dffo4  5616  dffo5  5617  f1eqcocnv  5742  mapsn  6636  ctssdccl  7056  acfun  7143  ccfunen  7185  cc4f  7190  cc4n  7192  dmaddpq  7300  dmmulpq  7301  recexprlemlol  7547  recexprlemupu  7549  ioom  10164  ctinfom  12199  ctinf  12201  omctfn  12214  nninfdclemp1  12223  txcn  12717
  Copyright terms: Public domain W3C validator