Theorem r19.20si 1704

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

Hypothesis

Ref	Expression
r19.20si.1	⊢ (φ → ψ)

Assertion

Ref	Expression
r19.20si	⊢ (∀x ∈ A φ → ∀x ∈ A ψ)

Proof of Theorem r19.20si

Step	Hyp	Ref	Expression
1		r19.20si.1	. . 3 ⊢ (φ → ψ)
2	1	a1i 8	. 2 ⊢ (x ∈ A → (φ → ψ))
3	2	r19.20i 1702	1 ⊢ (∀x ∈ A φ → ∀x ∈ A ψ)

Syntax hints:   → wi 3   ∈ wcel 957  ∀wral 1643

This theorem is referenced by:  r19.20sii 1705  reu6 1929  uniss2 2525  iunss2 2591  tfis 3123  find 3151  dffun7 3536  fununi 3559  fun11uni 3561  zfrep6 3610  fnopabg 3611  elrnopabg 3795  dffo5 3816  fopab2 3818  elrnoprabg 4117  unifi2 4542  iunfi 4552  rankonid 4678  aceq5 4723  ac5b 4736  ac6lem 4737  ac6 4738  kmlem6 4753  kmlem8 4755  kmlem13 4760  xrsupexmnf 6031  xrinfmexpnf 6032  cau3ir 6867  cau3 6868  cvganz 6876  2sumeq2dv 6947  fsum1s 6962  fsump1s 6966  fsumadd 6975  csbfsum 6980  fsummulc1 6986  fsumcmp 6993  fsumcmp0 6994  fsumcmpndx2 6995  fsumabs 6996  fsumabs2mul 6997  serzmulc1 7010  clm3 7032  clmi2 7040  clm0i 7042  climunii 7051  2climnn 7055  2climnn0 7056  climge0 7065  climabs0OLD 7066  iserzmulc1 7089  climcmplem 7090  climsqueeze 7093  climsqueeze2 7094  iserzcmp 7095  caucvg3 7120  iserzgt0 7163  basgen2t 7599  bastop 7602  neips 7687  cncnp 7738  meteq0 7772  mettri2 7773  mettri4 7774  lmcvg2 7895  caun0 7907  xplm 7937  iscms2 7956  isgrp 8003  grpidinv 8014  grpideu 8015  grpidinv2 8022  ringdi 8110  ringdir 8111  ringass 8112  vcid 8134  vcdi 8135  vcdir 8136  vcass 8137  nvs 8254  nvz 8261  nvtri 8262  ajmoi 8478  axgroth3 8734  grothinf 8736  projlem22 9162  adjmo 9715  adjvalvalt 9818  lnopcon 9919  lnfncon 9946  cnlnssadj 9969  stge0t 10107  stle1t 10108  mdbr3 10180  mdbr4 10181  mdsl1 10204  dmdbr6at 10306  dmdbr7at 10307  imonclem 10655

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-4 972  ax-5o 974

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

Copyright terms: Public domain