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

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
StepHypRef Expression
1 spv.1 . . 3 (𝑥 = 𝑦 → (𝜑𝜓))
21biimpd 144 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
32spimv 1811 1 (∀𝑥𝜑𝜓)
Colors of variables: wff set class
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  2961  nalset  4133  tfisi  4586  tfr1onlemsucfn  6340  tfr1onlemsucaccv  6341  tfr1onlembxssdm  6343  tfr1onlembfn  6344  tfr1onlemres  6349  tfri1dALT  6351  tfrcllemsucfn  6353  tfrcllemsucaccv  6354  tfrcllembxssdm  6356  tfrcllembfn  6357  tfrcllemres  6362  findcard2  6888  findcard2s  6889  bj-nalset  14617
  Copyright terms: Public domain W3C validator