Theorem ifpeq3a ≪ | index | src | ≫ 

theorem ifpeq3a (a b1 b2 p: wff):
  $ (~p -> (b1 <-> b2)) -> (ifp p a b1 <-> ifp p a b2) $;
StepHypRefExpression
1 aneq2a 
(~p -> (b1 <-> b2)) -> (~p /\ b1 <-> ~p /\ b2)
2 1 oreq2d 
(~p -> (b1 <-> b2)) -> (p /\ a \/ ~p /\ b1 <-> p /\ a \/ ~p /\ b2)
3 2 conv ifp 
(~p -> (b1 <-> b2)) -> (ifp p a b1 <-> ifp p a b2)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)