Theorem r19.22si 1726

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

Syntax hints:   -> wi 3   e. wcel 955  E.wrex 1638

This theorem is referenced by:  r19.40 1754  reu6 1922  abrexex 3845  elunirnALT 3854  tfrlem8 3903  oarec 4180  ixp0 4345  unbnn2 4522  scott0 4689  aceq6b 4714  numthlem 4755  numthcor 4758  zorn 4769  uniimadom 4782  cflim 4881  fsequb2 6456  cau3ir 6852  cau5i 6854  cvg3 6860  cvganz 6861  clm3 7017  clmi1 7024  clmi2 7025  clm0i 7027  climunii 7035  climsup 7091  ivthlem3 7218  ivthlem6 7221  ivthlem7 7222  ivthlem6OLD 7230  ivthlem7OLD 7231  basgen2t 7581  cnpco 7708  sncld 7726  blssex 7794  lmcvg2 7871  caun0 7880  lmfexlem3 7893  grprcan 7997  grpinveu 7998  ring2 8086  axgroth3 8718  grothinf 8720  hlimunii 9029  fgsb 10444  fgsb2 10449  dtt2 10462

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

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-ral 1641  df-rex 1642

Copyright terms: Public domain