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

Theorem cbvexv 1792
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 1416 . 2 (φyφ)
2 ax-17 1416 . 2 (ψxψ)
3 cbvalv.1 . 2 (x = y → (φψ))
41, 2, 3cbvexh 1635 1 (xφyψ)
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98  wex 1378
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 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  eujust  1899  euind  2722  reuind  2738  r19.3rm  3304  r19.9rmv  3307  raaanlem  3320  raaan  3321  cbvopab2v  3825  bm1.3ii  3869  mss  3953  zfun  4137  xpiindim  4416  relop  4429  dmmrnm  4497  dmxpm  4498  dmcoss  4544  xpm  4688  cnviinm  4802  fv3  5140  fo1stresm  5730  fo2ndresm  5731  iinerm  6114  riinerm  6115  ltexprlemdisj  6580  ltexprlemloc  6581  recexprlemdisj  6602  bdbm1.3ii  9346
  Copyright terms: Public domain W3C validator