Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  2false Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 2false.1 . . 3 ¬ 𝜑
2 2false.2 . . 3 ¬ 𝜓
31, 22th 253 . 2 𝜑 ↔ ¬ 𝜓)
43con4bii 310 1 (𝜑𝜓)
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator