Theorem a4s 983

Description: Generalization of antecedent.

Hypothesis

Ref	Expression
a4s.1	⊢ (φ → ψ)

Assertion

Ref	Expression
a4s	⊢ (∀xφ → ψ)

Proof of Theorem a4s

Step	Hyp	Ref	Expression
1		ax-4 972	. 2 ⊢ (∀xφ → φ)
2		a4s.1	. 2 ⊢ (φ → ψ)
3	1, 2	syl 10	1 ⊢ (∀xφ → ψ)

Syntax hints:   → wi 3  ∀wal 953

This theorem is referenced by:  19.20i 991  19.2 1029  19.21t 1114  exintr 1116  ax10o 1138  cbv1 1161  equvini 1167  drsb1 1174  sbied 1194  ax11v2 1214  dfsb2 1224  sbequi 1227  drsb2 1229  sbn 1230  sbi1 1231  hbsb4 1247  hbsb4t 1248  sbidm 1253  sbco2 1254  sbcom 1257  sbcom2 1333  sbal1 1345  ax11eq 1362  ax11el 1363  ax11inda 1370  a12lem1 1375  mopick 1432  rgen2a 1697  ralcom2 1774  reu3 1928  sbcralt 1987  sbcrext 1988  sbcralgf 1989  sbcrexgf 1990  csbie2t 2030  csbnestg 2033  sbcnestg 2035  moabex 2762  mosubopt 2800  ssopab2 2818  dfid3 2832  alxfr 2892  dmcosseq 3361  fununi 3559  fv3 3728  cbvfo 3880  fnoprabg 4007  pssnn 4522  kmlem16 4763  axextnd 4926  axrepndlem1 4927  axrepndlem2 4928  axunndlem1 4930  axunnd 4931  axpowndlem1 4932  axpowndlem2 4933  axpowndlem3 4934  axpowndlem4 4935  axregndlem1 4937  axregndlem2 4938  axregnd 4939  axinfndlem1 4940  axinfnd 4941  axacndlem4 4945  axacndlem5 4946  axacnd 4947  suppsr3 5207  uninqs 10400  cmphmp 10467  qusp 10489  imonclem 10655

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7  ax-4 972

Copyright terms: Public domain