Theorem spv 1860

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wal 1351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534

This theorem depends on definitions:  df-bi 117  df-nf 1461

This theorem is referenced by:  spvv  1907  cbvalvw  1919  chvarv  1937  ru  2962  nalset  4134  tfisi  4587  tfr1onlemsucfn  6341  tfr1onlemsucaccv  6342  tfr1onlembxssdm  6344  tfr1onlembfn  6345  tfr1onlemres  6350  tfri1dALT  6352  tfrcllemsucfn  6354  tfrcllemsucaccv  6355  tfrcllembxssdm  6357  tfrcllembfn  6358  tfrcllemres  6363  findcard2  6889  findcard2s  6890  bj-nalset  14650