Theorem Ifeq2a ≪ | index | src | ≫ 

theorem Ifeq2a (A B C: set) (p: wff): $ (p -> A == B) -> If p A C == If p B C $;
StepHypRefExpression
1 Ifeq2 
A == B -> If p A C == If p B C
2 1 imim2i 
(p -> A == B) -> p -> If p A C == If p B C
3 Ifneg 
~p -> If p A C == C
4 Ifneg 
~p -> If p B C == C
5 3, 4 eqstr4d 
~p -> If p A C == If p B C
6 5 a1i 
(p -> A == B) -> ~p -> If p A C == If p B C
7 2, 6 casesd 
(p -> A == B) -> If p A C == If p B C

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8)