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

Theorem 2falsed 697
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 614 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
3 2falsed.2 . . 3  |-  ( ph  ->  -.  ch )
43pm2.21d 614 . 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 610
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm5.21ni  698  bianfd  943  abvor0dc  3437  nn0eln0  4602  nntri3  6474  fin0  6861  omp1eomlem  7069  ctssdccl  7086  ismkvnex  7129  xrlttri3  9747  nltpnft  9764  ngtmnft  9767  xrrebnd  9769  xltadd1  9826  xposdif  9832  xleaddadd  9837  hashnncl  10723  zfz1isolemiso  10767  mod2eq1n2dvds  11831  m1exp1  11853  pceq0  12268
  Copyright terms: Public domain W3C validator