Theorem ax12olem3OLD 1979

Description: Obsolete proof of ax12oOLD 1984 as of 30-Jan-2018. Lemma for ax12oOLD 1984. Show the equivalence of an intermediate equivalent to ax12o 1976 with the conjunction of ax-12 1946 and a variant with negated equalities. (Contributed by NM, 24-Dec-2015.) (New usage is discouraged.) (Proof modification is discouraged.)

Assertion

Ref	Expression
ax12olem3OLD	|- ( ( -. 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 ax12olem3OLD

Step	Hyp	Ref	Expression
1		sp 1759	. . . . . 6 |- ( A. x -. y = z -> -. y = z )
2	1	con2i 114	. . . . 5 |- ( y = z -> -. A. x -. y = z )
3	2	imim1i 56	. . . 4 |- ( ( -. A. x -. y = z -> A. x y = z ) -> ( y = z -> A. x y = z ) )
4	3	imim2i 14	. . 3 |- ( ( -. x = y -> ( -. A. x -. y = z -> A. x y = z ) ) -> ( -. x = y -> ( y = z -> A. x y = z ) ) )
5		sp 1759	. . . . . 6 |- ( A. x y = z -> y = z )
6	5	imim2i 14	. . . . 5 |- ( ( -. A. x -. y = z -> A. x y = z ) -> ( -. A. x -. y = z -> y = z ) )
7	6	con1d 118	. . . 4 |- ( ( -. A. x -. y = z -> A. x y = z ) -> ( -. y = z -> A. x -. y = z ) )
8	7	imim2i 14	. . 3 |- ( ( -. x = y -> ( -. A. x -. y = z -> A. x y = z ) ) -> ( -. x = y -> ( -. y = z -> A. x -. y = z ) ) )
9	4, 8	jca 519	. 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 122	. . . . . 6 |- ( ( -. y = z -> A. x -. y = z ) -> ( -. A. x -. y = z -> y = z ) )
11	10	imim1d 71	. . . . 5 |- ( ( -. y = z -> A. x -. y = z ) -> ( ( y = z -> A. x y = z ) -> ( -. A. x -. y = z -> A. x y = z ) ) )
12	11	com12 29	. . . 4 |- ( ( y = z -> A. x y = z ) -> ( ( -. y = z -> A. x -. y = z ) -> ( -. A. x -. y = z -> A. x y = z ) ) )
13	12	imim3i 57	. . 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 419	. 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 181	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 177   /\ wa 359   A.wal 1546

This theorem is referenced by:  ax12olem4OLD  1980  ax12olem4wAUX7  29164  ax12olem4OLD7  29391

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757

This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548