Theorem r19.20si 1703

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

Syntax hints:   -> wi 3   e. wcel 956  A.wral 1642

This theorem is referenced by:  r19.20sii 1704  reu6 1928  uniss2 2524  iunss2 2590  tfis 3122  find 3150  dffun7 3532  fununi 3555  fun11uni 3557  zfrep6 3606  fnopabg 3607  elrnopabg 3791  dffo5 3812  fopab2 3814  elrnoprabg 4114  unifi2 4539  iunfi 4549  rankonid 4675  aceq5 4720  ac5b 4733  ac6lem 4734  ac6 4735  kmlem6 4750  kmlem8 4752  kmlem13 4757  xrsupexmnf 6029  xrinfmexpnf 6030  cau3ir 6860  cau3 6861  cvganz 6869  2sumeq2dv 6940  fsum1s 6955  fsump1s 6959  fsumadd 6968  csbfsum 6973  fsummulc1 6979  fsumcmp 6986  fsumcmp0 6987  fsumcmpndx2 6988  fsumabs 6989  fsumabs2mul 6990  serzmulc1 7003  clm3 7025  clmi2 7033  clm0i 7035  climunii 7043  2climnn 7047  2climnn0 7048  climge0 7057  iserzmulc1 7080  climcmplem 7081  climsqueeze 7084  climsqueeze2 7085  iserzcmp 7086  caucvg3 7111  iserzgt0 7154  basgen2t 7589  bastop 7592  neips 7677  cncnp 7728  meteq0 7762  mettri2 7763  mettri4 7764  lmcvg2 7885  caun0 7896  xplm 7925  iscms2 7944  isgrp 7991  grpidinv 8002  grpideu 8003  grpidinv2 8010  ringdi 8098  ringdir 8099  ringass 8100  vcid 8122  vcdi 8123  vcdir 8124  vcass 8125  nvs 8242  nvz 8249  nvtri 8250  ajmoi 8463  axgroth3 8718  grothinf 8720  projlem22 9146  adjmo 9698  adjvalvalt 9800  lnopcon 9901  lnfncon 9928  cnlnssadj 9951  stge0t 10089  stle1t 10090  mdbr3 10162  mdbr4 10163  mdsl1 10185  dmdbr6at 10285  imonclem 10619

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-4 971  ax-5o 973

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

Copyright terms: Public domain