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

Theorem 2false 350
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 239 . 2
43con4bii 297 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  <->wb 184
This theorem is referenced by:  bianfi  925  bifal  1408  iun0  4386  0iun  4387  sbcbr  4505  0xp  5085  cnv0  5414  co02  5526  0er  7365  00lss  17588  00ply1bas  18281  signswch  28518  dandysum2p2e4  32170  pexmidlem8N  35701
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 185
  Copyright terms: Public domain W3C validator