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  916  bifal  1383  iun0  4343  0iun  4344  sbcbr  4462  0xp  5034  cnv0  5359  co02  5470  0er  7270  00lss  17199  00ply1bas  17875  signswch  27418  dandysum2p2e4  30866  pexmidlem8N  34472
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