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

Theorem spv 1785
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 142 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
32spimv 1736 1 (∀𝑥𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103  wal 1285
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470
This theorem depends on definitions:  df-bi 115  df-nf 1393
This theorem is referenced by:  chvarv  1857  ru  2828  nalset  3946  tfisi  4377  tfr1onlemsucfn  6061  tfr1onlemsucaccv  6062  tfr1onlembxssdm  6064  tfr1onlembfn  6065  tfr1onlemres  6070  tfri1dALT  6072  tfrcllemsucfn  6074  tfrcllemsucaccv  6075  tfrcllembxssdm  6077  tfrcllembfn  6078  tfrcllemres  6083  findcard2  6559  findcard2s  6560  bj-nalset  11255
  Copyright terms: Public domain W3C validator