Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  spv GIF version

Theorem spv 1832
 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
StepHypRef Expression
1 spv.1 . . 3 (𝑥 = 𝑦 → (𝜑𝜓))
21biimpd 143 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
32spimv 1783 1 (∀𝑥𝜑𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104  ∀wal 1329 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514 This theorem depends on definitions:  df-bi 116  df-nf 1437 This theorem is referenced by:  spvv  1879  chvarv  1909  ru  2908  nalset  4058  tfisi  4501  tfr1onlemsucfn  6237  tfr1onlemsucaccv  6238  tfr1onlembxssdm  6240  tfr1onlembfn  6241  tfr1onlemres  6246  tfri1dALT  6248  tfrcllemsucfn  6250  tfrcllemsucaccv  6251  tfrcllembxssdm  6253  tfrcllembfn  6254  tfrcllemres  6259  findcard2  6783  findcard2s  6784  bj-nalset  13152
 Copyright terms: Public domain W3C validator