Theorem r19.22i 1729

Description: Inference quantifying both antecedent and consequent.

Hypothesis

Ref	Expression
r19.22i.1	|- (x e. A -> (ph -> ps))

Assertion

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

Proof of Theorem r19.22i

Step	Hyp	Ref	Expression
1		r19.22 1728	. 2 |- (A.x e. A (ph -> ps) -> (E.x e. A ph -> E.x e. A ps))
2		r19.22i.1	. 2 |- (x e. A -> (ph -> ps))
3	1, 2	mprg 1697	1 |- (E.x e. A ph -> E.x e. A ps)

Syntax hints:   -> wi 3   e. wcel 956  E.wrex 1643

This theorem is referenced by:  r19.22si 1731  iunpw 2909  tz7.49c 3951  abianfp 3953  trcl 4625  rankwflem 4645  xrsupexmnf 6029  xrinfmexpnf 6030  zqt 6206  seq1ublem 6856  cau3i 6859  cau4i 6863  cau5 6864  cvg1i 6865  caubnd 6871  caucvglem2 7102  metelcls 7916  metcnp4 7920  ubthlem6 8478  norm1ex 9061  projlem16 9140  chrelat2 10229

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

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

Copyright terms: Public domain