Theorem r19.20dva 1709

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 971	. 2 |- (ph -> A.xph)
2		r19.20dva.1	. 2 |- ((ph /\ x e. A) -> (ps -> ch))
3	1, 2	r19.20da 1708	1 |- (ph -> (A.x e. A ps -> A.x e. A ch))

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

This theorem is referenced by:  r19.20sdv 1710  onint 3006  tfrlem1 3911  aceq5 4740  alephle 4884  xrsupsslem 6076  xrinfmsslem 6077  uzwo4OLD 6210  uzwo 6455  uzwoOLD 6456  seq1bnd 6910  cau3ir 6915  cau5i 6917  cau4i 6918  cau5 6919  cvg1i 6920  cvg2 6922  cvg3 6923  cvganz 6924  caubnd 6926  caure 6927  cauim 6928  clm3 7079  clm4le 7081  2climnn 7102  2climnn0 7103  climaddlem3 7116  climaddc1 7118  climmullem8 7127  climmulc2 7129  climsubc2 7131  climcmpc1 7139  climsqueeze 7140  climsqueeze2 7141  caucvglem2 7158  caucvglem4 7160  caucvglem5 7161  cvgcmp3c 7186  reccnv 7218  infcvglem3 7223  expcnv 7233  fsum0diaglem2 7257  fsum0diag3 7260  rescncf 7272  infpnlem1 7506  metcnpi3 7892  metcnpi4 7893  metcni2 7895  metcnss2 7899  lmnn 7935  metcnp4lem2 7969  xplmi 7973  xplm 7975  xpcn 7976  iscms2lem3 7991  iscms2lem4 7992  lmcau 7996  nvlmle 8333  nmoub3i 8436  ubthlem5 8533  minveclem25 8569  minveclem26 8570  minveclem27 8571  htthlem7 8626  htthlem12 8631  hlimcaui 9106  ocsh 9156  occllem6 9178  occl 9181  projlem25 9210  chintcl 9295  osumlem4 9581  nmopub2tALT 9833  nmfnleub2t 9850  nlelch 9994  riesz1t 9998  leopaddt 10065  leopmulit 10066  leoptrt 10070  hmopidmch 10079  dmdbr3 10232  dmdbr4 10233  dmdbr5 10235  mdsl0 10237  mdsymlem6 10335  cdj1 10360  hmphsyma 10528  icmpmon 10744

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