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

Theorem 2falsed 352
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 109 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 2falsed.2 . . 3  |-  ( ph  ->  -.  ch )
43pm2.21d 109 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
52, 4impbid 193 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187
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 188
This theorem is referenced by:  pm5.21ni  353  bianfd  934  sbcrext  3379  abvor0  3786  sbcel12  3806  sbcne12  3809  sbcel2  3812  sbcbr123  4477  csbxp  4936  smoord  7092  tfr2b  7122  axrepnd  9017  hasheq0  12541  sadcadd  14406  stdbdxmet  21461  iccpnfcnv  21868  cxple2  23507  mirbtwnhl  24584  uvtx01vtx  25065  eupath2lem1  25550  isoun  28122  1smat1  28469  xrge0iifcnv  28578  sgn0bi  29206  signswch  29238  fz0n  30151  hfext  30735
  Copyright terms: Public domain W3C validator