Theorem 19.20i 968

Description: Inference quantifying both antecedent and consequent.

Hypothesis

Ref	Expression
19.20i.1	⊢ (φ → ψ)

Assertion

Ref	Expression
19.20i	⊢ (∀xφ → ∀xψ)

Proof of Theorem 19.20i

Step	Hyp	Ref	Expression
1		19.20i.1	. . 3 ⊢ (φ → ψ)
2	1	a4s 960	. 2 ⊢ (∀xφ → ψ)
3	2	a5i 965	1 ⊢ (∀xφ → ∀xψ)

Syntax hints:   → wi 3  ∀wal 950

This theorem is referenced by:  19.20i2 969  19.20 970  19.20ii 971  19.21ai 974  hbal 981  ax67 994  ax67to6 995  ax67to7 996  ax467 997  ax467to6 999  ax467to7 1000  19.9d 1013  19.18 1026  19.26 1043  19.25 1060  19.33 1067  19.33b 1068  hbimd 1086  19.21t 1091  equid 1113  alequcom 1125  a4a 1142  stdpc4 1168  sbied 1178  aev 1192  ax11 1203  hbsb4 1232  sbco3 1241  sbcom 1242  sb9i 1247  sbal1 1328  sbal2 1338  ax11eq 1340  ax11el 1341  ax11indi 1344  a12stdy3 1351  a12study 1355  mo 1370  eumo0 1372  mo2 1377  2mo 1424  bm1.1 1439  alral 1668  rgen2a 1675  r19.20i2 1679  r19.27av 1730  ceqsalg 1800  elabgt 1867  reu3 1902  sbciegft 1930  csbexg 1979  csbiegft 2000  csbnestg 2007  sbcnestg 2009  rabss2 2100  unss1 2170  ssrin 2205  undif4 2296  ralf0 2330  intmin4 2527  iinss 2568  axrep1 2662  axrep2 2663  bm1.3ii 2674  axnul 2677  axpr 2746  ssrel 3209  funin 3506  zfrep6 3554  fv3 3672  tfrlem5 3854  dfom3 4554  aceq5 4664  aceq6a 4665  aceq6b 4666  kmlem1 4689  kmlem13 4701  zorn 4721  brdom3 4725  brdom4 4727  axpowndlem2 4873  axacndlem1 4882  axacndlem2 4883  axacndlem3 4884  axacndlem4 4885  axacnd 4887  suppsr2 5146  suppsr3 5147  pre-axsup 5214  peano2nn 5834  islp2 7636  chsscm 9263  chcmh 9264  pjnormss 10221

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

Copyright terms: Public domain