This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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