Mathbox for Giovanni Mascellani < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mpobi123f Structured version   Visualization version   GIF version

Theorem mpobi123f 35593
 Description: Equality deduction for maps-to notations with two arguments. (Contributed by Giovanni Mascellani, 10-Apr-2018.)
Hypotheses
Ref Expression
mpobi123f.1 𝑥𝐴
mpobi123f.2 𝑥𝐵
mpobi123f.3 𝑦𝐴
mpobi123f.4 𝑦𝐵
mpobi123f.5 𝑦𝐶
mpobi123f.6 𝑦𝐷
mpobi123f.7 𝑥𝐶
mpobi123f.8 𝑥𝐷
Assertion
Ref Expression
mpobi123f (((𝐴 = 𝐵𝐶 = 𝐷) ∧ ∀𝑥𝐴𝑦𝐶 𝐸 = 𝐹) → (𝑥𝐴, 𝑦𝐶𝐸) = (𝑥𝐵, 𝑦𝐷𝐹))
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)   𝐷(𝑥,𝑦)   𝐸(𝑥,𝑦)   𝐹(𝑥,𝑦)

Proof of Theorem mpobi123f
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 mpobi123f.1 . . . . . . . 8 𝑥𝐴
2 mpobi123f.2 . . . . . . . 8 𝑥𝐵
31, 2nfeq 2971 . . . . . . 7 𝑥 𝐴 = 𝐵
4 eleq2 2881 . . . . . . 7 (𝐴 = 𝐵 → (𝑥𝐴𝑥𝐵))
53, 4alrimi 2212 . . . . . 6 (𝐴 = 𝐵 → ∀𝑥(𝑥𝐴𝑥𝐵))
6 mpobi123f.3 . . . . . . . . 9 𝑦𝐴
76nfcri 2946 . . . . . . . 8 𝑦 𝑥𝐴
8 mpobi123f.4 . . . . . . . . 9 𝑦𝐵
98nfcri 2946 . . . . . . . 8 𝑦 𝑥𝐵
107, 9nfbi 1904 . . . . . . 7 𝑦(𝑥𝐴𝑥𝐵)
11 ax-5 1911 . . . . . . 7 ((𝑥𝐴𝑥𝐵) → ∀𝑧(𝑥𝐴𝑥𝐵))
1210, 11alrimi 2212 . . . . . 6 ((𝑥𝐴𝑥𝐵) → ∀𝑦𝑧(𝑥𝐴𝑥𝐵))
135, 12sylg 1824 . . . . 5 (𝐴 = 𝐵 → ∀𝑥𝑦𝑧(𝑥𝐴𝑥𝐵))
14 mpobi123f.5 . . . . . . . 8 𝑦𝐶
15 mpobi123f.6 . . . . . . . 8 𝑦𝐷
1614, 15nfeq 2971 . . . . . . 7 𝑦 𝐶 = 𝐷
17 eleq2 2881 . . . . . . 7 (𝐶 = 𝐷 → (𝑦𝐶𝑦𝐷))
1816, 17alrimi 2212 . . . . . 6 (𝐶 = 𝐷 → ∀𝑦(𝑦𝐶𝑦𝐷))
19 ax-5 1911 . . . . . . 7 ((𝑦𝐶𝑦𝐷) → ∀𝑧(𝑦𝐶𝑦𝐷))
2019alimi 1813 . . . . . 6 (∀𝑦(𝑦𝐶𝑦𝐷) → ∀𝑦𝑧(𝑦𝐶𝑦𝐷))
21 mpobi123f.7 . . . . . . . . . . 11 𝑥𝐶
2221nfcri 2946 . . . . . . . . . 10 𝑥 𝑦𝐶
23 mpobi123f.8 . . . . . . . . . . 11 𝑥𝐷
2423nfcri 2946 . . . . . . . . . 10 𝑥 𝑦𝐷
2522, 24nfbi 1904 . . . . . . . . 9 𝑥(𝑦𝐶𝑦𝐷)
2625nfal 2334 . . . . . . . 8 𝑥𝑧(𝑦𝐶𝑦𝐷)
2726nfal 2334 . . . . . . 7 𝑥𝑦𝑧(𝑦𝐶𝑦𝐷)
2827nf5ri 2194 . . . . . 6 (∀𝑦𝑧(𝑦𝐶𝑦𝐷) → ∀𝑥𝑦𝑧(𝑦𝐶𝑦𝐷))
2918, 20, 283syl 18 . . . . 5 (𝐶 = 𝐷 → ∀𝑥𝑦𝑧(𝑦𝐶𝑦𝐷))
30 id 22 . . . . . . . 8 (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) → ((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)))
3130alanimi 1818 . . . . . . 7 ((∀𝑧(𝑥𝐴𝑥𝐵) ∧ ∀𝑧(𝑦𝐶𝑦𝐷)) → ∀𝑧((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)))
3231alanimi 1818 . . . . . 6 ((∀𝑦𝑧(𝑥𝐴𝑥𝐵) ∧ ∀𝑦𝑧(𝑦𝐶𝑦𝐷)) → ∀𝑦𝑧((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)))
3332alanimi 1818 . . . . 5 ((∀𝑥𝑦𝑧(𝑥𝐴𝑥𝐵) ∧ ∀𝑥𝑦𝑧(𝑦𝐶𝑦𝐷)) → ∀𝑥𝑦𝑧((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)))
3413, 29, 33syl2an 598 . . . 4 ((𝐴 = 𝐵𝐶 = 𝐷) → ∀𝑥𝑦𝑧((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)))
35 eqeq2 2813 . . . . . . 7 (𝐸 = 𝐹 → (𝑧 = 𝐸𝑧 = 𝐹))
3635alrimiv 1928 . . . . . 6 (𝐸 = 𝐹 → ∀𝑧(𝑧 = 𝐸𝑧 = 𝐹))
37362ralimi 3132 . . . . 5 (∀𝑥𝐴𝑦𝐶 𝐸 = 𝐹 → ∀𝑥𝐴𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹))
38 hbra1 3187 . . . . . . . . 9 (∀𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹) → ∀𝑦𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹))
39 rsp 3173 . . . . . . . . 9 (∀𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹) → (𝑦𝐶 → ∀𝑧(𝑧 = 𝐸𝑧 = 𝐹)))
4038, 39alrimih 1825 . . . . . . . 8 (∀𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹) → ∀𝑦(𝑦𝐶 → ∀𝑧(𝑧 = 𝐸𝑧 = 𝐹)))
41 19.21v 1940 . . . . . . . . 9 (∀𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)) ↔ (𝑦𝐶 → ∀𝑧(𝑧 = 𝐸𝑧 = 𝐹)))
4241albii 1821 . . . . . . . 8 (∀𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)) ↔ ∀𝑦(𝑦𝐶 → ∀𝑧(𝑧 = 𝐸𝑧 = 𝐹)))
4340, 42sylibr 237 . . . . . . 7 (∀𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹) → ∀𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))
4443ralimi 3131 . . . . . 6 (∀𝑥𝐴𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹) → ∀𝑥𝐴𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))
45 hbra1 3187 . . . . . . 7 (∀𝑥𝐴𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)) → ∀𝑥𝑥𝐴𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))
46 rsp 3173 . . . . . . 7 (∀𝑥𝐴𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)) → (𝑥𝐴 → ∀𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
4745, 46alrimih 1825 . . . . . 6 (∀𝑥𝐴𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)) → ∀𝑥(𝑥𝐴 → ∀𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
48 19.21v 1940 . . . . . . . 8 (∀𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ↔ (𝑥𝐴 → ∀𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
49482albii 1822 . . . . . . 7 (∀𝑥𝑦𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ↔ ∀𝑥𝑦(𝑥𝐴 → ∀𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
50719.21 2206 . . . . . . . 8 (∀𝑦(𝑥𝐴 → ∀𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ↔ (𝑥𝐴 → ∀𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
5150albii 1821 . . . . . . 7 (∀𝑥𝑦(𝑥𝐴 → ∀𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ↔ ∀𝑥(𝑥𝐴 → ∀𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
5249, 51sylbbr 239 . . . . . 6 (∀𝑥(𝑥𝐴 → ∀𝑦𝑧(𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) → ∀𝑥𝑦𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
5344, 47, 523syl 18 . . . . 5 (∀𝑥𝐴𝑦𝐶𝑧(𝑧 = 𝐸𝑧 = 𝐹) → ∀𝑥𝑦𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
5437, 53syl 17 . . . 4 (∀𝑥𝐴𝑦𝐶 𝐸 = 𝐹 → ∀𝑥𝑦𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
55 id 22 . . . . . . 7 ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
5655alanimi 1818 . . . . . 6 ((∀𝑧((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ ∀𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → ∀𝑧(((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
5756alanimi 1818 . . . . 5 ((∀𝑦𝑧((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ ∀𝑦𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → ∀𝑦𝑧(((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
5857alanimi 1818 . . . 4 ((∀𝑥𝑦𝑧((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ ∀𝑥𝑦𝑧(𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → ∀𝑥𝑦𝑧(((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
5934, 54, 58syl2an 598 . . 3 (((𝐴 = 𝐵𝐶 = 𝐷) ∧ ∀𝑥𝐴𝑦𝐶 𝐸 = 𝐹) → ∀𝑥𝑦𝑧(((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
60 tsan2 35573 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑥𝐴 ∨ ¬ (𝑥𝐴𝑦𝐶)))
6160ord 861 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ¬ (𝑥𝐴𝑦𝐶)))
62 tsan2 35573 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥𝐴𝑦𝐶) ∨ ¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)))
6362a1d 25 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ((𝑥𝐴𝑦𝐶) ∨ ¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸))))
6461, 63cnf1dd 35521 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)))
65 tsbi2 35565 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) ∨ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
6665ord 861 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
6766a1dd 50 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
68 ax-1 6 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) → ¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
6967, 68contrd 35528 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
7069a1d 25 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
7164, 70cnf1dd 35521 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
72 idd 24 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ¬ 𝑥𝐴))
73 tsan2 35573 . . . . . . . . . . . . . . . . . . 19 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥𝐴𝑥𝐵) ∨ ¬ ((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷))))
7473ord 861 . . . . . . . . . . . . . . . . . 18 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥𝐴𝑥𝐵) → ¬ ((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷))))
75 tsan2 35573 . . . . . . . . . . . . . . . . . . 19 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∨ ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))))
7675a1d 25 . . . . . . . . . . . . . . . . . 18 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥𝐴𝑥𝐵) → (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∨ ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))))
7774, 76cnf1dd 35521 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥𝐴𝑥𝐵) → ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))))
78 tsim2 35562 . . . . . . . . . . . . . . . . . 18 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
7978a1d 25 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥𝐴𝑥𝐵) → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))))
8077, 79cnf1dd 35521 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥𝐴𝑥𝐵) → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
81 ax-1 6 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥𝐴𝑥𝐵) → ¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
8280, 81contrd 35528 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑥𝐴𝑥𝐵))
8382a1d 25 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → (𝑥𝐴𝑥𝐵)))
84 tsbi3 35566 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥𝐴 ∨ ¬ 𝑥𝐵) ∨ ¬ (𝑥𝐴𝑥𝐵)))
8584a1d 25 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ((𝑥𝐴 ∨ ¬ 𝑥𝐵) ∨ ¬ (𝑥𝐴𝑥𝐵))))
8683, 85cnfn2dd 35524 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → (𝑥𝐴 ∨ ¬ 𝑥𝐵)))
8772, 86cnf1dd 35521 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ¬ 𝑥𝐵))
88 tsan2 35573 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑥𝐵 ∨ ¬ (𝑥𝐵𝑦𝐷)))
8988a1d 25 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → (𝑥𝐵 ∨ ¬ (𝑥𝐵𝑦𝐷))))
9087, 89cnf1dd 35521 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ¬ (𝑥𝐵𝑦𝐷)))
91 tsan2 35573 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥𝐵𝑦𝐷) ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
9291a1d 25 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ((𝑥𝐵𝑦𝐷) ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
9390, 92cnf1dd 35521 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥𝐴 → ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
9471, 93contrd 35528 . . . . . . . . 9 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → 𝑥𝐴)
9594a1d 25 . . . . . . . 8 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑥𝐴))
96 ax-1 6 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
9778a1d 25 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))))
9896, 97cnf2dd 35522 . . . . . . . . 9 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))))
99 tsan3 35574 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ∨ ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))))
10099a1d 25 . . . . . . . . 9 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ∨ ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))))
10198, 100cnfn2dd 35524 . . . . . . . 8 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
10295, 101mpdd 43 . . . . . . 7 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
103 notnotr 132 . . . . . . . . . . . . . . . . . 18 (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))
104103a1i 11 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
10591a1d 25 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((𝑥𝐵𝑦𝐷) ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
106104, 105cnfn2dd 35524 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑥𝐵𝑦𝐷)))
107 tsan3 35574 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑦𝐷 ∨ ¬ (𝑥𝐵𝑦𝐷)))
108107a1d 25 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑦𝐷 ∨ ¬ (𝑥𝐵𝑦𝐷))))
109106, 108cnfn2dd 35524 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → 𝑦𝐷))
110 tsan3 35574 . . . . . . . . . . . . . . . . . . 19 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((𝑦𝐶𝑦𝐷) ∨ ¬ ((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷))))
111110ord 861 . . . . . . . . . . . . . . . . . 18 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦𝐶𝑦𝐷) → ¬ ((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷))))
11275a1d 25 . . . . . . . . . . . . . . . . . 18 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦𝐶𝑦𝐷) → (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∨ ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))))
113111, 112cnf1dd 35521 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦𝐶𝑦𝐷) → ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))))
11478a1d 25 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦𝐶𝑦𝐷) → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))))
115113, 114cnf1dd 35521 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦𝐶𝑦𝐷) → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
116 ax-1 6 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦𝐶𝑦𝐷) → ¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
117115, 116contrd 35528 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑦𝐶𝑦𝐷))
118109, 117sylibrd 262 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → 𝑦𝐶))
11994a1d 25 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → 𝑥𝐴))
120 ax-1 6 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
12178a1d 25 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))))
122120, 121cnf2dd 35522 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))))
12399a1d 25 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ∨ ¬ (((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))))
124122, 123cnfn2dd 35524 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
125119, 124mpdd 43 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
126118, 125mpdd 43 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑧 = 𝐸𝑧 = 𝐹)))
127119, 118jcad 516 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑥𝐴𝑦𝐶)))
128 tsim3 35563 . . . . . . . . . . . . . . . . . . . 20 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
129128a1d 25 . . . . . . . . . . . . . . . . . . 19 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))))
130120, 129cnf2dd 35522 . . . . . . . . . . . . . . . . . 18 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
131 tsbi1 35564 . . . . . . . . . . . . . . . . . . 19 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) ∨ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
132131a1d 25 . . . . . . . . . . . . . . . . . 18 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) ∨ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
133130, 132cnf2dd 35522 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
134104, 133cnfn2dd 35524 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)))
135 tsan1 35572 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((¬ (𝑥𝐴𝑦𝐶) ∨ ¬ 𝑧 = 𝐸) ∨ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)))
136135a1d 25 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((¬ (𝑥𝐴𝑦𝐶) ∨ ¬ 𝑧 = 𝐸) ∨ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸))))
137134, 136cnf2dd 35522 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (¬ (𝑥𝐴𝑦𝐶) ∨ ¬ 𝑧 = 𝐸)))
138127, 137cnfn1dd 35523 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ¬ 𝑧 = 𝐸))
139 tsan3 35574 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑧 = 𝐹 ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
140139a1d 25 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑧 = 𝐹 ∨ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
141104, 140cnfn2dd 35524 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → 𝑧 = 𝐹))
142 tsbi3 35566 . . . . . . . . . . . . . . . . 17 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((𝑧 = 𝐸 ∨ ¬ 𝑧 = 𝐹) ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹)))
143142a1d 25 . . . . . . . . . . . . . . . 16 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((𝑧 = 𝐸 ∨ ¬ 𝑧 = 𝐹) ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹))))
144143or32dd 35525 . . . . . . . . . . . . . . 15 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ((𝑧 = 𝐸 ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹)) ∨ ¬ 𝑧 = 𝐹)))
145141, 144cnfn2dd 35524 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → (𝑧 = 𝐸 ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹))))
146138, 145cnf1dd 35521 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹) → ¬ (𝑧 = 𝐸𝑧 = 𝐹)))
147126, 146contrd 35528 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))
148147a1d 25 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
149128a1d 25 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) ∨ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))))
15096, 149cnf2dd 35522 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
15165a1d 25 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) ∨ (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))))
152150, 151cnf2dd 35522 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
153148, 152cnf2dd 35522 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)))
15462a1d 25 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((𝑥𝐴𝑦𝐶) ∨ ¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸))))
155153, 154cnfn2dd 35524 . . . . . . . . 9 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑥𝐴𝑦𝐶)))
156 tsan3 35574 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑦𝐶 ∨ ¬ (𝑥𝐴𝑦𝐶)))
157156a1d 25 . . . . . . . . 9 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑦𝐶 ∨ ¬ (𝑥𝐴𝑦𝐶))))
158155, 157cnfn2dd 35524 . . . . . . . 8 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑦𝐶))
159 tsan3 35574 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (𝑧 = 𝐸 ∨ ¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)))
160159a1d 25 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑧 = 𝐸 ∨ ¬ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸))))
161153, 160cnfn2dd 35524 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑧 = 𝐸))
16295, 82sylibd 242 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑥𝐵))
163158, 117sylibd 242 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑦𝐷))
164162, 163jcad 516 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑥𝐵𝑦𝐷)))
165 tsan1 35572 . . . . . . . . . . . . . 14 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((¬ (𝑥𝐵𝑦𝐷) ∨ ¬ 𝑧 = 𝐹) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
166165a1d 25 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ (𝑥𝐵𝑦𝐷) ∨ ¬ 𝑧 = 𝐹) ∨ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))))
167148, 166cnf2dd 35522 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (¬ (𝑥𝐵𝑦𝐷) ∨ ¬ 𝑧 = 𝐹)))
168164, 167cnfn1dd 35523 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ 𝑧 = 𝐹))
169 tsbi4 35567 . . . . . . . . . . . . 13 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((¬ 𝑧 = 𝐸𝑧 = 𝐹) ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹)))
170169a1d 25 . . . . . . . . . . . 12 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ 𝑧 = 𝐸𝑧 = 𝐹) ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹))))
171170or32dd 35525 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ 𝑧 = 𝐸 ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹)) ∨ 𝑧 = 𝐹)))
172168, 171cnf2dd 35522 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (¬ 𝑧 = 𝐸 ∨ ¬ (𝑧 = 𝐸𝑧 = 𝐹))))
173161, 172cnfn1dd 35523 . . . . . . . . 9 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ (𝑧 = 𝐸𝑧 = 𝐹)))
174 tsim1 35561 . . . . . . . . . . 11 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ((¬ 𝑦𝐶 ∨ (𝑧 = 𝐸𝑧 = 𝐹)) ∨ ¬ (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
175174a1d 25 . . . . . . . . . 10 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ 𝑦𝐶 ∨ (𝑧 = 𝐸𝑧 = 𝐹)) ∨ ¬ (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
176175or32dd 35525 . . . . . . . . 9 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ 𝑦𝐶 ∨ ¬ (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))) ∨ (𝑧 = 𝐸𝑧 = 𝐹))))
177173, 176cnf2dd 35522 . . . . . . . 8 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (¬ 𝑦𝐶 ∨ ¬ (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))))
178158, 177cnfn1dd 35523 . . . . . . 7 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹))))
179102, 178contrd 35528 . . . . . 6 (¬ ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹))) → ⊥)
180179efald2 35509 . . . . 5 ((((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → (((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
181180alimi 1813 . . . 4 (∀𝑧(((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → ∀𝑧(((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
1821812alimi 1814 . . 3 (∀𝑥𝑦𝑧(((𝑥𝐴𝑥𝐵) ∧ (𝑦𝐶𝑦𝐷)) ∧ (𝑥𝐴 → (𝑦𝐶 → (𝑧 = 𝐸𝑧 = 𝐹)))) → ∀𝑥𝑦𝑧(((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)))
183 oprabbi 35592 . . 3 (∀𝑥𝑦𝑧(((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)})
18459, 182, 1833syl 18 . 2 (((𝐴 = 𝐵𝐶 = 𝐷) ∧ ∀𝑥𝐴𝑦𝐶 𝐸 = 𝐹) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)})
185 df-mpo 7144 . 2 (𝑥𝐴, 𝑦𝐶𝐸) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐴𝑦𝐶) ∧ 𝑧 = 𝐸)}
186 df-mpo 7144 . 2 (𝑥𝐵, 𝑦𝐷𝐹) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥𝐵𝑦𝐷) ∧ 𝑧 = 𝐹)}
187184, 185, 1863eqtr4g 2861 1 (((𝐴 = 𝐵𝐶 = 𝐷) ∧ ∀𝑥𝐴𝑦𝐶 𝐸 = 𝐹) → (𝑥𝐴, 𝑦𝐶𝐸) = (𝑥𝐵, 𝑦𝐷𝐹))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844  ∀wal 1536   = wceq 1538  ⊥wfal 1550   ∈ wcel 2112  Ⅎwnfc 2939  ∀wral 3109  {coprab 7140   ∈ cmpo 7141 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-13 2382  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pr 5298 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-v 3446  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-oprab 7143  df-mpo 7144 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator