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

Theorem 2th 173
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 125 1  |-  ( ph  <->  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  trujust  1334  dftru2  1340  bitru  1344  vjust  2690  pwv  3743  int0  3793  0iin  3879  snnex  4377  ruv  4473  fo1st  6063  fo2nd  6064  eqer  6469  ener  6681  rexfiuz  10793  bdth  13200
  Copyright terms: Public domain W3C validator