Theorem pm5.21 502

Description: Two propositions are equivalent if they are both false. Theorem *5.21 of [WhiteheadRussell] p. 124.

Assertion

Ref	Expression
pm5.21	⊢ ((¬ φ ∧ ¬ ψ) → (φ ↔ ψ))

Proof of Theorem pm5.21

Step	Hyp	Ref	Expression
1		pm5.1 501	. 2 ⊢ ((¬ φ ∧ ¬ ψ) → (¬ φ ↔ ¬ ψ))
2	1	bicon4d 402	1 ⊢ ((¬ φ ∧ ¬ ψ) → (φ ↔ ψ))

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∧ wa 196

This theorem is referenced by:  pm5.21ni 503  iun0 2028  xp0r 2474  dm0 2542  dmsn0 2543  dmsnsn0 2544  cnv0 2633  co02 2663  fn0 2739  cleqfv 2880  eceqopreq 3249  axrepnd 3740  lt2sq 4414  nn0ltp1let 4556  nn0subt 4587  zltp1let 4597  znnenlem 4929

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org