Theorem spv 2296

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 219	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
3	2	spimv 2293	1 ⊢ (∀𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 196  ∀wal 1521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-12 2087  ax-13 2282

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745

This theorem is referenced by:  chvarv  2299  cbvalv  2309  ru  3467  nalset  4828  isowe2  6640  tfisi  7100  findcard2  8241  marypha1lem  8380  setind  8648  karden  8796  kmlem4  9013  axgroth3  9691  ramcl  15780  alexsubALTlem3  21900  i1fd  23493  dfpo2  31771  dfon2lem6  31817  trer  32435  axc11n-16  34542  elsetrecslem  42770