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

Theorem 2falsed 340
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 98 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 2falsed.2 . . 3  |-  ( ph  ->  -.  ch )
43pm2.21d 98 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
52, 4impbid 183 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176
This theorem is referenced by:  pm5.21ni  341  bianfd  892  abvor0  3485  smoord  6398  tfr2b  6428  axrepnd  8232  hasheq0  11369  sadcadd  12665  stdbdxmet  18077  iccpnfcnv  18458  cxple2  20060  xrge0iifcnv  23330  eupath2lem1  23916  fz0n  24112  hfext  24885  uvtx01vtx  28305
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