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

Metamath Proof Explorer

Theorem ioran

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

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

Proof

Step	Hyp	Ref	Expression
1		pm4.65	⊢ ( ¬ ( ¬ 𝜑 → 𝜓 ) ↔ ( ¬ 𝜑 ∧ ¬ 𝜓 ) )
2		pm4.64	⊢ ( ( ¬ 𝜑 → 𝜓 ) ↔ ( 𝜑 ∨ 𝜓 ) )
3	1 2	xchnxbi	⊢ ( ¬ ( 𝜑 ∨ 𝜓 ) ↔ ( ¬ 𝜑 ∧ ¬ 𝜓 ) )