New Foundations Explorer < Previous   Wrap > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  elopprim GIF version

Theorem elopprim 5506
 Description: PLEASE PUT DESCRIPTION HERE.
Hypothesis
Ref Expression
elopprim.1 A V
Assertion
Ref Expression
elopprim (A B, C ↔ (a(a B → ¬ b ¬ ((b A → ¬ c(c a → ¬ d ¬ ((d b → ((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)))) → ¬ (((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k))) → d b)))) → ¬ (¬ c(c a → ¬ d ¬ ((d b → ((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)))) → ¬ (((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k))) → d b))) → b A))) → ¬ a(a C → ¬ x ¬ ((x A → (y(y a → ¬ z ¬ ((z x → ((¬ a1(a1 yb1c1 ¬ d1 ¬ ((d1 b1d1 = c1) → ¬ (d1 = c1d1 b1)) → (e1(e1 a1 → ¬ e1 b1) → ¬ f1 ¬ ((f1 z → (¬ f1 a1f1 b1)) → ¬ ((¬ f1 a1f1 b1) → f1 z))))) → ¬ g1(¬ (¬ h1(i1 ¬ ((i1 h1j1 ¬ ((j1 i1 → ¬ j1 = j1) → ¬ (¬ j1 = j1j1 i1))) → ¬ (j1 ¬ ((j1 i1 → ¬ j1 = j1) → ¬ (¬ j1 = j1j1 i1)) → i1 h1)) → ¬ h1 g1) → ¬ k1(k1 g1 → ¬ l1(m1 ¬ ((m1 l1 → ¬ n1(n1 k1o1p1 ¬ q1 ¬ ((q1 o1q1 = p1) → ¬ (q1 = p1q1 o1)) → (r1(r1 n1 → ¬ r1 o1) → ¬ s1 ¬ ((s1 m1 → (¬ s1 n1s1 o1)) → ¬ ((¬ s1 n1s1 o1) → s1 m1)))))) → ¬ (¬ n1(n1 k1o1p1 ¬ q1 ¬ ((q1 o1q1 = p1) → ¬ (q1 = p1q1 o1)) → (r1(r1 n1 → ¬ r1 o1) → ¬ s1 ¬ ((s1 m1 → (¬ s1 n1s1 o1)) → ¬ ((¬ s1 n1s1 o1) → s1 m1))))) → m1 l1)) → ¬ l1 g1))) → y g1)) → ¬ (z yg1(¬ (¬ h1(i1 ¬ ((i1 h1j1 ¬ ((j1 i1 → ¬ j1 = j1) → ¬ (¬ j1 = j1j1 i1))) → ¬ (j1 ¬ ((j1 i1 → ¬ j1 = j1) → ¬ (¬ j1 = j1j1 i1)) → i1 h1)) → ¬ h1 g1) → ¬ k1(k1 g1 → ¬ l1(m1 ¬ ((m1 l1 → ¬ n1(n1 k1o1p1 ¬ q1 ¬ ((q1 o1q1 = p1) → ¬ (q1 = p1q1 o1)) → (r1(r1 n1 → ¬ r1 o1) → ¬ s1 ¬ ((s1 m1 → (¬ s1 n1s1 o1)) → ¬ ((¬ s1 n1s1 o1) → s1 m1)))))) → ¬ (¬ n1(n1 k1o1p1 ¬ q1 ¬ ((q1 o1q1 = p1) → ¬ (q1 = p1q1 o1)) → (r1(r1 n1 → ¬ r1 o1) → ¬ s1 ¬ ((s1 m1 → (¬ s1 n1s1 o1)) → ¬ ((¬ s1 n1s1 o1) → s1 m1))))) → m1 l1)) → ¬ l1 g1))) → y g1)))) → ¬ (((¬ a1(a1 yb1c1 ¬ d1 ¬ ((d1 b1d1 = c1) → ¬ (d1 = c1d1 b1)) → (e1(e1 a1 → ¬ e1 b1) → ¬ f1 ¬ ((f1 z → (¬ f1 a1f1 b1)) → ¬ ((¬ f1 a1f1 b1) → f1 z))))) → ¬ g1(¬ (¬ h1(i1 ¬ ((i1 h1j1 ¬ ((j1 i1 → ¬ j1 = j1) → ¬ (¬ j1 = j1j1 i1))) → ¬ (j1 ¬ ((j1 i1 → ¬ j1 = j1) → ¬ (¬ j1 = j1j1 i1)) → i1 h1)) → ¬ h1 g1) → ¬ k1(k1 g1 → ¬ l1(m1 ¬ ((m1 l1 → ¬ n1(n1 k1o1p1 ¬ q1 ¬ ((q1 o1q1 = p1) → ¬ (q1 = p1q1 o1)) → (r1(r1 n1 → ¬ r1 o1) → ¬ s1 ¬ ((s1 m1 → (¬ s1 n1s1 o1)) → ¬ ((¬ s1 n1s1 o1) → s1 m1)))))) → ¬ (¬ n1(n1 k1o1p1 ¬ q1 ¬ ((q1 o1q1 = p1) → ¬ (q1 = p1q1 o1)) → (r1(r1 n1 → ¬ r1 o1) → ¬ s1 ¬ ((s1 m1 → (¬ s1 n1s1 o1)) → ¬ ((¬ s1 n1s1 o1) → s1 m1))))) → m1 l1)) → ¬ l1 g1))) → y g1)) → ¬ (z yg1(¬ (¬ h1(i1 ¬ ((i1 h1j1 ¬ ((j1 i1 → ¬ j1 = j1) → ¬ (¬ j1 = j1j1 i1))) → ¬ (j1 ¬ ((j1 i1 → ¬ j1 = j1) → ¬ (¬ j1 = j1j1 i1)) → i1 h1)) → ¬ h1 g1) → ¬ k1(k1 g1 → ¬ l1(m1 ¬ ((m1 l1 → ¬ n1(n1 k1o1p1 ¬ q1 ¬ ((q1 o1q1 = p1) → ¬ (q1 = p1q1 o1)) → (r1(r1 n1 → ¬ r1 o1) → ¬ s1 ¬ ((s1 m1 → (¬ s1 n1s1 o1)) → ¬ ((¬ s1 n1s1 o1) → s1 m1)))))) → ¬ (¬ n1(n1 k1o1p1 ¬ q1 ¬ ((q1 o1q1 = p1) → ¬ (q1 = p1q1 o1)) → (r1(r1 n1 → ¬ r1 o1) → ¬ s1 ¬ ((s1 m1 → (¬ s1 n1s1 o1)) → ¬ ((¬ s1 n1s1 o1) → s1 m1))))) → m1 l1)) → ¬ l1 g1))) → y g1))) → z x))) → t1 ¬ ((t1 xu1 ¬ ((u1 t1 → ¬ u1 = u1) → ¬ (¬ u1 = u1u1 t1))) → ¬ (u1 ¬ ((u1 t1 → ¬ u1 = u1) → ¬ (¬ u1 = u1u1 t1)) → t1 x)))) → ¬ ((y(y a → ¬ z ¬ ((z x → ((¬ a1(a1 yb1c1 ¬ d1 ¬ ((d1 b1d1 = c1) → ¬ (d1 = c1d1 b1)) → (e1(e1 a1 → ¬ e1 b1) → ¬ f1 ¬ ((f1 z → (¬ f1 a1f1 b1)) → ¬ ((¬ f1 a1f1 b1) → f1 z))))) → ¬ g1(¬ (¬ h1(i1 ¬ ((i1 h1j1 ¬ ((j1 i1 → ¬ j1 = j1) → ¬ (¬ j1 = j1j1 i1))) → ¬ (j1 ¬ ((j1 i1 → ¬ j1 = j1) → ¬ (¬ j1 = j1j1 i1)) → i1 h1)) → ¬ h1 g1) → ¬ k1(k1 g1 → ¬ l1(m1 ¬ ((m1 l1 → ¬ n1(n1 k1o1p1 ¬ q1 ¬ ((q1 o1q1 = p1) → ¬ (q1 = p1q1 o1)) → (r1(r1 n1 → ¬ r1 o1) → ¬ s1 ¬ ((s1 m1 → (¬ s1 n1s1 o1)) → ¬ ((¬ s1 n1s1 o1) → s1 m1)))))) → ¬ (¬ n1(n1 k1o1p1 ¬ q1 ¬ ((q1 o1q1 = p1) → ¬ (q1 = p1q1 o1)) → (r1(r1 n1 → ¬ r1 o1) → ¬ s1 ¬ ((s1 m1 → (¬ s1 n1s1 o1)) → ¬ ((¬ s1 n1s1 o1) → s1 m1))))) → m1 l1)) → ¬ l1 g1))) → y g1)) → ¬ (z yg1(¬ (¬ h1(i1 ¬ ((i1 h1j1 ¬ ((j1 i1 → ¬ j1 = j1) → ¬ (¬ j1 = j1j1 i1))) → ¬ (j1 ¬ ((j1 i1 → ¬ j1 = j1) → ¬ (¬ j1 = j1j1 i1)) → i1 h1)) → ¬ h1 g1) → ¬ k1(k1 g1 → ¬ l1(m1 ¬ ((m1 l1 → ¬ n1(n1 k1o1p1 ¬ q1 ¬ ((q1 o1q1 = p1) → ¬ (q1 = p1q1 o1)) → (r1(r1 n1 → ¬ r1 o1) → ¬ s1 ¬ ((s1 m1 → (¬ s1 n1s1 o1)) → ¬ ((¬ s1 n1s1 o1) → s1 m1)))))) → ¬ (¬ n1(n1 k1o1p1 ¬ q1 ¬ ((q1 o1q1 = p1) → ¬ (q1 = p1q1 o1)) → (r1(r1 n1 → ¬ r1 o1) → ¬ s1 ¬ ((s1 m1 → (¬ s1 n1s1 o1)) → ¬ ((¬ s1 n1s1 o1) → s1 m1))))) → m1 l1)) → ¬ l1 g1))) → y g1)))) → ¬ (((¬ a1(a1 yb1c1 ¬ d1 ¬ ((d1 b1d1 = c1) → ¬ (d1 = c1d1 b1)) → (e1(e1 a1 → ¬ e1 b1) → ¬ f1 ¬ ((f1 z → (¬ f1 a1f1 b1)) → ¬ ((¬ f1 a1f1 b1) → f1 z))))) → ¬ g1(¬ (¬ h1(i1 ¬ ((i1 h1j1 ¬ ((j1 i1 → ¬ j1 = j1) → ¬ (¬ j1 = j1j1 i1))) → ¬ (j1 ¬ ((j1 i1 → ¬ j1 = j1) → ¬ (¬ j1 = j1j1 i1)) → i1 h1)) → ¬ h1 g1) → ¬ k1(k1 g1 → ¬ l1(m1 ¬ ((m1 l1 → ¬ n1(n1 k1o1p1 ¬ q1 ¬ ((q1 o1q1 = p1) → ¬ (q1 = p1q1 o1)) → (r1(r1 n1 → ¬ r1 o1) → ¬ s1 ¬ ((s1 m1 → (¬ s1 n1s1 o1)) → ¬ ((¬ s1 n1s1 o1) → s1 m1)))))) → ¬ (¬ n1(n1 k1o1p1 ¬ q1 ¬ ((q1 o1q1 = p1) → ¬ (q1 = p1q1 o1)) → (r1(r1 n1 → ¬ r1 o1) → ¬ s1 ¬ ((s1 m1 → (¬ s1 n1s1 o1)) → ¬ ((¬ s1 n1s1 o1) → s1 m1))))) → m1 l1)) → ¬ l1 g1))) → y g1)) → ¬ (z yg1(¬ (¬ h1(i1 ¬ ((i1 h1j1 ¬ ((j1 i1 → ¬ j1 = j1) → ¬ (¬ j1 = j1j1 i1))) → ¬ (j1 ¬ ((j1 i1 → ¬ j1 = j1) → ¬ (¬ j1 = j1j1 i1)) → i1 h1)) → ¬ h1 g1) → ¬ k1(k1 g1 → ¬ l1(m1 ¬ ((m1 l1 → ¬ n1(n1 k1o1p1 ¬ q1 ¬ ((q1 o1q1 = p1) → ¬ (q1 = p1q1 o1)) → (r1(r1 n1 → ¬ r1 o1) → ¬ s1 ¬ ((s1 m1 → (¬ s1 n1s1 o1)) → ¬ ((¬ s1 n1s1 o1) → s1 m1)))))) → ¬ (¬ n1(n1 k1o1p1 ¬ q1 ¬ ((q1 o1q1 = p1) → ¬ (q1 = p1q1 o1)) → (r1(r1 n1 → ¬ r1 o1) → ¬ s1 ¬ ((s1 m1 → (¬ s1 n1s1 o1)) → ¬ ((¬ s1 n1s1 o1) → s1 m1))))) → m1 l1)) → ¬ l1 g1))) → y g1))) → z x))) → t1 ¬ ((t1 xu1 ¬ ((u1 t1 → ¬ u1 = u1) → ¬ (¬ u1 = u1u1 t1))) → ¬ (u1 ¬ ((u1 t1 → ¬ u1 = u1) → ¬ (¬ u1 = u1u1 t1)) → t1 x))) → x A)))))
Distinct variable groups:   a1,b1,e1   a1,f1   y,a1,z   A,a,b   a,c   x,a,A   y,a   b1,c1,d1   b1,e1   b1,f1   y,b1,z   B,a   b,c,d   c1,d1   C,a   c,d,e,f   k,c   e,d,f,j   e,i   e,j   z,f1   f,g,h   f,i   f,j   g1,h1   g1,k1,l1   y,g1   g,h   h1,i1   i1,j1   k1,l1,m1   k1,n1,o1   k,l   k,o,p   l1,m1   m,l   m1,n1,o1,s1   m,n   n1,o1,r1   n1,s1   o1,p1,q1   o1,r1   o1,s1   o,p,q   o,r,s   p1,q1   q,p   r,q,s,w   v,r   w,r   t,s,u   v,s   w,s   t1,u1   x,t1   u,t   x,y,z
Allowed substitution hints:   A(y,z,w,v,u,t,e,f,g,h,i,j,k,m,n,o,s,r,q,p,c,d,l,a1,b1,c1,d1,e1,f1,g1,h1,i1,j1,k1,l1,m1,n1,o1,p1,q1,r1,s1,t1,u1)   B(x,y,z,w,v,u,t,e,f,g,h,i,j,k,m,n,o,s,r,q,p,b,c,d,l,a1,b1,c1,d1,e1,f1,g1,h1,i1,j1,k1,l1,m1,n1,o1,p1,q1,r1,s1,t1,u1)   C(x,y,z,w,v,u,t,e,f,g,h,i,j,k,m,n,o,s,r,q,p,b,c,d,l,a1,b1,c1,d1,e1,f1,g1,h1,i1,j1,k1,l1,m1,n1,o1,p1,q1,r1,s1,t1,u1)

