Theorem spv 1789

Description: Specialization, using implicit substitition. (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 143	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓))
3	2	spimv 1740	1 ⊢ (∀𝑥𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 104  ∀wal 1288

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473

This theorem depends on definitions:  df-bi 116  df-nf 1396

This theorem is referenced by:  chvarv  1861  ru  2840  nalset  3975  tfisi  4415  tfr1onlemsucfn  6119  tfr1onlemsucaccv  6120  tfr1onlembxssdm  6122  tfr1onlembfn  6123  tfr1onlemres  6128  tfri1dALT  6130  tfrcllemsucfn  6132  tfrcllemsucaccv  6133  tfrcllembxssdm  6135  tfrcllembfn  6136  tfrcllemres  6141  findcard2  6659  findcard2s  6660  bj-nalset  12059