Theorem eqstr3g ≪ | index | src | ≫

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

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

Axiom use

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