Theorem r19.22i 1732

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

Syntax hints:   -> wi 3   e. wcel 958  E.wrex 1646

This theorem is referenced by:  r19.22si 1734  iunpw 2914  tz7.49c 3960  abianfp 3962  trcl 4645  rankwflem 4665  xrsupexmnf 6074  xrinfmexpnf 6075  zqt 6260  seq1ublem 6911  cau3i 6914  cau4i 6918  cau5 6919  cvg1i 6920  caubnd 6926  caucvglem2 7158  metelcls 7965  metcnp4 7970  ubthlem6 8534  norm1ex 9122  projlem16 9201  chrelat2 10292

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

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

Copyright terms: Public domain