Theorem ax12olem3 1929

Description: Lemma for ax12o 1934. Show the equivalence of an intermediate equivalent to ax12o 1934 with the conjunction of ax-12 1925 and a variant with negated equalities. (Contributed by NM, 24-Dec-2015.)

Assertion

Ref	Expression
ax12olem3	|- ((-. x = y -> (-. A.x -. y = z -> A.x y = z)) <-> ((-. x = y -> (y = z -> A.x y = z)) /\ (-. x = y -> (-. y = z -> A.x -. y = z))))

Proof of Theorem ax12olem3

Step	Hyp	Ref	Expression
1		sp 1747	. . . . . 6 |- (A.x -. y = z -> -. y = z)
2	1	con2i 112	. . . . 5 |- (y = z -> -. A.x -. y = z)
3	2	imim1i 54	. . . 4 |- ((-. A.x -. y = z -> A.x y = z) -> (y = z -> A.x y = z))
4	3	imim2i 13	. . 3 |- ((-. x = y -> (-. A.x -. y = z -> A.x y = z)) -> (-. x = y -> (y = z -> A.x y = z)))
5		sp 1747	. . . . . 6 |- (A.x y = z -> y = z)
6	5	imim2i 13	. . . . 5 |- ((-. A.x -. y = z -> A.x y = z) -> (-. A.x -. y = z -> y = z))
7	6	con1d 116	. . . 4 |- ((-. A.x -. y = z -> A.x y = z) -> (-. y = z -> A.x -. y = z))
8	7	imim2i 13	. . 3 |- ((-. x = y -> (-. A.x -. y = z -> A.x y = z)) -> (-. x = y -> (-. y = z -> A.x -. y = z)))
9	4, 8	jca 518	. 2 |- ((-. x = y -> (-. A.x -. y = z -> A.x y = z)) -> ((-. x = y -> (y = z -> A.x y = z)) /\ (-. x = y -> (-. y = z -> A.x -. y = z))))
10		con1 120	. . . . . 6 |- ((-. y = z -> A.x -. y = z) -> (-. A.x -. y = z -> y = z))
11	10	imim1d 69	. . . . 5 |- ((-. y = z -> A.x -. y = z) -> ((y = z -> A.x y = z) -> (-. A.x -. y = z -> A.x y = z)))
12	11	com12 27	. . . 4 |- ((y = z -> A.x y = z) -> ((-. y = z -> A.x -. y = z) -> (-. A.x -. y = z -> A.x y = z)))
13	12	imim3i 55	. . 3 |- ((-. x = y -> (y = z -> A.x y = z)) -> ((-. x = y -> (-. y = z -> A.x -. y = z)) -> (-. x = y -> (-. A.x -. y = z -> A.x y = z))))
14	13	imp 418	. 2 |- (((-. x = y -> (y = z -> A.x y = z)) /\ (-. x = y -> (-. y = z -> A.x -. y = z))) -> (-. x = y -> (-. A.x -. y = z -> A.x y = z)))
15	9, 14	impbii 180	1 |- ((-. x = y -> (-. A.x -. y = z -> A.x y = z)) <-> ((-. x = y -> (y = z -> A.x y = z)) /\ (-. x = y -> (-. y = z -> A.x -. y = z))))

Syntax hints:  -. wn 3   -> wi 4   <-> wb 176   /\ wa 358  A.wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542

This theorem is referenced by:  ax12olem4  1930