ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  2falsed Unicode version

Theorem 2falsed 692
Description: Two falsehoods are equivalent (deduction form). (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 609 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 2falsed.2 . . 3  |-  ( ph  ->  -.  ch )
43pm2.21d 609 . 2  |-  ( ph  ->  ( ch  ->  ps ) )
52, 4impbid 128 1  |-  ( ph  ->  ( ps  <->  ch )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107  ax-in2 605
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm5.21ni  693  bianfd  933  abvor0dc  3390  nn0eln0  4540  nntri3  6400  fin0  6786  omp1eomlem  6986  ctssdccl  7003  ismkvnex  7036  xrlttri3  9612  nltpnft  9626  ngtmnft  9629  xrrebnd  9631  xltadd1  9688  xposdif  9694  xleaddadd  9699  hashnncl  10573  zfz1isolemiso  10613  mod2eq1n2dvds  11610  m1exp1  11632
  Copyright terms: Public domain W3C validator