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

Theorem 2th 172
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 124 1  |-  ( ph  <->  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  trujust  1289  dftru2  1295  bitru  1299  vjust  2616  pwv  3634  int0  3684  0iin  3770  snnex  4243  ruv  4337  fo1st  5878  fo2nd  5879  eqer  6269  ener  6441  rexfiuz  10309  bdth  11151
  Copyright terms: Public domain W3C validator