Theorem r19.22dv 1740

Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90.

Hypothesis

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

Assertion

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

Distinct variable group:   ph,x

Proof of Theorem r19.22dv

Step	Hyp	Ref	Expression
1		ax-17 973	. 2 |- (ph -> A.xph)
2		r19.22dv.1	. 2 |- (ph -> (x e. A -> (ps -> ch)))
3	1, 2	r19.22d 1738	1 |- (ph -> (E.x e. A ps -> E.x e. A ch))

Syntax hints:   -> wi 3   e. wcel 960  E.wrex 1649

This theorem is referenced by:  r19.22sdv 1741  r19.22dva 1742  r19.12 1743  wefrc 2949  isomin 3905  isofrlem 3907  oaordex 4198  odi 4216  omass 4217  r1pwcl 4697  climsup 7155  reccnv 7218  grpidinv 8049  cvat 10288  atcvat4 10319  mdsymlem2 10326  mdsymlem3 10327  sumdmdi 10337

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

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-ral 1652  df-rex 1653

Copyright terms: Public domain