Theorem r19.23aiva 1741

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 373	. 2 |- (x e. A -> (ph -> ps))
3	2	r19.23aiv 1740	1 |- (E.x e. A ph -> ps)

Syntax hints:   -> wi 3   /\ wa 223   e. wcel 956  E.wrex 1643

This theorem is referenced by:  unon 3083  tfrlem8 3909  oawordeulem 4178  nneob 4245  ominf 4514  isfinite1 4516  pwfi 4551  alephfp 4880  0cnALT 5330  addcan 5331  1re 5415  mulcan 5667  om2uzran 6245  clm3 7025  subtop 7596  neiint 7669  neips 7677  metcnp4 7920  iscms2lem4 7942  ubthlem6 8478  minveclem14 8502  norm1ex 9061  lnopcon 9901  lnfncon 9928  pjssdif1 10041  pjhmopidm 10048  str 10122  hstr 10130  stcltrth 10143  shatomic 10222  fgsb 10480  fgsb2 10485

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-rex 1647

Copyright terms: Public domain