Theorem ifpeq2d | index | src |

theorem ifpeq2d (_G p _a1 _a2 b: wff):
  $ _G -> (_a1 <-> _a2) $ >
  $ _G -> (ifp p _a1 b <-> ifp p _a2 b) $;
StepHypRefExpression
1 biidd
_G -> (p <-> p)
2 hyp _h
_G -> (_a1 <-> _a2)
3 biidd
_G -> (b <-> b)
4 1, 2, 3 ifpeqd
_G -> (ifp p _a1 b <-> ifp p _a2 b)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)