This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY Propositional calculus Abbreviated conjunction and disjunction of three wff's 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 ⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) ↔ ¬ ( ¬ 𝜑 ∨ ¬ 𝜓 ∨ ¬ 𝜒 ) )