Step 
Hyp 
Ref 
Expression 
1 

equvinv 
 ( y = z <> E. w ( w = y /\ w = z ) ) 
2 

ax13lem1 
 ( . x = y > ( w = y > A. x w = y ) ) 
3 
2

imp 
 ( ( . x = y /\ w = y ) > A. x w = y ) 
4 

ax13lem1 
 ( . x = z > ( w = z > A. x w = z ) ) 
5 
4

imp 
 ( ( . x = z /\ w = z ) > A. x w = z ) 
6 

ax7v1 
 ( w = y > ( w = z > y = z ) ) 
7 
6

imp 
 ( ( w = y /\ w = z ) > y = z ) 
8 
7

alanimi 
 ( ( A. x w = y /\ A. x w = z ) > A. x y = z ) 
9 
3 5 8

syl2an 
 ( ( ( . x = y /\ w = y ) /\ ( . x = z /\ w = z ) ) > A. x y = z ) 
10 
9

an4s 
 ( ( ( . x = y /\ . x = z ) /\ ( w = y /\ w = z ) ) > A. x y = z ) 
11 
10

ex 
 ( ( . x = y /\ . x = z ) > ( ( w = y /\ w = z ) > A. x y = z ) ) 
12 
11

exlimdv 
 ( ( . x = y /\ . x = z ) > ( E. w ( w = y /\ w = z ) > A. x y = z ) ) 
13 
1 12

syl5bi 
 ( ( . x = y /\ . x = z ) > ( y = z > A. x y = z ) ) 
14 
13

ex 
 ( . x = y > ( . x = z > ( y = z > A. x y = z ) ) ) 
15 

ax13b 
 ( ( . x = y > ( y = z > A. x y = z ) ) <> ( . x = y > ( . x = z > ( y = z > A. x y = z ) ) ) ) 
16 
14 15

mpbir 
 ( . x = y > ( y = z > A. x y = z ) ) 