Theorem spv 2415

Description: Specialization, using implicit substitution. (Contributed by NM, 30-Aug-1993.)

Hypothesis

Ref	Expression
spv.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
spv	⊢ (∀𝑥𝜑 → 𝜓)

Distinct variable group:   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝜓(𝑦)

Proof of Theorem spv

Step	Hyp	Ref	Expression
1		spv.1	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
2	1	biimpd 221	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
3	2	spimv 2412	1 ⊢ (∀𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 198  ∀wal 1656

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-12 2222  ax-13 2391

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1881  df-nf 1885

This theorem is referenced by:  cbvalv  2427  ru  3662  nalset  5021  isowe2  6856  tfisi  7320  findcard2  8470  marypha1lem  8609  setind  8888  karden  9036  kmlem4  9291  axgroth3  9969  ramcl  16105  alexsubALTlem3  22224  i1fd  23848  dfpo2  32188  dfon2lem6  32232  trer  32850  axc11n-16  35014  elsetrecslem  43341