MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2th Unicode version

Theorem 2th 239
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 11 . 2
3 2th.1 . . 3
43a1i 11 . 2
52, 4impbii 188 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184
This theorem is referenced by:  2false  350  trujust  1397  dftru2  1403  bitru  1407  vjust  3110  dfnul2  3786  dfnul3  3787  rab0  3806  pwv  4248  int0  4300  0iin  4388  snnex  6606  orduninsuc  6678  fo1st  6820  fo2nd  6821  1st2val  6826  2nd2val  6827  eqer  7363  ener  7582  ruv  8048  acncc  8841  grothac  9229  grothtsk  9234  hashneq0  12434  rexfiuz  13180  foo3  27362  signswch  28518  dfpo2  29184  domep  29225  fobigcup  29550  elhf2  29832  limsucncmpi  29910  lco0  33028  uunT1  33577  bj-vjust  34372  bj-df-v  34583
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
  Copyright terms: Public domain W3C validator