Theorem r19.23aiva 1744

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 1743	1 |- (E.x e. A ph -> ps)

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

This theorem is referenced by:  unon 3088  tfrlem8 3918  oawordeulem 4188  nneob 4255  ominfOLD 4529  isfinite1OLD 4531  pwfiOLD 4571  alephfp 4900  0cnALT 5350  addcan 5351  1re 5435  mulcan 5686  mulcanOLD 5687  om2uzran 6300  clm3 7079  subtop 7646  neiint 7719  neips 7727  metcnp4 7970  iscms2lem4 7992  ubthlem6 8534  minveclem14 8558  norm1ex 9122  lnopcon 9963  lnfncon 9990  pjssdif1 10103  pjhmopidm 10110  str 10184  hstr 10192  stcltrth 10205  shatomic 10285  fgsb 10570  fgsbOLD 10571  fgsb2 10580

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-rex 1650

Copyright terms: Public domain