Theorem nic-axALT 1439

Description: A direct proof of nic-ax 1438. (Contributed by NM, 11-Dec-2008.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
nic-axALT	⊢ ((φ ⊼ (χ ⊼ ψ)) ⊼ ((τ ⊼ (τ ⊼ τ)) ⊼ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ)))))

Proof of Theorem nic-axALT

Step	Hyp	Ref	Expression
1		simpl 443	. . . . . 6 ⊢ ((χ ∧ ψ) → χ)
2	1	imim2i 13	. . . . 5 ⊢ ((φ → (χ ∧ ψ)) → (φ → χ))
3		con3 126	. . . . . 6 ⊢ ((φ → χ) → (¬ χ → ¬ φ))
4	3	imim2d 48	. . . . 5 ⊢ ((φ → χ) → ((θ → ¬ χ) → (θ → ¬ φ)))
5	2, 4	syl 15	. . . 4 ⊢ ((φ → (χ ∧ ψ)) → ((θ → ¬ χ) → (θ → ¬ φ)))
6		anidm 625	. . . . 5 ⊢ ((τ ∧ τ) ↔ τ)
7	6	biimpri 197	. . . 4 ⊢ (τ → (τ ∧ τ))
8	5, 7	jctil 523	. . 3 ⊢ ((φ → (χ ∧ ψ)) → ((τ → (τ ∧ τ)) ∧ ((θ → ¬ χ) → (θ → ¬ φ))))
9		df-nan 1288	. . . . . . . . 9 ⊢ ((χ ⊼ ψ) ↔ ¬ (χ ∧ ψ))
10	9	anbi2i 675	. . . . . . . 8 ⊢ ((φ ∧ (χ ⊼ ψ)) ↔ (φ ∧ ¬ (χ ∧ ψ)))
11	10	notbii 287	. . . . . . 7 ⊢ (¬ (φ ∧ (χ ⊼ ψ)) ↔ ¬ (φ ∧ ¬ (χ ∧ ψ)))
12		df-nan 1288	. . . . . . 7 ⊢ ((φ ⊼ (χ ⊼ ψ)) ↔ ¬ (φ ∧ (χ ⊼ ψ)))
13		iman 413	. . . . . . 7 ⊢ ((φ → (χ ∧ ψ)) ↔ ¬ (φ ∧ ¬ (χ ∧ ψ)))
14	11, 12, 13	3bitr4i 268	. . . . . 6 ⊢ ((φ ⊼ (χ ⊼ ψ)) ↔ (φ → (χ ∧ ψ)))
15		df-nan 1288	. . . . . . 7 ⊢ (((τ ⊼ (τ ⊼ τ)) ⊼ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ)))) ↔ ¬ ((τ ⊼ (τ ⊼ τ)) ∧ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ)))))
16		df-nan 1288	. . . . . . . . . . 11 ⊢ ((τ ⊼ τ) ↔ ¬ (τ ∧ τ))
17	16	anbi2i 675	. . . . . . . . . 10 ⊢ ((τ ∧ (τ ⊼ τ)) ↔ (τ ∧ ¬ (τ ∧ τ)))
18	17	notbii 287	. . . . . . . . 9 ⊢ (¬ (τ ∧ (τ ⊼ τ)) ↔ ¬ (τ ∧ ¬ (τ ∧ τ)))
19		df-nan 1288	. . . . . . . . 9 ⊢ ((τ ⊼ (τ ⊼ τ)) ↔ ¬ (τ ∧ (τ ⊼ τ)))
20		iman 413	. . . . . . . . 9 ⊢ ((τ → (τ ∧ τ)) ↔ ¬ (τ ∧ ¬ (τ ∧ τ)))
21	18, 19, 20	3bitr4i 268	. . . . . . . 8 ⊢ ((τ ⊼ (τ ⊼ τ)) ↔ (τ → (τ ∧ τ)))
22		df-nan 1288	. . . . . . . . . . . 12 ⊢ ((θ ⊼ χ) ↔ ¬ (θ ∧ χ))
23		imnan 411	. . . . . . . . . . . 12 ⊢ ((θ → ¬ χ) ↔ ¬ (θ ∧ χ))
24	22, 23	bitr4i 243	. . . . . . . . . . 11 ⊢ ((θ ⊼ χ) ↔ (θ → ¬ χ))
25		df-nan 1288	. . . . . . . . . . . 12 ⊢ (((φ ⊼ θ) ⊼ (φ ⊼ θ)) ↔ ¬ ((φ ⊼ θ) ∧ (φ ⊼ θ)))
26		anidm 625	. . . . . . . . . . . . 13 ⊢ (((φ ⊼ θ) ∧ (φ ⊼ θ)) ↔ (φ ⊼ θ))
27		df-nan 1288	. . . . . . . . . . . . 13 ⊢ ((φ ⊼ θ) ↔ ¬ (φ ∧ θ))
28		imnan 411	. . . . . . . . . . . . . 14 ⊢ ((φ → ¬ θ) ↔ ¬ (φ ∧ θ))
29		con2b 324	. . . . . . . . . . . . . 14 ⊢ ((φ → ¬ θ) ↔ (θ → ¬ φ))
30	28, 29	bitr3i 242	. . . . . . . . . . . . 13 ⊢ (¬ (φ ∧ θ) ↔ (θ → ¬ φ))
31	26, 27, 30	3bitri 262	. . . . . . . . . . . 12 ⊢ (((φ ⊼ θ) ∧ (φ ⊼ θ)) ↔ (θ → ¬ φ))
32	25, 31	xchbinx 301	. . . . . . . . . . 11 ⊢ (((φ ⊼ θ) ⊼ (φ ⊼ θ)) ↔ ¬ (θ → ¬ φ))
33	24, 32	anbi12i 678	. . . . . . . . . 10 ⊢ (((θ ⊼ χ) ∧ ((φ ⊼ θ) ⊼ (φ ⊼ θ))) ↔ ((θ → ¬ χ) ∧ ¬ (θ → ¬ φ)))
34	33	notbii 287	. . . . . . . . 9 ⊢ (¬ ((θ ⊼ χ) ∧ ((φ ⊼ θ) ⊼ (φ ⊼ θ))) ↔ ¬ ((θ → ¬ χ) ∧ ¬ (θ → ¬ φ)))
35		df-nan 1288	. . . . . . . . 9 ⊢ (((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ))) ↔ ¬ ((θ ⊼ χ) ∧ ((φ ⊼ θ) ⊼ (φ ⊼ θ))))
36		iman 413	. . . . . . . . 9 ⊢ (((θ → ¬ χ) → (θ → ¬ φ)) ↔ ¬ ((θ → ¬ χ) ∧ ¬ (θ → ¬ φ)))
37	34, 35, 36	3bitr4i 268	. . . . . . . 8 ⊢ (((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ))) ↔ ((θ → ¬ χ) → (θ → ¬ φ)))
38	21, 37	anbi12i 678	. . . . . . 7 ⊢ (((τ ⊼ (τ ⊼ τ)) ∧ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ)))) ↔ ((τ → (τ ∧ τ)) ∧ ((θ → ¬ χ) → (θ → ¬ φ))))
39	15, 38	xchbinx 301	. . . . . 6 ⊢ (((τ ⊼ (τ ⊼ τ)) ⊼ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ)))) ↔ ¬ ((τ → (τ ∧ τ)) ∧ ((θ → ¬ χ) → (θ → ¬ φ))))
40	14, 39	anbi12i 678	. . . . 5 ⊢ (((φ ⊼ (χ ⊼ ψ)) ∧ ((τ ⊼ (τ ⊼ τ)) ⊼ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ))))) ↔ ((φ → (χ ∧ ψ)) ∧ ¬ ((τ → (τ ∧ τ)) ∧ ((θ → ¬ χ) → (θ → ¬ φ)))))
41	40	notbii 287	. . . 4 ⊢ (¬ ((φ ⊼ (χ ⊼ ψ)) ∧ ((τ ⊼ (τ ⊼ τ)) ⊼ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ))))) ↔ ¬ ((φ → (χ ∧ ψ)) ∧ ¬ ((τ → (τ ∧ τ)) ∧ ((θ → ¬ χ) → (θ → ¬ φ)))))
42		iman 413	. . . 4 ⊢ (((φ → (χ ∧ ψ)) → ((τ → (τ ∧ τ)) ∧ ((θ → ¬ χ) → (θ → ¬ φ)))) ↔ ¬ ((φ → (χ ∧ ψ)) ∧ ¬ ((τ → (τ ∧ τ)) ∧ ((θ → ¬ χ) → (θ → ¬ φ)))))
43	41, 42	bitr4i 243	. . 3 ⊢ (¬ ((φ ⊼ (χ ⊼ ψ)) ∧ ((τ ⊼ (τ ⊼ τ)) ⊼ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ))))) ↔ ((φ → (χ ∧ ψ)) → ((τ → (τ ∧ τ)) ∧ ((θ → ¬ χ) → (θ → ¬ φ)))))
44	8, 43	mpbir 200	. 2 ⊢ ¬ ((φ ⊼ (χ ⊼ ψ)) ∧ ((τ ⊼ (τ ⊼ τ)) ⊼ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ)))))
45		df-nan 1288	. 2 ⊢ (((φ ⊼ (χ ⊼ ψ)) ⊼ ((τ ⊼ (τ ⊼ τ)) ⊼ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ))))) ↔ ¬ ((φ ⊼ (χ ⊼ ψ)) ∧ ((τ ⊼ (τ ⊼ τ)) ⊼ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ))))))
46	44, 45	mpbir 200	1 ⊢ ((φ ⊼ (χ ⊼ ψ)) ⊼ ((τ ⊼ (τ ⊼ τ)) ⊼ ((θ ⊼ χ) ⊼ ((φ ⊼ θ) ⊼ (φ ⊼ θ)))))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 358   ⊼ wnan 1287

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 177  df-an 360  df-nan 1288

This theorem is used by: (None)