Users' Mathboxes Mathbox for Giovanni Mascellani < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mpt2bi123f Structured version   Unicode version

Theorem mpt2bi123f 28975
Description: Equality deduction for maps-to notations with two arguments. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
Hypotheses
Ref Expression
mpt2bi123f.1  |-  F/_ x A
mpt2bi123f.2  |-  F/_ x B
mpt2bi123f.3  |-  F/_ y A
mpt2bi123f.4  |-  F/_ y B
mpt2bi123f.5  |-  F/_ y C
mpt2bi123f.6  |-  F/_ y D
mpt2bi123f.7  |-  F/_ x C
mpt2bi123f.8  |-  F/_ x D
Assertion
Ref Expression
mpt2bi123f  |-  ( ( ( A  =  B  /\  C  =  D )  /\  A. x  e.  A  A. y  e.  C  E  =  F )  ->  (
x  e.  A , 
y  e.  C  |->  E )  =  ( x  e.  B ,  y  e.  D  |->  F ) )
Distinct variable group:    x, y
Allowed substitution hints:    A( x, y)    B( x, y)    C( x, y)    D( x, y)    E( x, y)    F( x, y)

Proof of Theorem mpt2bi123f
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 mpt2bi123f.1 . . . . . . . 8  |-  F/_ x A
2 mpt2bi123f.2 . . . . . . . 8  |-  F/_ x B
31, 2nfeq 2586 . . . . . . 7  |-  F/ x  A  =  B
4 eleq2 2504 . . . . . . 7  |-  ( A  =  B  ->  (
x  e.  A  <->  x  e.  B ) )
53, 4alrimi 1811 . . . . . 6  |-  ( A  =  B  ->  A. x
( x  e.  A  <->  x  e.  B ) )
6 mpt2bi123f.3 . . . . . . . . . 10  |-  F/_ y A
76nfcri 2573 . . . . . . . . 9  |-  F/ y  x  e.  A
8 mpt2bi123f.4 . . . . . . . . . 10  |-  F/_ y B
98nfcri 2573 . . . . . . . . 9  |-  F/ y  x  e.  B
107, 9nfbi 1867 . . . . . . . 8  |-  F/ y ( x  e.  A  <->  x  e.  B )
11 ax-5 1670 . . . . . . . 8  |-  ( ( x  e.  A  <->  x  e.  B )  ->  A. z
( x  e.  A  <->  x  e.  B ) )
1210, 11alrimi 1811 . . . . . . 7  |-  ( ( x  e.  A  <->  x  e.  B )  ->  A. y A. z ( x  e.  A  <->  x  e.  B
) )
1312alimi 1604 . . . . . 6  |-  ( A. x ( x  e.  A  <->  x  e.  B
)  ->  A. x A. y A. z ( x  e.  A  <->  x  e.  B ) )
145, 13syl 16 . . . . 5  |-  ( A  =  B  ->  A. x A. y A. z ( x  e.  A  <->  x  e.  B ) )
15 mpt2bi123f.5 . . . . . . . 8  |-  F/_ y C
16 mpt2bi123f.6 . . . . . . . 8  |-  F/_ y D
1715, 16nfeq 2586 . . . . . . 7  |-  F/ y  C  =  D
18 eleq2 2504 . . . . . . 7  |-  ( C  =  D  ->  (
y  e.  C  <->  y  e.  D ) )
1917, 18alrimi 1811 . . . . . 6  |-  ( C  =  D  ->  A. y
( y  e.  C  <->  y  e.  D ) )
20 ax-5 1670 . . . . . . 7  |-  ( ( y  e.  C  <->  y  e.  D )  ->  A. z
( y  e.  C  <->  y  e.  D ) )
2120alimi 1604 . . . . . 6  |-  ( A. y ( y  e.  C  <->  y  e.  D
)  ->  A. y A. z ( y  e.  C  <->  y  e.  D
) )
22 mpt2bi123f.7 . . . . . . . . . . 11  |-  F/_ x C
2322nfcri 2573 . . . . . . . . . 10  |-  F/ x  y  e.  C
24 mpt2bi123f.8 . . . . . . . . . . 11  |-  F/_ x D
2524nfcri 2573 . . . . . . . . . 10  |-  F/ x  y  e.  D
2623, 25nfbi 1867 . . . . . . . . 9  |-  F/ x
( y  e.  C  <->  y  e.  D )
2726nfal 1873 . . . . . . . 8  |-  F/ x A. z ( y  e.  C  <->  y  e.  D
)
2827nfal 1873 . . . . . . 7  |-  F/ x A. y A. z ( y  e.  C  <->  y  e.  D )
2928nfri 1808 . . . . . 6  |-  ( A. y A. z ( y  e.  C  <->  y  e.  D )  ->  A. x A. y A. z ( y  e.  C  <->  y  e.  D ) )
3019, 21, 293syl 20 . . . . 5  |-  ( C  =  D  ->  A. x A. y A. z ( y  e.  C  <->  y  e.  D ) )
31 id 22 . . . . . . . 8  |-  ( ( ( x  e.  A  <->  x  e.  B )  /\  ( y  e.  C  <->  y  e.  D ) )  ->  ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) ) )
3231alanimi 1607 . . . . . . 7  |-  ( ( A. z ( x  e.  A  <->  x  e.  B )  /\  A. z ( y  e.  C  <->  y  e.  D
) )  ->  A. z
( ( x  e.  A  <->  x  e.  B
)  /\  ( y  e.  C  <->  y  e.  D
) ) )
3332alanimi 1607 . . . . . 6  |-  ( ( A. y A. z
( x  e.  A  <->  x  e.  B )  /\  A. y A. z ( y  e.  C  <->  y  e.  D ) )  ->  A. y A. z ( ( x  e.  A  <->  x  e.  B )  /\  ( y  e.  C  <->  y  e.  D ) ) )
3433alanimi 1607 . . . . 5  |-  ( ( A. x A. y A. z ( x  e.  A  <->  x  e.  B
)  /\  A. x A. y A. z ( y  e.  C  <->  y  e.  D ) )  ->  A. x A. y A. z ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) ) )
3514, 30, 34syl2an 477 . . . 4  |-  ( ( A  =  B  /\  C  =  D )  ->  A. x A. y A. z ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) ) )
36 eqeq2 2452 . . . . . . . 8  |-  ( E  =  F  ->  (
z  =  E  <->  z  =  F ) )
3736alrimiv 1685 . . . . . . 7  |-  ( E  =  F  ->  A. z
( z  =  E  <-> 
z  =  F ) )
3837ralimi 2791 . . . . . 6  |-  ( A. y  e.  C  E  =  F  ->  A. y  e.  C  A. z
( z  =  E  <-> 
z  =  F ) )
3938ralimi 2791 . . . . 5  |-  ( A. x  e.  A  A. y  e.  C  E  =  F  ->  A. x  e.  A  A. y  e.  C  A. z
( z  =  E  <-> 
z  =  F ) )
40 hbra1 2765 . . . . . . . . 9  |-  ( A. y  e.  C  A. z ( z  =  E  <->  z  =  F )  ->  A. y A. y  e.  C  A. z ( z  =  E  <->  z  =  F ) )
41 rsp 2776 . . . . . . . . 9  |-  ( A. y  e.  C  A. z ( z  =  E  <->  z  =  F )  ->  ( y  e.  C  ->  A. z
( z  =  E  <-> 
z  =  F ) ) )
4240, 41alrimih 1612 . . . . . . . 8  |-  ( A. y  e.  C  A. z ( z  =  E  <->  z  =  F )  ->  A. y
( y  e.  C  ->  A. z ( z  =  E  <->  z  =  F ) ) )
43 19.21v 1909 . . . . . . . . 9  |-  ( A. z ( y  e.  C  ->  ( z  =  E  <->  z  =  F ) )  <->  ( y  e.  C  ->  A. z
( z  =  E  <-> 
z  =  F ) ) )
4443albii 1610 . . . . . . . 8  |-  ( A. y A. z ( y  e.  C  ->  (
z  =  E  <->  z  =  F ) )  <->  A. y
( y  e.  C  ->  A. z ( z  =  E  <->  z  =  F ) ) )
4542, 44sylibr 212 . . . . . . 7  |-  ( A. y  e.  C  A. z ( z  =  E  <->  z  =  F )  ->  A. y A. z ( y  e.  C  ->  ( z  =  E  <->  z  =  F ) ) )
4645ralimi 2791 . . . . . 6  |-  ( A. x  e.  A  A. y  e.  C  A. z ( z  =  E  <->  z  =  F )  ->  A. x  e.  A  A. y A. z ( y  e.  C  ->  ( z  =  E  <->  z  =  F ) ) )
47 hbra1 2765 . . . . . . 7  |-  ( A. x  e.  A  A. y A. z ( y  e.  C  ->  (
z  =  E  <->  z  =  F ) )  ->  A. x A. x  e.  A  A. y A. z ( y  e.  C  ->  ( z  =  E  <->  z  =  F ) ) )
48 rsp 2776 . . . . . . 7  |-  ( A. x  e.  A  A. y A. z ( y  e.  C  ->  (
z  =  E  <->  z  =  F ) )  -> 
( x  e.  A  ->  A. y A. z
( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )
4947, 48alrimih 1612 . . . . . 6  |-  ( A. x  e.  A  A. y A. z ( y  e.  C  ->  (
z  =  E  <->  z  =  F ) )  ->  A. x ( x  e.  A  ->  A. y A. z ( y  e.  C  ->  ( z  =  E  <->  z  =  F ) ) ) )
50719.21 1839 . . . . . . . . 9  |-  ( A. y ( x  e.  A  ->  A. z
( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) )  <->  ( x  e.  A  ->  A. y A. z ( y  e.  C  ->  ( z  =  E  <->  z  =  F ) ) ) )
5150albii 1610 . . . . . . . 8  |-  ( A. x A. y ( x  e.  A  ->  A. z
( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) )  <->  A. x
( x  e.  A  ->  A. y A. z
( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )
5251biimpri 206 . . . . . . 7  |-  ( A. x ( x  e.  A  ->  A. y A. z ( y  e.  C  ->  ( z  =  E  <->  z  =  F ) ) )  ->  A. x A. y ( x  e.  A  ->  A. z ( y  e.  C  ->  ( z  =  E  <->  z  =  F ) ) ) )
53 19.21v 1909 . . . . . . . 8  |-  ( A. z ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <->  z  =  F ) ) )  <-> 
( x  e.  A  ->  A. z ( y  e.  C  ->  (
z  =  E  <->  z  =  F ) ) ) )
54532albii 1611 . . . . . . 7  |-  ( A. x A. y A. z
( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) )  <->  A. x A. y ( x  e.  A  ->  A. z
( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )
5552, 54sylibr 212 . . . . . 6  |-  ( A. x ( x  e.  A  ->  A. y A. z ( y  e.  C  ->  ( z  =  E  <->  z  =  F ) ) )  ->  A. x A. y A. z ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <->  z  =  F ) ) ) )
5646, 49, 553syl 20 . . . . 5  |-  ( A. x  e.  A  A. y  e.  C  A. z ( z  =  E  <->  z  =  F )  ->  A. x A. y A. z ( x  e.  A  -> 
( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )
5739, 56syl 16 . . . 4  |-  ( A. x  e.  A  A. y  e.  C  E  =  F  ->  A. x A. y A. z ( x  e.  A  -> 
( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )
58 id 22 . . . . . . 7  |-  ( ( ( ( x  e.  A  <->  x  e.  B
)  /\  ( y  e.  C  <->  y  e.  D
) )  /\  (
x  e.  A  -> 
( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) ) )
5958alanimi 1607 . . . . . 6  |-  ( ( A. z ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  A. z ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <->  z  =  F ) ) ) )  ->  A. z
( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) ) )
6059alanimi 1607 . . . . 5  |-  ( ( A. y A. z
( ( x  e.  A  <->  x  e.  B
)  /\  ( y  e.  C  <->  y  e.  D
) )  /\  A. y A. z ( x  e.  A  ->  (
y  e.  C  -> 
( z  =  E  <-> 
z  =  F ) ) ) )  ->  A. y A. z ( ( ( x  e.  A  <->  x  e.  B
)  /\  ( y  e.  C  <->  y  e.  D
) )  /\  (
x  e.  A  -> 
( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) ) )
6160alanimi 1607 . . . 4  |-  ( ( A. x A. y A. z ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  A. x A. y A. z ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <->  z  =  F ) ) ) )  ->  A. x A. y A. z ( ( ( x  e.  A  <->  x  e.  B
)  /\  ( y  e.  C  <->  y  e.  D
) )  /\  (
x  e.  A  -> 
( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) ) )
6235, 57, 61syl2an 477 . . 3  |-  ( ( ( A  =  B  /\  C  =  D )  /\  A. x  e.  A  A. y  e.  C  E  =  F )  ->  A. x A. y A. z ( ( ( x  e.  A  <->  x  e.  B
)  /\  ( y  e.  C  <->  y  e.  D
) )  /\  (
x  e.  A  -> 
( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) ) )
63 tsan2 28953 . . . . . . . . . . . . 13  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( x  e.  A  \/  -.  ( x  e.  A  /\  y  e.  C ) ) )
6463ord 377 . . . . . . . . . . . 12  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  x  e.  A  ->  -.  (
x  e.  A  /\  y  e.  C )
) )
65 tsan2 28953 . . . . . . . . . . . . 13  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( ( x  e.  A  /\  y  e.  C )  \/  -.  ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E ) ) )
6665a1d 25 . . . . . . . . . . . 12  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  x  e.  A  ->  ( (
x  e.  A  /\  y  e.  C )  \/  -.  ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E ) ) ) )
6764, 66cnf1dd 28893 . . . . . . . . . . 11  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  x  e.  A  ->  -.  (
( x  e.  A  /\  y  e.  C
)  /\  z  =  E ) ) )
68 tsbi2 28945 . . . . . . . . . . . . . . 15  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( ( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E
)  \/  ( ( x  e.  B  /\  y  e.  D )  /\  z  =  F
) )  \/  (
( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) ) )
6968ord 377 . . . . . . . . . . . . . 14  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  ( ( ( x  e.  A  /\  y  e.  C
)  /\  z  =  E )  \/  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) ) )
7069a1dd 46 . . . . . . . . . . . . 13  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  ( ( ( x  e.  A  /\  y  e.  C
)  /\  z  =  E )  \/  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F ) )  -> 
( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) ) ) )
71 ax-1 6 . . . . . . . . . . . . 13  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  ( ( ( x  e.  A  /\  y  e.  C
)  /\  z  =  E )  \/  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F ) )  ->  -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) ) ) )
7270, 71contrd 28900 . . . . . . . . . . . 12  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  \/  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F ) ) )
7372a1d 25 . . . . . . . . . . 11  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  x  e.  A  ->  ( (
( x  e.  A  /\  y  e.  C
)  /\  z  =  E )  \/  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F ) ) ) )
7467, 73cnf1dd 28893 . . . . . . . . . 10  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  x  e.  A  ->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )
75 idd 24 . . . . . . . . . . . . 13  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  x  e.  A  ->  -.  x  e.  A ) )
76 tsan2 28953 . . . . . . . . . . . . . . . . . . 19  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( ( x  e.  A  <->  x  e.  B
)  \/  -.  (
( x  e.  A  <->  x  e.  B )  /\  ( y  e.  C  <->  y  e.  D ) ) ) )
7776ord 377 . . . . . . . . . . . . . . . . . 18  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  ( x  e.  A  <->  x  e.  B )  ->  -.  ( ( x  e.  A  <->  x  e.  B
)  /\  ( y  e.  C  <->  y  e.  D
) ) ) )
78 tsan2 28953 . . . . . . . . . . . . . . . . . . 19  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  \/ 
-.  ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) ) ) )
7978a1d 25 . . . . . . . . . . . . . . . . . 18  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  ( x  e.  A  <->  x  e.  B )  ->  (
( ( x  e.  A  <->  x  e.  B
)  /\  ( y  e.  C  <->  y  e.  D
) )  \/  -.  ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) ) ) ) )
8077, 79cnf1dd 28893 . . . . . . . . . . . . . . . . 17  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  ( x  e.  A  <->  x  e.  B )  ->  -.  ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) ) ) )
81 tsim2 28942 . . . . . . . . . . . . . . . . . 18  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  \/  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) ) ) )
8281a1d 25 . . . . . . . . . . . . . . . . 17  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  ( x  e.  A  <->  x  e.  B )  ->  (
( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  \/  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) ) ) ) )
8380, 82cnf1dd 28893 . . . . . . . . . . . . . . . 16  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  ( x  e.  A  <->  x  e.  B )  ->  (
( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) ) ) )
84 ax-1 6 . . . . . . . . . . . . . . . 16  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  ( x  e.  A  <->  x  e.  B )  ->  -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) ) ) )
8583, 84contrd 28900 . . . . . . . . . . . . . . 15  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( x  e.  A  <->  x  e.  B ) )
8685a1d 25 . . . . . . . . . . . . . 14  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  x  e.  A  ->  ( x  e.  A  <->  x  e.  B
) ) )
87 tsbi3 28946 . . . . . . . . . . . . . . 15  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( ( x  e.  A  \/  -.  x  e.  B )  \/  -.  ( x  e.  A  <->  x  e.  B ) ) )
8887a1d 25 . . . . . . . . . . . . . 14  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  x  e.  A  ->  ( (
x  e.  A  \/  -.  x  e.  B
)  \/  -.  (
x  e.  A  <->  x  e.  B ) ) ) )
8986, 88cnfn2dd 28896 . . . . . . . . . . . . 13  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  x  e.  A  ->  ( x  e.  A  \/  -.  x  e.  B )
) )
9075, 89cnf1dd 28893 . . . . . . . . . . . 12  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  x  e.  A  ->  -.  x  e.  B ) )
91 tsan2 28953 . . . . . . . . . . . . 13  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( x  e.  B  \/  -.  ( x  e.  B  /\  y  e.  D ) ) )
9291a1d 25 . . . . . . . . . . . 12  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  x  e.  A  ->  ( x  e.  B  \/  -.  ( x  e.  B  /\  y  e.  D
) ) ) )
9390, 92cnf1dd 28893 . . . . . . . . . . 11  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  x  e.  A  ->  -.  (
x  e.  B  /\  y  e.  D )
) )
94 tsan2 28953 . . . . . . . . . . . 12  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( ( x  e.  B  /\  y  e.  D )  \/  -.  ( ( x  e.  B  /\  y  e.  D )  /\  z  =  F ) ) )
9594a1d 25 . . . . . . . . . . 11  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  x  e.  A  ->  ( (
x  e.  B  /\  y  e.  D )  \/  -.  ( ( x  e.  B  /\  y  e.  D )  /\  z  =  F ) ) ) )
9693, 95cnf1dd 28893 . . . . . . . . . 10  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  x  e.  A  ->  -.  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F ) ) )
9774, 96contrd 28900 . . . . . . . . 9  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  ->  x  e.  A )
9897a1d 25 . . . . . . . 8  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -. F.  ->  x  e.  A ) )
99 ax-1 6 . . . . . . . . . 10  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -. F.  ->  -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) ) ) )
10081a1d 25 . . . . . . . . . 10  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -. F.  ->  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  \/  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) ) ) ) )
10199, 100cnf2dd 28894 . . . . . . . . 9  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -. F.  ->  ( ( ( x  e.  A  <->  x  e.  B
)  /\  ( y  e.  C  <->  y  e.  D
) )  /\  (
x  e.  A  -> 
( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) ) ) )
102 tsan3 28954 . . . . . . . . . 10  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <->  z  =  F ) ) )  \/  -.  ( ( ( x  e.  A  <->  x  e.  B )  /\  ( y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <->  z  =  F ) ) ) ) ) )
103102a1d 25 . . . . . . . . 9  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -. F.  ->  ( ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) )  \/  -.  ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) ) ) ) )
104101, 103cnfn2dd 28896 . . . . . . . 8  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -. F.  ->  ( x  e.  A  -> 
( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) ) )
10598, 104mpdd 40 . . . . . . 7  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -. F.  ->  ( y  e.  C  -> 
( z  =  E  <-> 
z  =  F ) ) ) )
106 notnot2 112 . . . . . . . . . . . . . . . . . 18  |-  ( -. 
-.  ( ( x  e.  B  /\  y  e.  D )  /\  z  =  F )  ->  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F ) )
107106a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  -.  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F )  ->  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F ) ) )
10894a1d 25 . . . . . . . . . . . . . . . . 17  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  -.  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F )  ->  (
( x  e.  B  /\  y  e.  D
)  \/  -.  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F ) ) ) )
109107, 108cnfn2dd 28896 . . . . . . . . . . . . . . . 16  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  -.  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F )  ->  (
x  e.  B  /\  y  e.  D )
) )
110 tsan3 28954 . . . . . . . . . . . . . . . . 17  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( y  e.  D  \/  -.  ( x  e.  B  /\  y  e.  D ) ) )
111110a1d 25 . . . . . . . . . . . . . . . 16  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  -.  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F )  ->  (
y  e.  D  \/  -.  ( x  e.  B  /\  y  e.  D
) ) ) )
112109, 111cnfn2dd 28896 . . . . . . . . . . . . . . 15  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  -.  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F )  ->  y  e.  D ) )
113 tsan3 28954 . . . . . . . . . . . . . . . . . . 19  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( ( y  e.  C  <->  y  e.  D
)  \/  -.  (
( x  e.  A  <->  x  e.  B )  /\  ( y  e.  C  <->  y  e.  D ) ) ) )
114113ord 377 . . . . . . . . . . . . . . . . . 18  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  ( y  e.  C  <->  y  e.  D )  ->  -.  ( ( x  e.  A  <->  x  e.  B
)  /\  ( y  e.  C  <->  y  e.  D
) ) ) )
11578a1d 25 . . . . . . . . . . . . . . . . . 18  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  ( y  e.  C  <->  y  e.  D )  ->  (
( ( x  e.  A  <->  x  e.  B
)  /\  ( y  e.  C  <->  y  e.  D
) )  \/  -.  ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) ) ) ) )
116114, 115cnf1dd 28893 . . . . . . . . . . . . . . . . 17  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  ( y  e.  C  <->  y  e.  D )  ->  -.  ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) ) ) )
11781a1d 25 . . . . . . . . . . . . . . . . 17  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  ( y  e.  C  <->  y  e.  D )  ->  (
( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  \/  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) ) ) ) )
118116, 117cnf1dd 28893 . . . . . . . . . . . . . . . 16  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  ( y  e.  C  <->  y  e.  D )  ->  (
( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) ) ) )
119 ax-1 6 . . . . . . . . . . . . . . . 16  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  ( y  e.  C  <->  y  e.  D )  ->  -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) ) ) )
120118, 119contrd 28900 . . . . . . . . . . . . . . 15  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( y  e.  C  <->  y  e.  D ) )
121112, 120sylibrd 234 . . . . . . . . . . . . . 14  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  -.  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F )  ->  y  e.  C ) )
12297a1d 25 . . . . . . . . . . . . . . 15  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  -.  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F )  ->  x  e.  A ) )
123 ax-1 6 . . . . . . . . . . . . . . . . 17  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  -.  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F )  ->  -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) ) ) )
12481a1d 25 . . . . . . . . . . . . . . . . 17  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  -.  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F )  ->  (
( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  \/  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) ) ) ) )
125123, 124cnf2dd 28894 . . . . . . . . . . . . . . . 16  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  -.  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F )  ->  (
( ( x  e.  A  <->  x  e.  B
)  /\  ( y  e.  C  <->  y  e.  D
) )  /\  (
x  e.  A  -> 
( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) ) ) )
126102a1d 25 . . . . . . . . . . . . . . . 16  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  -.  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F )  ->  (
( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) )  \/  -.  ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) ) ) ) )
127125, 126cnfn2dd 28896 . . . . . . . . . . . . . . 15  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  -.  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F )  ->  (
x  e.  A  -> 
( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) ) )
128122, 127mpdd 40 . . . . . . . . . . . . . 14  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  -.  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F )  ->  (
y  e.  C  -> 
( z  =  E  <-> 
z  =  F ) ) ) )
129121, 128mpdd 40 . . . . . . . . . . . . 13  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  -.  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F )  ->  (
z  =  E  <->  z  =  F ) ) )
130122, 121jcad 533 . . . . . . . . . . . . . . 15  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  -.  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F )  ->  (
x  e.  A  /\  y  e.  C )
) )
131 tsim3 28943 . . . . . . . . . . . . . . . . . . . 20  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  ( ( ( x  e.  A  /\  y  e.  C
)  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) )  \/  (
( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) ) ) )
132131a1d 25 . . . . . . . . . . . . . . . . . . 19  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  -.  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F )  ->  ( -.  ( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) )  \/  (
( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) ) ) ) )
133123, 132cnf2dd 28894 . . . . . . . . . . . . . . . . . 18  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  -.  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F )  ->  -.  ( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) ) )
134 tsbi1 28944 . . . . . . . . . . . . . . . . . . 19  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( ( -.  (
( x  e.  A  /\  y  e.  C
)  /\  z  =  E )  \/  -.  ( ( x  e.  B  /\  y  e.  D )  /\  z  =  F ) )  \/  ( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) ) )
135134a1d 25 . . . . . . . . . . . . . . . . . 18  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  -.  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F )  ->  (
( -.  ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E
)  \/  -.  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F ) )  \/  ( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) ) ) )
136133, 135cnf2dd 28894 . . . . . . . . . . . . . . . . 17  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  -.  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F )  ->  ( -.  ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  \/  -.  ( ( x  e.  B  /\  y  e.  D )  /\  z  =  F ) ) ) )
137107, 136cnfn2dd 28896 . . . . . . . . . . . . . . . 16  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  -.  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F )  ->  -.  ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E ) ) )
138 tsan1 28952 . . . . . . . . . . . . . . . . 17  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( ( -.  (
x  e.  A  /\  y  e.  C )  \/  -.  z  =  E )  \/  ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E
) ) )
139138a1d 25 . . . . . . . . . . . . . . . 16  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  -.  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F )  ->  (
( -.  ( x  e.  A  /\  y  e.  C )  \/  -.  z  =  E )  \/  ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E ) ) ) )
140137, 139cnf2dd 28894 . . . . . . . . . . . . . . 15  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  -.  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F )  ->  ( -.  ( x  e.  A  /\  y  e.  C
)  \/  -.  z  =  E ) ) )
141130, 140cnfn1dd 28895 . . . . . . . . . . . . . 14  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  -.  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F )  ->  -.  z  =  E )
)
142 tsan3 28954 . . . . . . . . . . . . . . . . 17  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( z  =  F  \/  -.  ( ( x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )
143142a1d 25 . . . . . . . . . . . . . . . 16  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  -.  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F )  ->  (
z  =  F  \/  -.  ( ( x  e.  B  /\  y  e.  D )  /\  z  =  F ) ) ) )
144107, 143cnfn2dd 28896 . . . . . . . . . . . . . . 15  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  -.  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F )  ->  z  =  F ) )
145 tsbi3 28946 . . . . . . . . . . . . . . . . 17  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( ( z  =  E  \/  -.  z  =  F )  \/  -.  ( z  =  E  <-> 
z  =  F ) ) )
146145a1d 25 . . . . . . . . . . . . . . . 16  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  -.  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F )  ->  (
( z  =  E  \/  -.  z  =  F )  \/  -.  ( z  =  E  <-> 
z  =  F ) ) ) )
147146or32dd 28897 . . . . . . . . . . . . . . 15  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  -.  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F )  ->  (
( z  =  E  \/  -.  ( z  =  E  <->  z  =  F ) )  \/ 
-.  z  =  F ) ) )
148144, 147cnfn2dd 28896 . . . . . . . . . . . . . 14  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  -.  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F )  ->  (
z  =  E  \/  -.  ( z  =  E  <-> 
z  =  F ) ) ) )
149141, 148cnf1dd 28893 . . . . . . . . . . . . 13  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -.  -.  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F )  ->  -.  ( z  =  E  <-> 
z  =  F ) ) )
150129, 149contrd 28900 . . . . . . . . . . . 12  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  ->  -.  ( ( x  e.  B  /\  y  e.  D )  /\  z  =  F ) )
151150a1d 25 . . . . . . . . . . 11  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -. F.  ->  -.  ( ( x  e.  B  /\  y  e.  D )  /\  z  =  F ) ) )
152131a1d 25 . . . . . . . . . . . . 13  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -. F.  ->  ( -.  ( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E
)  <->  ( ( x  e.  B  /\  y  e.  D )  /\  z  =  F ) )  \/  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) ) ) ) )
15399, 152cnf2dd 28894 . . . . . . . . . . . 12  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -. F.  ->  -.  ( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) ) )
15468a1d 25 . . . . . . . . . . . 12  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -. F.  ->  ( ( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  \/  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F ) )  \/  ( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) ) ) )
155153, 154cnf2dd 28894 . . . . . . . . . . 11  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -. F.  ->  ( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  \/  (
( x  e.  B  /\  y  e.  D
)  /\  z  =  F ) ) ) )
156151, 155cnf2dd 28894 . . . . . . . . . 10  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -. F.  ->  ( ( x  e.  A  /\  y  e.  C
)  /\  z  =  E ) ) )
15765a1d 25 . . . . . . . . . 10  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -. F.  ->  ( ( x  e.  A  /\  y  e.  C
)  \/  -.  (
( x  e.  A  /\  y  e.  C
)  /\  z  =  E ) ) ) )
158156, 157cnfn2dd 28896 . . . . . . . . 9  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -. F.  ->  ( x  e.  A  /\  y  e.  C )
) )
159 tsan3 28954 . . . . . . . . . 10  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( y  e.  C  \/  -.  ( x  e.  A  /\  y  e.  C ) ) )
160159a1d 25 . . . . . . . . 9  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -. F.  ->  ( y  e.  C  \/  -.  ( x  e.  A  /\  y  e.  C
) ) ) )
161158, 160cnfn2dd 28896 . . . . . . . 8  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -. F.  ->  y  e.  C ) )
162 tsan3 28954 . . . . . . . . . . . 12  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( z  =  E  \/  -.  ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E
) ) )
163162a1d 25 . . . . . . . . . . 11  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -. F.  ->  ( z  =  E  \/  -.  ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E ) ) ) )
164156, 163cnfn2dd 28896 . . . . . . . . . 10  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -. F.  ->  z  =  E ) )
16598, 85sylibd 214 . . . . . . . . . . . . 13  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -. F.  ->  x  e.  B ) )
166161, 120sylibd 214 . . . . . . . . . . . . 13  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -. F.  ->  y  e.  D ) )
167165, 166jcad 533 . . . . . . . . . . . 12  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -. F.  ->  ( x  e.  B  /\  y  e.  D )
) )
168 tsan1 28952 . . . . . . . . . . . . . 14  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( ( -.  (
x  e.  B  /\  y  e.  D )  \/  -.  z  =  F )  \/  ( ( x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )
169168a1d 25 . . . . . . . . . . . . 13  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -. F.  ->  ( ( -.  ( x  e.  B  /\  y  e.  D )  \/  -.  z  =  F )  \/  ( ( x  e.  B  /\  y  e.  D )  /\  z  =  F ) ) ) )
170151, 169cnf2dd 28894 . . . . . . . . . . . 12  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -. F.  ->  ( -.  ( x  e.  B  /\  y  e.  D )  \/  -.  z  =  F )
) )
171167, 170cnfn1dd 28895 . . . . . . . . . . 11  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -. F.  ->  -.  z  =  F ) )
172 tsbi4 28947 . . . . . . . . . . . . 13  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( ( -.  z  =  E  \/  z  =  F )  \/  -.  ( z  =  E  <-> 
z  =  F ) ) )
173172a1d 25 . . . . . . . . . . . 12  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -. F.  ->  ( ( -.  z  =  E  \/  z  =  F )  \/  -.  ( z  =  E  <-> 
z  =  F ) ) ) )
174173or32dd 28897 . . . . . . . . . . 11  |-  ( -.  ( ( ( ( x  e.  A  <->  x  e.  B )  /\  (
y  e.  C  <->  y  e.  D ) )  /\  ( x  e.  A  ->  ( y  e.  C  ->  ( z  =  E  <-> 
z  =  F ) ) ) )  -> 
( ( ( x  e.  A  /\  y  e.  C )  /\  z  =  E )  <->  ( (
x  e.  B  /\  y  e.  D )  /\  z  =  F
) ) )  -> 
( -. F.  ->  ( ( -.  z  =  E  \/  -.  (
z  =  E  <->  z  =  F ) )  \/  z  =  F ) ) )
175171, 174cnf2dd 28894 . . . . . . . . . 10  |-  ( -.