Theorem r19.20sdv 1702

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 1701	1 |- (ph -> (A.x e. A ps -> A.x e. A ch))

Syntax hints:   -> wi 3   e. wcel 955  A.wral 1637

This theorem is referenced by:  tfindsg 3152  dffo4 3805  dffo5 3806  abianfp 3947  rankval3 4653  bndrank 4654  cfub 4880  cau3i 6851  fsumcom 6966  fsummulc2 6972  fsumdivc 6973  fsumdivcALT 6974  fsum2mul 6975  climconst 7031  2climnn 7039  2climnn0 7040  climaddc2 7055  climsqueeze 7076  climsqueeze2 7077  rescncf 7207  iincld 7621  cnpco 7708  cnsscnp 7711  cncnplem4 7716  cncnp 7717  metcnss2 7838  lmuni 7886  caussi 7889  metcnp4lem2 7903  iscms2lem3 7925  lmcau 7930  nmlnoubi 8388  cnrsfin 10396

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972

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

Copyright terms: Public domain