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 ⊢φ⊼χ⊼ψ⊼τ⊼τ⊼τ⊼θ⊼χ⊼φ⊼θ⊼φ⊼θ