Theorem eqsidd | index | src |

theorem eqsidd (G: wff) (A: set): $ G -> A == A $;
StepHypRefExpression
1 eqsid
A == A
2 1 a1i
G -> A == A

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp), axs_pred_calc (ax_gen)