Theorem r19.20dva 1706

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:   ph,x

Proof of Theorem r19.20dva

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

Syntax hints:   -> wi 3   /\ wa 223   e. wcel 956  A.wral 1642

This theorem is referenced by:  r19.20sdv 1707  onint 3001  tfrlem1 3902  aceq5 4720  alephle 4864  xrsupsslem 6031  xrinfmsslem 6032  uzwo4OLD 6166  uzwo 6395  uzwoOLD 6396  seq1bnd 6855  cau3ir 6860  cau5i 6862  cau4i 6863  cau5 6864  cvg1i 6865  cvg2 6867  cvg3 6868  cvganz 6869  caubnd 6871  caure 6872  cauim 6873  clm3 7025  clm4le 7027  2climnn 7047  2climnn0 7048  climaddlem3 7060  climaddc1 7062  climmullem8 7071  climmulc2 7073  climsubc2 7075  climcmpc1 7083  climsqueeze 7084  climsqueeze2 7085  caucvglem2 7102  caucvglem4 7104  caucvglem5 7105  cvgcmp3c 7130  reccnv 7161  infcvglem3 7166  expcnv 7176  fsum0diaglem2 7200  fsum0diag3 7203  rescncf 7215  infpnlem1 7457  metcnpi3 7844  metcnpi4 7845  metcni2 7847  metcnss2 7851  lmnn 7887  metcnp4lem2 7919  xplmi 7923  xplm 7925  xpcn 7926  iscms2lem3 7941  iscms2lem4 7942  lmcau 7946  nvlmle 8281  nmoub3i 8381  ubthlem5 8477  minveclem25 8513  minveclem26 8514  minveclem27 8515  htthlem7 8569  htthlem12 8574  hlimcaui 9045  ocsh 9095  occllem6 9117  occl 9120  projlem25 9149  chintcl 9233  osumlem4 9521  nmopub2tALT 9773  nmfnleub2t 9789  nlelch 9932  riesz1t 9936  leopaddt 10003  leopmulit 10004  leoptrt 10008  hmopidmch 10017  dmdbr3 10170  dmdbr4 10171  mdsl0 10174  mdsymlem6 10272  cdj1 10294  hmphsyma 10451  icmpmon 10623

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