Theorem r19.20sdv 1707

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

Hypothesis

Ref	Expression
r19.20sdv.1	|- (ph -> (ps -> ch))

Assertion

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

Distinct variable group:   ph,x

Proof of Theorem r19.20sdv

Step	Hyp	Ref	Expression
1		r19.20sdv.1	. . 3 |- (ph -> (ps -> ch))
2	1	adantr 389	. 2 |- ((ph /\ x e. A) -> (ps -> ch))
3	2	r19.20dva 1706	1 |- (ph -> (A.x e. A ps -> A.x e. A ch))

Syntax hints:   -> wi 3   e. wcel 956  A.wral 1642

This theorem is referenced by:  tfindsg 3157  dffo4 3811  dffo5 3812  abianfp 3953  rankval3 4661  bndrank 4662  cfub 4888  cau3i 6859  fsumcom 6974  fsummulc2 6980  fsumdivc 6981  fsumdivcALT 6982  fsum2mul 6983  climconst 7039  2climnn 7047  2climnn0 7048  climaddc2 7063  climsqueeze 7084  climsqueeze2 7085  rescncf 7215  iincld 7629  cnpco 7719  cnsscnp 7722  cncnplem4 7727  cncnp 7728  metcnss2 7851  lmuni 7902  caussi 7905  metcnp4lem2 7919  iscms2lem3 7941  lmcau 7946  nmlnoubi 8401  cnrsfin 10432

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

This theorem depends on definitions:  df-bi 147  df-an 225  df-ral 1646

Copyright terms: Public domain