Theorem r19.20dva 1256

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

Hypothesis

Ref	Expression
r19.20dva.1	|- ((ph /\ x e. A) -> (ps -> ch))

Assertion

Ref	Expression
r19.20dva	|- (ph -> (A.x e. A ps -> A.x e. A ch))

Distinct variable group(s):   ph,x

Proof of Theorem r19.20dva

Step	Hyp	Ref	Expression
1		ax-17 925	. 2 |- (ph -> A.xph)
2		r19.20dva.1	. 2 |- ((ph /\ x e. A) -> (ps -> ch))
3	1, 2	r19.20da 1255	1 |- (ph -> (A.x e. A ps -> A.x e. A ch))

Syntax hints:   -> wi 2   /\ wa 196   e. wcel 1092  A.wral 1201

This theorem is referenced by:  r19.20sdv 1257  onint 2261  tfrlem1 2949  aceq5 3563  alephle 3689  uzwo 4605  nnwoOLD 4608  hlimcaui 5141  ocsh 5164  occllem6 5185  occl 5188  projlem25 5217  chintcl 5296  osumlem4 5533  mdsymlem6 5781

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925

This theorem depends on definitions:  df-bi 128  df-an 198  df-ral 1205

metamath.org