Theorem oreq1 ≪ | index | src | ≫

theorem oreq1 (_a1 _a2 b: wff): $ (_a1 <-> _a2) -> (_a1 \/ b <-> _a2 \/ b) $;

(_a1 <-> _a2) -> (_a1 <-> _a2)

(_a1 <-> _a2) -> (_a1 \/ b <-> _a2 \/ b)

Axiom use