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

Theorem 2falsed 351
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 106 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 2falsed.2 . . 3  |-  ( ph  ->  -.  ch )
43pm2.21d 106 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
52, 4impbid 191 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  pm5.21ni  352  bianfd  924  sbcrext  3414  abvor0  3803  sbcel12  3823  sbcne12  3827  sbcel2  3831  sbcbr123  4498  csbxp  5081  smoord  7037  tfr2b  7066  axrepnd  8970  hasheq0  12402  sadcadd  13970  stdbdxmet  20845  iccpnfcnv  21271  cxple2  22903  uvtx01vtx  24265  eupath2lem1  24750  isoun  27289  xrge0iifcnv  27666  sgn0bi  28237  signswch  28269  fz0n  28861  hfext  29693
  Copyright terms: Public domain W3C validator