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

Theorem cbvexv 1777
Description: Rule used to change bound variables, using implicit substitition. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
cbvalv.1 (x = y → (φψ))
Assertion
Ref Expression
cbvexv (xφyψ)
Distinct variable groups:   φ,y   ψ,x
Allowed substitution hints:   φ(x)   ψ(y)

Proof of Theorem cbvexv
StepHypRef Expression
1 ax-17 1400 . 2 (φyφ)
2 ax-17 1400 . 2 (ψxψ)
3 cbvalv.1 . 2 (x = y → (φψ))
41, 2, 3cbvexh 1620 1 (xφyψ)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98  wex 1362
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-4 1381  ax-17 1400  ax-i9 1404  ax-ial 1409
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  eujust  1884  euind  2705  reuind  2721  r19.3rm  3289  r19.9rmv  3291  raaanlem  3305  raaan  3306  cbvopab2v  3808  bm1.3ii  3852  mss  3936  zfun  4121  xpiindim  4400  relop  4413  dmmrnm  4481  dmxpm  4482  dmcoss  4528  xpm  4672  cnviinm  4786  fv3  5122  fo1stresm  5711  fo2ndresm  5712  iinerm  6089  riinerm  6090  ltexprlemdisj  6443  ltexprlemloc  6444  recexprlemdisj  6464  bdbm1.3ii  7117
  Copyright terms: Public domain W3C validator