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

Theorem 2th 252
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 197 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 194
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 195
This theorem is referenced by:  2false  363  trujust  1476  dftru2  1482  bitru  1486  vjust  3170  dfnul2  3872  dfnul3  3873  rab0OLD  3906  pwv  4362  int0  4416  int0OLD  4417  0iin  4505  snnex  6836  orduninsuc  6909  fo1st  7053  fo2nd  7054  1st2val  7059  2nd2val  7060  eqer  7638  eqerOLD  7639  ener  7862  enerOLD  7863  ruv  8364  acncc  9119  grothac  9505  grothtsk  9510  hashneq0  12965  rexfiuz  13878  foo3  28489  signswch  29767  dfpo2  30701  domep  30745  fobigcup  30980  elhf2  31255  limsucncmpi  31417  bj-vjust  31784  bj-df-v  32007  uunT1  37828  nabctnabc  39548  clifte  39552  cliftet  39553  clifteta  39554  cliftetb  39555  confun5  39560  pldofph  39562  lco0  42009
  Copyright terms: Public domain W3C validator