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 φ χ φ ψ χ φ ψ χ