Theorem ifeq1 ≪ | index | src | ≫

theorem ifeq1 (_p1 _p2: wff) (a b: nat):
  $ (_p1 <-> _p2) -> if _p1 a b = if _p2 a b $;

(_p1 <-> _p2) -> (_p1 <-> _p2)

(_p1 <-> _p2) -> if _p1 a b = if _p2 a b

Axiom use