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

Theorem 2false 339
Description: Two falsehoods are equivalent. (Contributed by NM, 4-Apr-2005.) (Proof shortened by Wolf Lammen, 19-May-2013.)
Hypotheses
Ref Expression
2false.1  |-  -.  ph
2false.2  |-  -.  ps
Assertion
Ref Expression
2false  |-  ( ph  <->  ps )

Proof of Theorem 2false
StepHypRef Expression
1 2false.1 . . 3  |-  -.  ph
2 2false.2 . . 3  |-  -.  ps
31, 22th 230 . 2  |-  ( -. 
ph 
<->  -.  ps )
43con4bii 288 1  |-  ( ph  <->  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176
This theorem is referenced by:  bianfi  891  bifal  1318  iun0  3974  0iun  3975  xp0r  4784  cnv0  5100  co02  5202  0er  6711  00lss  15715  00ply1bas  16334  dandysum2p2e4  28046  osumcllem11N  30777  pexmidlem8N  30788  dochexmidlem8  32279
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator