Theorem oran

Description: Disjunction in terms of conjunction (De Morgan's law). Compare Theorem *4.57 of WhiteheadRussell p. 120. (Contributed by NM, 3-Jan-1993) (Proof shortened by Andrew Salmon, 7-May-2011)

	Ref	Expression
Assertion	oran	⊢ ( ( 𝜑 ∨ 𝜓 ) ↔ ¬ ( ¬ 𝜑 ∧ ¬ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		pm4.56	⊢ ( ( ¬ 𝜑 ∧ ¬ 𝜓 ) ↔ ¬ ( 𝜑 ∨ 𝜓 ) )
2	1	con2bii	⊢ ( ( 𝜑 ∨ 𝜓 ) ↔ ¬ ( ¬ 𝜑 ∧ ¬ 𝜓 ) )