Theorem 2false 364

Description: Two falsehoods are equivalent. (Contributed by NM, 4-Apr-2005.) (Proof shortened by Wolf Lammen, 19-May-2013.)

Hypotheses

Ref	Expression
2false.1	⊢ ¬ 𝜑
2false.2	⊢ ¬ 𝜓

Assertion

Ref	Expression
2false	⊢ (𝜑 ↔ 𝜓)

Proof of Theorem 2false

Step	Hyp	Ref	Expression
1		2false.1	. . 3 ⊢ ¬ 𝜑
2		2false.2	. . 3 ⊢ ¬ 𝜓
3	1, 2	2th 253	. 2 ⊢ (¬ 𝜑 ↔ ¬ 𝜓)
4	3	con4bii 310	1 ⊢ (𝜑 ↔ 𝜓)

Syntax hints:  ¬ wn 3   ↔ wb 195

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

This theorem depends on definitions:  df-bi 196

This theorem is referenced by:  bianfi  962  bifal  1488  iun0  4512  0iun  4513  0xp  5122  cnv0OLD  5455  co02  5566  0er  7667  0erOLD  7668  00lss  18763  00ply1bas  19431  2lgslem4  24931  signswch  29964  finxp0  32404  pexmidlem8N  34281  dandysum2p2e4  39814