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  3958  0iun  3959  xp0r  4768  cnv0  5084  co02  5186  0er  6695  00lss  15699  00ply1bas  16318  dandysum2p2e4  27943  osumcllem11N  30155  pexmidlem8N  30166  dochexmidlem8  31657
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