theorem eqmeqm23d (G: wff) (a b c d n: nat):
$ G -> mod(n): a = b $ >
$ G -> mod(n): c = d $ >
$ G -> (mod(n): a = c <-> mod(n): b = d) $;
Step | Hyp | Ref | Expression |
1 |
|
eqmtr |
mod(n): b = a -> mod(n): a = d -> mod(n): b = d |
2 |
|
eqmcom |
mod(n): a = b -> mod(n): b = a |
3 |
|
hyp h1 |
G -> mod(n): a = b |
4 |
3 |
anwl |
G /\ mod(n): a = c -> mod(n): a = b |
5 |
2, 4 |
syl |
G /\ mod(n): a = c -> mod(n): b = a |
6 |
|
eqmtr |
mod(n): a = c -> mod(n): c = d -> mod(n): a = d |
7 |
|
anr |
G /\ mod(n): a = c -> mod(n): a = c |
8 |
|
hyp h2 |
G -> mod(n): c = d |
9 |
8 |
anwl |
G /\ mod(n): a = c -> mod(n): c = d |
10 |
6, 7, 9 |
sylc |
G /\ mod(n): a = c -> mod(n): a = d |
11 |
1, 5, 10 |
sylc |
G /\ mod(n): a = c -> mod(n): b = d |
12 |
|
eqmtr |
mod(n): a = b -> mod(n): b = c -> mod(n): a = c |
13 |
3 |
anwl |
G /\ mod(n): b = d -> mod(n): a = b |
14 |
|
eqmtr |
mod(n): b = d -> mod(n): d = c -> mod(n): b = c |
15 |
|
anr |
G /\ mod(n): b = d -> mod(n): b = d |
16 |
|
eqmcom |
mod(n): c = d -> mod(n): d = c |
17 |
8 |
anwl |
G /\ mod(n): b = d -> mod(n): c = d |
18 |
16, 17 |
syl |
G /\ mod(n): b = d -> mod(n): d = c |
19 |
14, 15, 18 |
sylc |
G /\ mod(n): b = d -> mod(n): b = c |
20 |
12, 13, 19 |
sylc |
G /\ mod(n): b = d -> mod(n): a = c |
21 |
11, 20 |
ibida |
G -> (mod(n): a = c <-> mod(n): b = d) |
Axiom use
axs_prop_calc
(ax_1,
ax_2,
ax_3,
ax_mp),
axs_pred_calc
(ax_gen,
ax_4,
ax_5,
ax_6,
ax_7)