Theorem ax12bOLD 1690

Description: Obsolete version of ax12b 1689 as of 12-Aug-2017. (Contributed by NM, 2-May-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
ax12bOLD	|- ((-. x = y -> (y = z -> A.x y = z)) <-> (-. x = y -> (-. x = z -> (y = z -> A.x y = z))))

Proof of Theorem ax12bOLD

Step	Hyp	Ref	Expression
1		bi2.04 350	. . . 4 |- ((-. x = y -> (y = z -> A.x y = z)) <-> (y = z -> (-. x = y -> A.x y = z)))
2		equtrr 1683	. . . . . . . . 9 |- (z = y -> (x = z -> x = y))
3	2	equcoms 1681	. . . . . . . 8 |- (y = z -> (x = z -> x = y))
4	3	con3d 125	. . . . . . 7 |- (y = z -> (-. x = y -> -. x = z))
5	4	pm4.71d 615	. . . . . 6 |- (y = z -> (-. x = y <-> (-. x = y /\ -. x = z)))
6	5	imbi1d 308	. . . . 5 |- (y = z -> ((-. x = y -> A.x y = z) <-> ((-. x = y /\ -. x = z) -> A.x y = z)))
7	6	pm5.74i 236	. . . 4 |- ((y = z -> (-. x = y -> A.x y = z)) <-> (y = z -> ((-. x = y /\ -. x = z) -> A.x y = z)))
8	1, 7	bitri 240	. . 3 |- ((-. x = y -> (y = z -> A.x y = z)) <-> (y = z -> ((-. x = y /\ -. x = z) -> A.x y = z)))
9		bi2.04 350	. . 3 |- ((y = z -> ((-. x = y /\ -. x = z) -> A.x y = z)) <-> ((-. x = y /\ -. x = z) -> (y = z -> A.x y = z)))
10	8, 9	bitri 240	. 2 |- ((-. x = y -> (y = z -> A.x y = z)) <-> ((-. x = y /\ -. x = z) -> (y = z -> A.x y = z)))
11		impexp 433	. 2 |- (((-. x = y /\ -. x = z) -> (y = z -> A.x y = z)) <-> (-. x = y -> (-. x = z -> (y = z -> A.x y = z))))
12	10, 11	bitri 240	1 |- ((-. x = y -> (y = z -> A.x y = z)) <-> (-. x = y -> (-. x = z -> (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

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

This theorem is referenced by: (None)