Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  spv Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 spv.1 . . 3 (𝑥 = 𝑦 → (𝜑𝜓))
21biimpd 221 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
32spimv 2412 1 (∀𝑥𝜑𝜓)
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator