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

Theorem 2th 253
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 198 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 195
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 196
This theorem is referenced by:  2false  364  trujust  1477  dftru2  1483  bitru  1487  vjust  3174  dfnul2  3876  dfnul3  3877  rab0OLD  3910  pwv  4371  int0  4425  int0OLD  4426  0iin  4514  snnex  6862  orduninsuc  6935  fo1st  7079  fo2nd  7080  1st2val  7085  2nd2val  7086  eqer  7664  eqerOLD  7665  ener  7888  enerOLD  7889  ruv  8390  acncc  9145  grothac  9531  grothtsk  9536  hashneq0  13016  rexfiuz  13935  foo3  28686  signswch  29964  dfpo2  30898  domep  30942  fobigcup  31177  elhf2  31452  limsucncmpi  31614  bj-vjust  31974  bj-df-v  32207  uunT1  38028  nabctnabc  39747  clifte  39751  cliftet  39752  clifteta  39753  cliftetb  39754  confun5  39759  pldofph  39761  lco0  42010
  Copyright terms: Public domain W3C validator