Metamath Proof Explorer


Theorem 3anor

Description: Triple conjunction expressed in terms of triple disjunction. (Contributed by Jeff Hankins, 15-Aug-2009) (Proof shortened by Wolf Lammen, 8-Apr-2022)

Ref Expression
Assertion 3anor φψχ¬¬φ¬ψ¬χ

Proof

Step Hyp Ref Expression
1 3ianor ¬φψχ¬φ¬ψ¬χ
2 1 con1bii ¬¬φ¬ψ¬χφψχ
3 2 bicomi φψχ¬¬φ¬ψ¬χ