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

Theorem 2th 173
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 125 1 (𝜑𝜓)
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  1333  dftru2  1339  bitru  1343  vjust  2687  pwv  3735  int0  3785  0iin  3871  snnex  4369  ruv  4465  fo1st  6055  fo2nd  6056  eqer  6461  ener  6673  rexfiuz  10768  bdth  13059
  Copyright terms: Public domain W3C validator