Theorem r19.22si 1732

Description: Inference quantifying both antecedent and consequent.

Hypothesis

Ref	Expression
r19.22si.1	|- (ph -> ps)

Assertion

Ref	Expression
r19.22si	|- (E.x e. A ph -> E.x e. A ps)

Proof of Theorem r19.22si

Step	Hyp	Ref	Expression
1		r19.22si.1	. . 3 |- (ph -> ps)
2	1	a1i 8	. 2 |- (x e. A -> (ph -> ps))
3	2	r19.22i 1730	1 |- (E.x e. A ph -> E.x e. A ps)

Syntax hints:   -> wi 3   e. wcel 957  E.wrex 1644

This theorem is referenced by:  r19.40 1760  reu6 1929  abrexex 3855  elunirnALT 3864  tfrlem8 3913  oarec 4189  ixp0 4354  unbnn2 4531  scott0 4700  aceq6b 4725  numthlem 4766  numthcor 4769  zorn 4780  uniimadom 4793  cflim 4892  fsequb2 6469  cau3ir 6867  cau5i 6869  cvg3 6875  cvganz 6876  clm3 7032  clmi1 7039  clmi2 7040  clm0i 7042  climunii 7051  climsup 7108  ivthlem3 7235  ivthlem6 7238  ivthlem7 7239  ivthlem6OLD 7247  ivthlem7OLD 7248  basgen2t 7599  cnpco 7729  sncld 7747  blssex 7816  lmcvg2 7895  caun0 7907  lmfexlem3 7920  grprcan 8025  grpinveu 8026  ring2 8113  axgroth3 8734  grothinf 8736  hlimunii 9063  fgsb 10503  fgsb2 10508  dtt2 10534

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-4 972  ax-5o 974

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-ral 1647  df-rex 1648

Copyright terms: Public domain