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

Theorem 2falsed 341
Description: Two falsehoods are equivalent (deduction rule). (Contributed by NM, 11-Oct-2013.)
Hypotheses
Ref Expression
2falsed.1  |-  ( ph  ->  -.  ps )
2falsed.2  |-  ( ph  ->  -.  ch )
Assertion
Ref Expression
2falsed  |-  ( ph  ->  ( ps  <->  ch )
)

Proof of Theorem 2falsed
StepHypRef Expression
1 2falsed.1 . . 3  |-  ( ph  ->  -.  ps )
21pm2.21d 100 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 2falsed.2 . . 3  |-  ( ph  ->  -.  ch )
43pm2.21d 100 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
52, 4impbid 184 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177
This theorem is referenced by:  pm5.21ni  342  bianfd  893  abvor0  3590  smoord  6565  tfr2b  6595  axrepnd  8404  hasheq0  11573  sadcadd  12899  stdbdxmet  18437  iccpnfcnv  18842  cxple2  20457  uvtx01vtx  21369  eupath2lem1  21549  isoun  23932  xrge0iifcnv  24125  fz0n  24983  hfext  25840
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 178
  Copyright terms: Public domain W3C validator