Theorem sbet ≪ | index | src | ≫

theorem sbet {x: nat} (a: nat) (b: wff x) (c: wff):
  $ A. x (x = a -> (b <-> c)) -> ([a / x] b <-> c) $;

F/ x c

A. x (x = a -> (b <-> c)) -> ([a / x] b <-> c)

Axiom use