Proof of Theorem elopprim
Dummy variable t3 is distinct from all other variables.
StepHypRef Expression
1 df-op 3674 . . . 4 B, C = ({t3 a B t3 = Phi a} ∪ {t3 a C t3 = ( Phi a ∪ {0c})})
21eleq2i 1958 . . 3 (A B, CA ({t3 a B t3 = Phi a} ∪ {t3 a C t3 = ( Phi a ∪ {0c})}))
3 elun 2622 . . 3 (A ({t3 a B t3 = Phi a} ∪ {t3 a C t3 = ( Phi a ∪ {0c})}) ↔ (A {t3 a B t3 = Phi a} A {t3 a C t3 = ( Phi a ∪ {0c})}))
42, 3bitri 237 . 2 (A B, C ↔ (A {t3 a B t3 = Phi a} A {t3 a C t3 = ( Phi a ∪ {0c})}))
5 elopprim.1 . . . . . 6 A V
6 eqeq1 1901 . . . . . . 7 (t3 = A → (t3 = Phi aA = Phi a))
76rexbidv 2122 . . . . . 6 (t3 = A → (a B t3 = Phi aa B A = Phi a))
85, 7elab 2412 . . . . 5 (A {t3 a B t3 = Phi a} ↔ a B A = Phi a)
9 dfcleq 1889 . . . . . . . . 9 (A = Phi ab(b Ab Phi a))
10 vex 2303 . . . . . . . . . . . . 13 b V
1110elphiprim 5505 . . . . . . . . . . . 12 (b Phi a ↔ ¬ c(c a → ¬ d ¬ ((d b → ((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)))) → ¬ (((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k))) → d b))))
1211bibi2i 301 . . . . . . . . . . 11 ((b Ab Phi a) ↔ (b A ↔ ¬ c(c a → ¬ d ¬ ((d b → ((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)))) → ¬ (((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k))) → d b)))))
13 dfbi1 181 . . . . . . . . . . 11 ((b A ↔ ¬ c(c a → ¬ d ¬ ((d b → ((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)))) → ¬ (((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k))) → d b)))) ↔ ¬ ((b A → ¬ c(c a → ¬ d ¬ ((d b → ((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)))) → ¬ (((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k))) → d b)))) → ¬ (¬ c(c a → ¬ d ¬ ((d b → ((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)))) → ¬ (((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k))) → d b))) → b A)))
1412, 13bitri 237 . . . . . . . . . 10 ((b Ab Phi a) ↔ ¬ ((b A → ¬ c(c a → ¬ d ¬ ((d b → ((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)))) → ¬ (((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k))) → d b)))) → ¬ (¬ c(c a → ¬ d ¬ ((d b → ((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)))) → ¬ (((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k))) → d b))) → b A)))
1514albii 1342 . . . . . . . . 9 (b(b Ab Phi a) ↔ b ¬ ((b A → ¬ c(c a → ¬ d ¬ ((d b → ((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)))) → ¬ (((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k))) → d b)))) → ¬ (¬ c(c a → ¬ d ¬ ((d b → ((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)))) → ¬ (((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k))) → d b))) → b A)))
169, 15bitri 237 . . . . . . . 8 (A = Phi ab ¬ ((b A → ¬ c(c a → ¬ d ¬ ((d b → ((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)))) → ¬ (((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k))) → d b)))) → ¬ (¬ c(c a → ¬ d ¬ ((d b → ((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)))) → ¬ (((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k))) → d b))) → b A)))
1716rexbii 2126 . . . . . . 7 (a B A = Phi aa B b ¬ ((b A → ¬ c(c a → ¬ d ¬ ((d b → ((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)))) → ¬ (((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k))) → d b)))) → ¬ (¬ c(c a → ¬ d ¬ ((d b → ((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)))) → ¬ (((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k))) → d b))) → b A)))
18 df-rex 2108 . . . . . . 7 (a B b ¬ ((b A → ¬ c(c a → ¬ d ¬ ((d b → ((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)))) → ¬ (((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k))) → d b)))) → ¬ (¬ c(c a → ¬ d ¬ ((d b → ((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)))) → ¬ (((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k))) → d b))) → b A)) ↔ a(a B b ¬ ((b A → ¬ c(c a → ¬ d ¬ ((d b → ((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)))) → ¬ (((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k))) → d b)))) → ¬ (¬ c(c a → ¬ d ¬ ((d b → ((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)))) → ¬ (((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k))) → d b))) → b A))))
1917, 18bitri 237 . . . . . 6 (a B A = Phi aa(a B b ¬ ((b A → ¬ c(c a → ¬ d ¬ ((d b → ((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)))) → ¬ (((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k))) → d b)))) → ¬ (¬ c(c a → ¬ d ¬ ((d b → ((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)))) → ¬ (((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k))) → d b))) → b A))))
20 alinexa 1355 . . . . . . 7 (a(a B → ¬ b ¬ ((b A → ¬ c(c a → ¬ d ¬ ((d b → ((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)))) → ¬ (((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k))) → d b)))) → ¬ (¬ c(c a → ¬ d ¬ ((d b → ((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)))) → ¬ (((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k))) → d b))) → b A))) ↔ ¬ a(a B b ¬ ((b A → ¬ c(c a → ¬ d ¬ ((d b → ((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)))) → ¬ (((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k))) → d b)))) → ¬ (¬ c(c a → ¬ d ¬ ((d b → ((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)))) → ¬ (((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k))) → d b))) → b A))))
2120con2bii 319 . . . . . 6 (a(a B b ¬ ((b A → ¬ c(c a → ¬ d ¬ ((d b → ((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)))) → ¬ (((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k))) → d b)))) → ¬ (¬ c(c a → ¬ d ¬ ((d b → ((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)))) → ¬ (((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k))) → d b))) → b A))) ↔ ¬ a(a B → ¬ b ¬ ((b A → ¬ c(c a → ¬ d ¬ ((d b → ((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)))) → ¬ (((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k))) → d b)))) → ¬ (¬ c(c a → ¬ d ¬ ((d b → ((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)))) → ¬ (((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k))) → d b))) → b A))))
2219, 21bitri 237 . . . . 5 (a B A = Phi a ↔ ¬ a(a B → ¬ b ¬ ((b A → ¬ c(c a → ¬ d ¬ ((d b → ((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)))) → ¬ (((¬ e(e cfg ¬ h ¬ ((h fh = g) → ¬ (h = gh f)) → (i(i e → ¬ i f) → ¬ j ¬ ((j d → (¬ j ej f)) → ¬ ((¬ j ej f) → j d))))) → ¬ k(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q))))) → q p)) → ¬ p k))) → c k)) → ¬ (d ck(¬ (¬ l(m ¬ ((m ln ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m))) → ¬ (n ¬ ((n m → ¬ n = n) → ¬ (¬ n = nn m)) → m l)) → ¬ l k) → ¬ o(o k → ¬ p(q ¬ ((q p → ¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v s) → ¬ w ¬ ((w q → (¬ w rw s)) → ¬ ((¬ w rw s) → w q)))))) → ¬ (¬ r(r ost ¬ u ¬ ((u su = t) → ¬ (u = tu s)) → (v(v r → ¬ v