Theorem r19.20si 1752

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 1750	1 ⊢ (∀x ∈ A φ → ∀x ∈ A ψ)

Syntax hints:   → wi 3   ∈ wcel 994  ∀wral 1691

This theorem is referenced by:  r19.20sii 1753  reu6 1978  uniss2 2596  iunss2 2663  tfis 3208  find 3243  dffun8 3645  fununi 3668  fun11uni 3670  zfrep6 3721  fnopabg 3722  elrnopabg 3914  dffo5 3935  fopab2 3937  elrnoprabg 4186  unifi2 4702  iunfi 4712  rankonid 4841  aceq5 4886  ac5b 4899  ac6lem 4900  ac6 4901  kmlem6 4916  kmlem8 4918  kmlem13 4923  xrsupexmnf 6242  xrinfmexpnf 6243  cau3iri 7118  cau3i 7119  cvganz 7127  2sumeq2dv 7197  fsum1s 7212  fsump1s 7216  fsumadd 7225  csbfsum 7230  fsummulc1 7236  fsumcmp 7243  fsumcmp0 7244  fsumcmpndx2 7245  fsumabs 7246  fsumabs2mul 7247  serzmulc1 7260  clm3i 7282  clmi2i 7290  clm0ii 7292  climunii 7301  2climnn 7305  2climnn0 7306  climge0 7315  climabs0i 7316  iserzmulc1 7339  climcmplem 7340  climsqueeze 7343  climsqueeze2 7344  iserzcmp 7345  caucvg3i 7370  iserzgt0 7415  explecnv 7438  basgen2 7851  bastop1 7854  neips 7937  cncnp 7988  meteq0 8022  mettri2 8023  mettri4 8024  lmcvg2 8144  caun0 8156  xplm 8186  iscms2 8205  isgrp 8254  grpidinv 8265  grpideu 8266  grprlidrid 8270  grpidinv2 8277  ringideu 8387  ringdi 8388  ringdir 8389  ringass 8390  vcid 8417  vcdi 8418  vcdir 8419  vcass 8420  nvs 8537  nvz 8544  nvtri 8545  ajmoi 8775  laspwcl 8930  lanfwcl 8931  axgroth3 9051  grothinf 9053  grothpw 9054  projlem22 9483  adjmo 10038  adjvalval 10141  lnopconi 10242  lnfnconi 10269  cnlnssadj 10292  stge0 10432  stle1 10433  mdbr3 10505  mdbr4 10506  mdsl1i 10529  dmdbr6ati 10632  dmdbr7ati 10633  ref3w 10772  labs1 10836  labs2 10838  opidon 10898  exidu1 10902  grpmnd 10933  rngmgmbs4 10945  uznzr 10967  imonclem 11268  iepiclem 11278  topbasfne 11560  neibastop1 11579  neibastop2lem2 11581  neibastop2lem3 11582  neibastop2 11584  fipreima 11848  frinfm 11850  sdclem1 11875  fsum00 11883  fsumlt 11884  fsumlt1 11894  sstotbnd 11992  heiborlem23 12033

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-4 1009  ax-5o 1011

This theorem depends on definitions:  df-bi 145  df-ral 1695

Copyright terms: Public domain