Theorem a4s 682

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 673	. 2 ⊢ (∀xφ → φ)
2		a4s.1	. 2 ⊢ (φ → ψ)
3	1, 2	syl 12	1 ⊢ (∀xφ → ψ)

Syntax hints:   → wi 2  ∀wal 672

This theorem is referenced by:  19.20 690  19.20i 691  19.2 713  19.21g 792  exintr 793  cbv1 845  eqvin.l1 851  del43 856  sb6y 872  hbsb3 875  sbequi 876  del44 878  del45 879  sbn1 880  sbi1 884  sbied 903  hbsb4 905  hbsb4t 906  sbidm 912  sbco2 913  sbcom 916  sbcom2 992  sbal1 996  mopick 1054  rgen2 1248  ralcom2 1314  moabex 1868  ssopab2 2119  dmcosseq 2572  fununi 2705  fv3 2839  cbvfo 2923  pssnn 3428  kmlem16 3595  axextnd 3737  axrepndlem1 3738  axrepndlem2 3739  axunndlem1 3741  axunnd 3742  axpowndlem1 3743  axpowndlem2 3744  axpowndlem3 3745  axpowndlem4 3746  axregndlem1 3748  axregndlem2 3749  axregnd 3750  axinfndlem1 3751  axinfnd 3752  axacndlem4 3756  axacndlem5 3757  axacnd 3758  suppsr3 4018

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-mp 6  ax-4 673

metamath.org