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  3472  smoord  6382  tfr2b  6412  axrepnd  8216  hasheq0  11353  sadcadd  12649  stdbdxmet  18061  iccpnfcnv  18442  cxple2  20044  xrge0iifcnv  23315  eupath2lem1  23901  fz0n  24097  hfext  24813  uvtx01vtx  28164
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