Theorem r19.20sdv 1710

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

Syntax hints:   -> wi 3   e. wcel 958  A.wral 1645

This theorem is referenced by:  tfindsg 3162  dffo4 3820  dffo5 3821  abianfp 3962  rankval3 4681  bndrank 4682  cfub 4908  cau3i 6914  fsumcom 7028  fsummulc2 7034  fsumdivc 7035  fsumdivcALT 7036  fsum2mul 7037  climconst 7094  2climnn 7102  2climnn0 7103  climaddc2 7119  climsqueeze 7140  climsqueeze2 7141  rescncf 7272  iincld 7679  cnpco 7769  cnsscnp 7772  cncnplem4 7777  cncnp 7778  metcnss2 7899  lmuni 7951  caussi 7954  metcnp4lem2 7969  iscms2lem3 7991  lmcau 7996  nmlnoubi 8456  lnon0 8458  cnrsfin 10509

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-ral 1649

Copyright terms: Public domain