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

Theorem 2th 167
Description: Two truths are equivalent. (Contributed by NM, 18-Aug-1993.)
Hypotheses
Ref Expression
2th.1 𝜑
2th.2 𝜓
Assertion
Ref Expression
2th (𝜑𝜓)

Proof of Theorem 2th
StepHypRef Expression
1 2th.2 . . 3 𝜓
21a1i 9 . 2 (𝜑𝜓)
3 2th.1 . . 3 𝜑
43a1i 9 . 2 (𝜓𝜑)
52, 4impbii 121 1 (𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  trujust  1261  dftru2  1267  bitru  1271  vjust  2575  pwv  3607  int0  3657  0iin  3743  snnex  4209  ruv  4302  fo1st  5812  fo2nd  5813  eqer  6169  ener  6290  rexfiuz  9816  bdth  10338
  Copyright terms: Public domain W3C validator