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

Theorem eximdv 1802
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 1460 . 2  |-  ( ph  ->  A. x ph )
2 alimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2eximdh 1543 1  |-  ( ph  ->  ( E. x ps 
->  E. x ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1422
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  2eximdv  1804  reximdv2  2461  cgsexg  2635  spc3egv  2690  euind  2780  ssel  2994  reupick  3255  reximdva0m  3270  uniss  3630  eusvnfb  4212  coss1  4519  coss2  4520  dmss  4562  dmcosseq  4631  funssres  4972  imain  5012  brprcneu  5202  fv3  5229  dffo4  5347  dffo5  5348  f1eqcocnv  5462  dmaddpq  6631  dmmulpq  6632  recexprlemlol  6878  recexprlemupu  6880  ioom  9347
  Copyright terms: Public domain W3C validator