Theorem eqstr4g ≪ | index | src | ≫

theorem eqstr4g (A B C D: set) (G: wff):
  $ C == A $ >
  $ D == B $ >
  $ G -> A == B $ >
  $ G -> C == D $;

Step	Hyp	Ref	Expression
1		hyp h1	C == A
2		hyp h2	D == B
3		hyp h	G -> A == B
4	2, 3	syl6eqsr	G -> A == D
5	1, 4	syl5eqs	G -> C == D

Axiom use

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