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

Theorem eximdv 1880
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 1526 . 2  |-  ( ph  ->  A. x ph )
2 alimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2eximdh 1611 1  |-  ( ph  ->  ( E. x ps 
->  E. x ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1492
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  2eximdv  1882  reximdv2  2576  cgsexg  2774  spc3egv  2831  euind  2926  ssel  3151  reupick  3421  reximdva0m  3440  uniss  3832  eusvnfb  4456  coss1  4784  coss2  4785  dmss  4828  dmcosseq  4900  funssres  5260  imain  5300  brprcneu  5510  fv3  5540  dffo4  5666  dffo5  5667  f1eqcocnv  5794  mapsn  6692  ctssdccl  7112  acfun  7208  ccfunen  7265  cc4f  7270  cc4n  7272  dmaddpq  7380  dmmulpq  7381  recexprlemlol  7627  recexprlemupu  7629  ioom  10263  ctinfom  12431  ctinf  12433  omctfn  12446  nninfdclemp1  12453  ptex  12718  subgintm  13063  txcn  13860
  Copyright terms: Public domain W3C validator