Theorem r19.20si 1682

Description: Inference quantifying both antecedent and consequent, with strong hypothesis.

Hypothesis

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

Assertion

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

Proof of Theorem r19.20si

Step	Hyp	Ref	Expression
1		r19.20si.1	. . 3 |- (ph -> ps)
2	1	a1i 8	. 2 |- (x e. A -> (ph -> ps))
3	2	r19.20i 1680	1 |- (A.x e. A ph -> A.x e. A ps)

Syntax hints:   -> wi 3   e. wcel 1105  A.wral 1621

This theorem is referenced by:  r19.20sii 1683  reu6 1903  uniss2 2497  iunss2 2563  tfis 3090  find 3118  dffun7 3481  fununi 3503  fun11uni 3505  zfrep6 3554  fnopabg 3555  elrnopabg 3739  dffo5 3760  fopab2 3762  elrnoprabg 4062  unifi2 4485  iunfi 4495  rankonid 4619  aceq5 4664  ac5b 4677  ac6lem 4678  ac6 4679  kmlem6 4694  kmlem8 4696  kmlem13 4701  xrsupexmnf 5972  xrinfmexpnf 5973  cau3ir 6803  cau3 6804  cvganz 6812  2sumeq2dv 6883  fsum1s 6898  fsump1s 6902  fsumadd 6911  csbfsum 6916  fsummulc1 6922  fsumcmp 6929  fsumcmp0 6930  fsumcmpndx2 6931  fsumabs 6932  fsumabs2mul 6933  serzmulc1 6946  clm3 6968  clmi2 6976  clm0i 6978  climunii 6986  2climnn 6990  2climnn0 6991  climge0 7000  iserzmulc1 7023  climcmplem 7024  climsqueeze 7027  climsqueeze2 7028  iserzcmp 7029  caucvg3 7054  iserzgt0 7097  basgen2t 7532  bastop 7535  neips 7616  cncnp 7665  meteq0 7699  mettri2 7700  mettri4 7701  lmcvg2 7819  caun0 7828  xplm 7857  iscms2 7876  isgrp 7923  grpidinv 7934  grpideu 7935  grpidinv2 7942  ringdi 8031  ringdir 8032  ringass 8033  vcid 8057  vcdi 8058  vcdir 8059  vcass 8060  nvs 8166  nvz 8173  nvtri 8174  ajmoi 8385  axgroth3 8631  grothinf 8633  imonclem 8933  projlem22 9337  adjmo 9889  adjvalvalt 9991  lnopcon 10092  lnfncon 10119  cnlnssadj 10142  stge0t 10275  stle1t 10276  mdbr3 10348  mdbr4 10349  mdsl1 10370  dmdbr6at 10470

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-gen 955

This theorem depends on definitions:  df-bi 147  df-ral 1625

Copyright terms: Public domain