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

Theorem 2th 174
Description: Two truths are equivalent. (Contributed by NM, 18-Aug-1993.)
Hypotheses
Ref Expression
2th.1  |-  ph
2th.2  |-  ps
Assertion
Ref Expression
2th  |-  ( ph  <->  ps )

Proof of Theorem 2th
StepHypRef Expression
1 2th.2 . . 3  |-  ps
21a1i 9 . 2  |-  ( ph  ->  ps )
3 2th.1 . . 3  |-  ph
43a1i 9 . 2  |-  ( ps 
->  ph )
52, 4impbii 126 1  |-  ( ph  <->  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  trujust  1355  dftru2  1361  bitru  1365  vjust  2738  pwv  3808  int0  3858  0iin  3945  snnex  4448  ruv  4549  fo1st  6157  fo2nd  6158  eqer  6566  ener  6778  rexfiuz  10993  bdth  14503
  Copyright terms: Public domain W3C validator