Metamath Proof Explorer

Theorem nic-axALT

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

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

Proof

Step Hyp Ref Expression
1 simpl ⊢ χ ∧ ψ → χ
2 1 imim2i ⊢ φ → χ ∧ ψ → φ → χ
3 con3 ⊢ φ → χ → ¬ χ → ¬ φ
4 3 imim2d ⊢ φ → χ → θ → ¬ χ → θ → ¬ φ
5 2 4 syl ⊢ φ → χ ∧ ψ → θ → ¬ χ → θ → ¬ φ
6 anidm ⊢ τ ∧ τ ↔ τ
7 6 biimpri ⊢ τ → τ ∧ τ
8 5 7 jctil ⊢ φ → χ ∧ ψ → τ → τ ∧ τ ∧ θ → ¬ χ → θ → ¬ φ
9 df-nan ⊢ χ ⊼ ψ ↔ ¬ χ ∧ ψ
10 9 anbi2i ⊢ φ ∧ χ ⊼ ψ ↔ φ ∧ ¬ χ ∧ ψ
11 10 notbii ⊢ ¬ φ ∧ χ ⊼ ψ ↔ ¬ φ ∧ ¬ χ ∧ ψ
12 df-nan ⊢ φ ⊼ χ ⊼ ψ ↔ ¬ φ ∧ χ ⊼ ψ
13 iman ⊢ φ → χ ∧ ψ ↔ ¬ φ ∧ ¬ χ ∧ ψ
14 11 12 13 3bitr4i ⊢ φ ⊼ χ ⊼ ψ ↔ φ → χ ∧ ψ
15 df-nan ⊢ τ ⊼ τ ⊼ τ ⊼ θ ⊼ χ ⊼ φ ⊼ θ ⊼ φ ⊼ θ ↔ ¬ τ ⊼ τ ⊼ τ ∧ θ ⊼ χ ⊼ φ ⊼ θ ⊼ φ ⊼ θ
16 df-nan ⊢ τ ⊼ τ ↔ ¬ τ ∧ τ
17 16 anbi2i ⊢ τ ∧ τ ⊼ τ ↔ τ ∧ ¬ τ ∧ τ
18 17 notbii ⊢ ¬ τ ∧ τ ⊼ τ ↔ ¬ τ ∧ ¬ τ ∧ τ
19 df-nan ⊢ τ ⊼ τ ⊼ τ ↔ ¬ τ ∧ τ ⊼ τ
20 iman ⊢ τ → τ ∧ τ ↔ ¬ τ ∧ ¬ τ ∧ τ
21 18 19 20 3bitr4i ⊢ τ ⊼ τ ⊼ τ ↔ τ → τ ∧ τ
22 df-nan ⊢ θ ⊼ χ ↔ ¬ θ ∧ χ
23 imnan ⊢ θ → ¬ χ ↔ ¬ θ ∧ χ
24 22 23 bitr4i ⊢ θ ⊼ χ ↔ θ → ¬ χ
25 df-nan ⊢ φ ⊼ θ ⊼ φ ⊼ θ ↔ ¬ φ ⊼ θ ∧ φ ⊼ θ
26 anidm ⊢ φ ⊼ θ ∧ φ ⊼ θ ↔ φ ⊼ θ
27 df-nan ⊢ φ ⊼ θ ↔ ¬ φ ∧ θ
28 imnan ⊢ φ → ¬ θ ↔ ¬ φ ∧ θ
29 con2b ⊢ φ → ¬ θ ↔ θ → ¬ φ
30 28 29 bitr3i ⊢ ¬ φ ∧ θ ↔ θ → ¬ φ
31 26 27 30 3bitri ⊢ φ ⊼ θ ∧ φ ⊼ θ ↔ θ → ¬ φ
32 25 31 xchbinx ⊢ φ ⊼ θ ⊼ φ ⊼ θ ↔ ¬ θ → ¬ φ
33 24 32 anbi12i ⊢ θ ⊼ χ ∧ φ ⊼ θ ⊼ φ ⊼ θ ↔ θ → ¬ χ ∧ ¬ θ → ¬ φ
34 33 notbii ⊢ ¬ θ ⊼ χ ∧ φ ⊼ θ ⊼ φ ⊼ θ ↔ ¬ θ → ¬ χ ∧ ¬ θ → ¬ φ
35 df-nan ⊢ θ ⊼ χ ⊼ φ ⊼ θ ⊼ φ ⊼ θ ↔ ¬ θ ⊼ χ ∧ φ ⊼ θ ⊼ φ ⊼ θ
36 iman ⊢ θ → ¬ χ → θ → ¬ φ ↔ ¬ θ → ¬ χ ∧ ¬ θ → ¬ φ
37 34 35 36 3bitr4i ⊢ θ ⊼ χ ⊼ φ ⊼ θ ⊼ φ ⊼ θ ↔ θ → ¬ χ → θ → ¬ φ
38 21 37 anbi12i ⊢ τ ⊼ τ ⊼ τ ∧ θ ⊼ χ ⊼ φ ⊼ θ ⊼ φ ⊼ θ ↔ τ → τ ∧ τ ∧ θ → ¬ χ → θ → ¬ φ
39 15 38 xchbinx ⊢ τ ⊼ τ ⊼ τ ⊼ θ ⊼ χ ⊼ φ ⊼ θ ⊼ φ ⊼ θ ↔ ¬ τ → τ ∧ τ ∧ θ → ¬ χ → θ → ¬ φ
40 14 39 anbi12i ⊢ φ ⊼ χ ⊼ ψ ∧ τ ⊼ τ ⊼ τ ⊼ θ ⊼ χ ⊼ φ ⊼ θ ⊼ φ ⊼ θ ↔ φ → χ ∧ ψ ∧ ¬ τ → τ ∧ τ ∧ θ → ¬ χ → θ → ¬ φ
41 40 notbii ⊢ ¬ φ ⊼ χ ⊼ ψ ∧ τ ⊼ τ ⊼ τ ⊼ θ ⊼ χ ⊼ φ ⊼ θ ⊼ φ ⊼ θ ↔ ¬ φ → χ ∧ ψ ∧ ¬ τ → τ ∧ τ ∧ θ → ¬ χ → θ → ¬ φ
42 iman ⊢ φ → χ ∧ ψ → τ → τ ∧ τ ∧ θ → ¬ χ → θ → ¬ φ ↔ ¬ φ → χ ∧ ψ ∧ ¬ τ → τ ∧ τ ∧ θ → ¬ χ → θ → ¬ φ
43 41 42 bitr4i ⊢ ¬ φ ⊼ χ ⊼ ψ ∧ τ ⊼ τ ⊼ τ ⊼ θ ⊼ χ ⊼ φ ⊼ θ ⊼ φ ⊼ θ ↔ φ → χ ∧ ψ → τ → τ ∧ τ ∧ θ → ¬ χ → θ → ¬ φ
44 8 43 mpbir ⊢ ¬ φ ⊼ χ ⊼ ψ ∧ τ ⊼ τ ⊼ τ ⊼ θ ⊼ χ ⊼ φ ⊼ θ ⊼ φ ⊼ θ
45 df-nan ⊢ φ ⊼ χ ⊼ ψ ⊼ τ ⊼ τ ⊼ τ ⊼ θ ⊼ χ ⊼ φ ⊼ θ ⊼ φ ⊼ θ ↔ ¬ φ ⊼ χ ⊼ ψ ∧ τ ⊼ τ ⊼ τ ⊼ θ ⊼ χ ⊼ φ ⊼ θ ⊼ φ ⊼ θ
46 44 45 mpbir ⊢ φ ⊼ χ ⊼ ψ ⊼ τ ⊼ τ ⊼ τ ⊼ θ ⊼ χ ⊼ φ ⊼ θ ⊼ φ ⊼ θ