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

Theorem mpt2bi123f 32139
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 2593 . . . . . . 7  |-  F/ x  A  =  B
4 eleq2 2493 . . . . . . 7  |-  ( A  =  B  ->  (
x  e.  A  <->  x  e.  B ) )
53, 4alrimi 1927 . . . . . 6  |-  ( A  =  B  ->  A. x
( x  e.  A  <->  x  e.  B ) )
6 mpt2bi123f.3 . . . . . . . . . 10  |-  F/_ y A
76nfcri 2575 . . . . . . . . 9  |-  F/ y  x  e.  A
8 mpt2bi123f.4 . . . . . . . . . 10  |-  F/_ y B
98nfcri 2575 . . . . . . . . 9  |-  F/ y  x  e.  B
107, 9nfbi 1989 . . . . . . . 8  |-  F/ y ( x  e.  A  <->  x  e.  B )
11 ax-5 1748 . . . . . . . 8  |-  ( ( x  e.  A  <->  x  e.  B )  ->  A. z
( x  e.  A  <->  x  e.  B ) )
1210, 11alrimi 1927 . . . . . . 7  |-  ( ( x  e.  A  <->  x  e.  B )  ->  A. y A. z ( x  e.  A  <->  x  e.  B
) )
1312alimi 1680 . . . . . 6  |-  ( A. x ( x  e.  A  <->  x  e.  B
)  ->  A. x A. y A. z ( x  e.  A  <->  x  e.  B ) )
145, 13syl 17 . . . . 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 2593 . . . . . . 7  |-  F/ y  C  =  D
18 eleq2 2493 . . . . . . 7  |-  ( C  =  D  ->  (
y  e.  C  <->  y  e.  D ) )
1917, 18alrimi 1927 . . . . . 6  |-  ( C  =  D  ->  A. y
( y  e.  C  <->  y  e.  D ) )
20 ax-5 1748 . . . . . . 7  |-  ( ( y  e.  C  <->  y  e.  D )  ->  A. z
( y  e.  C  <->  y  e.  D ) )
2120alimi 1680 . . . . . 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 2575 . . . . . . . . . 10  |-  F/ x  y  e.  C
24 mpt2bi123f.8 . . . . . . . . . . 11  |-  F/_ x D
2524nfcri 2575 . . . . . . . . . 10  |-  F/ x  y  e.  D
2623, 25nfbi 1989 . . . . . . . . 9  |-  F/ x
( y  e.  C  <->  y  e.  D )
2726nfal 2002 . . . . . . . 8  |-  F/ x A. z ( y  e.  C  <->  y  e.  D
)
2827nfal 2002 . . . . . . 7  |-  F/ x A. y A. z ( y  e.  C  <->  y  e.  D )
2928nfri 1924 . . . . . 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 18 . . . . 5  |-  ( C  =  D  ->  A. x A. y A. z ( y  e.  C  <->  y  e.  D ) )
31 id 23 . . . . . . . 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 1684 . . . . . . 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 1684 . . . . . 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 1684 . . . . 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 479 . . . 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 2435 . . . . . . . 8  |-  ( E  =  F  ->  (
z  =  E  <->  z  =  F ) )
3736alrimiv 1763 . . . . . . 7  |-  ( E  =  F  ->  A. z
( z  =  E  <-> 
z  =  F ) )
3837ralimi 2816 . . . . . 6  |-  ( A. y  e.  C  E  =  F  ->  A. y  e.  C  A. z
( z  =  E  <-> 
z  =  F ) )
3938ralimi 2816 . . . . 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 2805 . . . . . . . . 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 2789 . . . . . . . . 9  |-  ( A. y  e.  C  A. z ( z  =  E  <->  z  =  F )  ->  ( y  e.  C  ->  A. z
( z  =  E  <-> 
z  =  F ) ) )
4240, 41alrimih 1689 . . . . . . . 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 1775 . . . . . . . . 9  |-  ( A. z ( y  e.  C  ->  ( z  =  E  <->  z  =  F ) )  <->  ( y  e.  C  ->  A. z
( z  =  E  <-> 
z  =  F ) ) )
4443albii 1687 . . . . . . . 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 215 . . . . . . 7  |-  ( A. y  e.  C  A. z ( z  =  E  <->  z  =  F )  ->  A. y A. z ( y  e.  C  ->  ( z  =  E  <->  z  =  F ) ) )
4645ralimi 2816 . . . . . 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 2805 . . . . . . 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 2789 . . . . . . 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 1689 . . . . . 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 1959 . . . . . . . . 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 1687 . . . . . . . 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 209 . . . . . . 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 1775 . . . . . . . 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 1688 . . . . . . 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 215 . . . . . 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 18 . . . . 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 17 . . . 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 23 . . . . . . 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 1684 . . . . . 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 1684 . . . . 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 1684 . . . 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 479 . . 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 32117 . . . . . . . . . . . . 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 378 . . . . . . . . . . . 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 32117 . . . . . . . . . . . . 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 26 . . . . . . . . . . . 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 32059 . . . . . . . . . . 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 32109 . . . . . . . . . . . . . . 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 378 . . . . . . . . . . . . . 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 47 . . . . . . . . . . . . 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 32066 . . . . . . . . . . . 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 26 . . . . . . . . . . 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 32059 . . . . . . . . . 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 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
) ) )  -> 
( -.  x  e.  A  ->  -.  x  e.  A ) )
76 tsan2 32117 . . . . . . . . . . . . . . . . . . 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 378 . . . . . . . . . . . . . . . . . 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 32117 . . . . . . . . . . . . . . . . . . 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 26 . . . . . . . . . . . . . . . . . 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 32059 . . . . . . . . . . . . . . . . 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 32106 . . . . . . . . . . . . . . . . . 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 26 . . . . . . . . . . . . . . . . 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 32059 . . . . . . . . . . . . . . . 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 32066 . . . . . . . . . . . . . . 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 26 . . . . . . . . . . . . . 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 32110 . . . . . . . . . . . . . . 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 26 . . . . . . . . . . . . . 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 32062 . . . . . . . . . . . . 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 32059 . . . . . . . . . . . 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 32117 . . . . . . . . . . . . 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 26 . . . . . . . . . . . 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 32059 . . . . . . . . . . 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 32117 . . . . . . . . . . . 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 26 . . . . . . . . . . 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 32059 . . . . . . . . . 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 32066 . . . . . . . . 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 26 . . . . . . . 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 26 . . . . . . . . . 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 32060 . . . . . . . . 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 32118 . . . . . . . . . 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 26 . . . . . . . . 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 32062 . . . . . . . 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 41 . . . . . . 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 115 . . . . . . . . . . . . . . . . . 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 26 . . . . . . . . . . . . . . . . 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 32062 . . . . . . . . . . . . . . . 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 32118 . . . . . . . . . . . . . . . . 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 26 . . . . . . . . . . . . . . . 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 32062 . . . . . . . . . . . . . . 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 32118 . . . . . . . . . . . . . . . . . . 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 378 . . . . . . . . . . . . . . . . . 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 26 . . . . . . . . . . . . . . . . . 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 32059 . . . . . . . . . . . . . . . . 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 26 . . . . . . . . . . . . . . . . 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 32059 . . . . . . . . . . . . . . . 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 32066 . . . . . . . . . . . . . . 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 237 . . . . . . . . . . . . . 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 26 . . . . . . . . . . . . . . 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 26 . . . . . . . . . . . . . . . . 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 32060 . . . . . . . . . . . . . . . 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 26 . . . . . . . . . . . . . . . 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 32062 . . . . . . . . . . . . . . 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 41 . . . . . . . . . . . . . 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 41 . . . . . . . . . . . . 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 535 . . . . . . . . . . . . . . 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 32107 . . . . . . . . . . . . . . . . . . . 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 26 . . . . . . . . . . . . . . . . . . 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 32060 . . . . . . . . . . . . . . . . . 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 32108 . . . . . . . . . . . . . . . . . . 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 26 . . . . . . . . . . . . . . . . . 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 32060 . . . . . . . . . . . . . . . . 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 32062 . . . . . . . . . . . . . . . 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 32116 . . . . . . . . . . . . . . . . 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 26 . . . . . . . . . . . . . . . 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 32060 . . . . . . . . . . . . . . 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 32061 . . . . . . . . . . . . . 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 32118 . . . . . . . . . . . . . . . . 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 26 . . . . . . . . . . . . . . . 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 32062 . . . . . . . . . . . . . . 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 32110 . . . . . . . . . . . . . . . . 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 26 . . . . . . . . . . . . . . . 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 32063 . . . . . . . . . . . . . . 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 32062 . . . . . . . . . . . . . 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 32059 . . . . . . . . . . . . 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 32066 . . . . . . . . . . . 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 26 . . . . . . . . . . 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 26 . . . . . . . . . . . . 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 32060 . . . . . . . . . . . 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 26 . . . . . . . . . . . 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 32060 . . . . . . . . . . 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 32060 . . . . . . . . . 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 26 . . . . . . . . . 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 32062 . . . . . . . . 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 32118 . . . . . . . . . 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 26 . . . . . . . . 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 32062 . . . . . . . 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 32118 . . . . . . . . . . . 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 26 . . . . . . . . . . 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 32062 . . . . . . . . . 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 217 . . . . . . . . . . . . 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 217 . . . . . . . . . . . . 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 535 . . . . . . . . . . . 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 32116 . . . . . . . . . . . . . 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 26 . . . . . . . . . . . . 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 32060 . . . . . . . . . . . 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 32061 . . . . . . . . . . 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 32111 . . . . . . . . . . . . 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 26 . . . . . . . . . . . 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 32063 . . . . . . . . . . 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 32060