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

Theorem 2th 172
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 124 1 (𝜑𝜓)
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  2615  pwv  3629  int0  3679  0iin  3765  snnex  4238  ruv  4332  fo1st  5866  fo2nd  5867  eqer  6257  ener  6429  rexfiuz  10263  bdth  11079
  Copyright terms: Public domain W3C validator