Theorem r19.23aiva 1790

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version).

Hypothesis

Ref	Expression
r19.23aiva.1	|- ((x e. A /\ ph) -> ps)

Assertion

Ref	Expression
r19.23aiva	|- (E.x e. A ph -> ps)

Distinct variable group:   ps,x

Proof of Theorem r19.23aiva

Step	Hyp	Ref	Expression
1		r19.23aiva.1	. . 3 |- ((x e. A /\ ph) -> ps)
2	1	ex 371	. 2 |- (x e. A -> (ph -> ps))
3	2	r19.23aiv 1789	1 |- (E.x e. A ph -> ps)

Syntax hints:   -> wi 3   /\ wa 221   e. wcel 994  E.wrex 1692

This theorem is referenced by:  unon 3185  tfrlem8 4219  oawordeulem 4324  nneob 4395  ominf 4675  isfinite1 4677  alephfp 5050  0cnALT 5504  addcani 5505  1re 5589  mulcani 5842  om2uzrani 6663  clm3i 7282  subtop 7858  neiint 7929  neips 7937  metcnp4 8181  iscms2lem4 8203  ubthlem6 8792  minveclem14 8818  norm1exi 9398  lnopconi 10242  lnfnconi 10269  pjssdif1i 10383  pjhmopidm 10390  stri 10465  hstri 10473  stcltrthi 10486  shatomici 10566  sallnei 11016  fgsb 11082  fgsb2 11086  fcluscomp 11733  raleqfn 11790  sdclem2 11876  sdc 11877  heiborlem38 12048

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-rex 1696

Copyright terms: Public domain