Theorem r19.22dv 1737

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 971	. 2 |- (ph -> A.xph)
2		r19.22dv.1	. 2 |- (ph -> (x e. A -> (ps -> ch)))
3	1, 2	r19.22d 1735	1 |- (ph -> (E.x e. A ps -> E.x e. A ch))

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

This theorem is referenced by:  r19.22sdv 1738  r19.22dva 1739  r19.12 1740  wefrc 2943  isomin 3899  isofrlem 3901  oaordex 4192  odi 4210  omass 4211  r1pwcl 4687  climsup 7155  reccnv 7218  grpidinv 8052  cvat 10293  atcvat4 10324  mdsymlem2 10331  mdsymlem3 10332  sumdmdi 10342

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  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