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

Theorem eximdv 1852
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 1590 1  |-  ( ph  ->  ( E. x ps 
->  E. x ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1468
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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  2eximdv  1854  reximdv2  2531  cgsexg  2721  spc3egv  2777  euind  2871  ssel  3091  reupick  3360  reximdva0m  3378  uniss  3757  eusvnfb  4375  coss1  4694  coss2  4695  dmss  4738  dmcosseq  4810  funssres  5165  imain  5205  brprcneu  5414  fv3  5444  dffo4  5568  dffo5  5569  f1eqcocnv  5692  mapsn  6584  ctssdccl  6996  acfun  7063  ccfunen  7079  cc4f  7084  cc4n  7086  dmaddpq  7194  dmmulpq  7195  recexprlemlol  7441  recexprlemupu  7443  ioom  10045  ctinfom  11947  ctinf  11949  omctfn  11962  txcn  12453
  Copyright terms: Public domain W3C validator