Metamath Proof Explorer

Theorem nanass

Description: A characterization of when an expression involving alternative denials associates. Remark: alternative denial is commutative, see nancom . (Contributed by Richard Penner, 29-Feb-2020) (Proof shortened by Wolf Lammen, 23-Oct-2022)

Ref Expression
Assertion nanass ⊢φ↔χ↔φ⊼ψ⊼χ↔φ⊼ψ⊼χ

Proof

Step Hyp Ref Expression
1 bicom1 ⊢φ↔χ→χ↔φ
2 nanbi2 ⊢φ↔χ→ψ⊼φ↔ψ⊼χ
3 1 2 nanbi12d ⊢φ↔χ→χ⊼ψ⊼φ↔φ⊼ψ⊼χ
4 nannan ⊢φ⊼ψ⊼χ↔φ→ψ∧χ
5 simpr ⊢ψ∧χ→χ
6 5 imim2i ⊢φ→ψ∧χ→φ→χ
7 4 6 sylbi ⊢φ⊼ψ⊼χ→φ→χ
8 nannan ⊢χ⊼ψ⊼φ↔χ→ψ∧φ
9 simpr ⊢ψ∧φ→φ
10 9 imim2i ⊢χ→ψ∧φ→χ→φ
11 8 10 sylbi ⊢χ⊼ψ⊼φ→χ→φ
12 7 11 impbid21d ⊢χ⊼ψ⊼φ→φ⊼ψ⊼χ→φ↔χ
13 nanan ⊢φ∧ψ⊼χ↔¬φ⊼ψ⊼χ
14 simpl ⊢φ∧ψ⊼χ→φ
15 13 14 sylbir ⊢¬φ⊼ψ⊼χ→φ
16 nanan ⊢χ∧ψ⊼φ↔¬χ⊼ψ⊼φ
17 simpl ⊢χ∧ψ⊼φ→χ
18 16 17 sylbir ⊢¬χ⊼ψ⊼φ→χ
19 pm5.1im ⊢φ→χ→φ↔χ
20 15 18 19 syl2imc ⊢¬χ⊼ψ⊼φ→¬φ⊼ψ⊼χ→φ↔χ
21 12 20 bija ⊢χ⊼ψ⊼φ↔φ⊼ψ⊼χ→φ↔χ
22 3 21 impbii ⊢φ↔χ↔χ⊼ψ⊼φ↔φ⊼ψ⊼χ
23 nancom ⊢ψ⊼φ↔φ⊼ψ
24 23 nanbi2i ⊢χ⊼ψ⊼φ↔χ⊼φ⊼ψ
25 nancom ⊢χ⊼φ⊼ψ↔φ⊼ψ⊼χ
26 24 25 bitri ⊢χ⊼ψ⊼φ↔φ⊼ψ⊼χ
27 26 bibi1i ⊢χ⊼ψ⊼φ↔φ⊼ψ⊼χ↔φ⊼ψ⊼χ↔φ⊼ψ⊼χ
28 22 27 bitri ⊢φ↔χ↔φ⊼ψ⊼χ↔φ⊼ψ⊼χ