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

Theorem 2th 254
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 199 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 196
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 197
This theorem is referenced by:  2false  365  trujust  1483  dftru2  1489  bitru  1494  vjust  3196  dfnul2  3909  dfnul3  3910  rab0OLD  3947  pwv  4424  int0  4481  int0OLD  4482  0iin  4569  snnexOLD  6952  orduninsuc  7028  fo1st  7173  fo2nd  7174  1st2val  7179  2nd2val  7180  eqer  7762  eqerOLD  7763  ener  7987  enerOLD  7988  ruv  8492  acncc  9247  grothac  9637  grothtsk  9642  hashneq0  13138  rexfiuz  14068  foo3  29272  signswch  30612  dfpo2  31620  domep  31672  fobigcup  31982  elhf2  32257  limsucncmpi  32419  bj-vjust  32761  bj-df-v  32991  uunT1  38827  nabctnabc  40861  clifte  40865  cliftet  40866  clifteta  40867  cliftetb  40868  confun5  40873  pldofph  40875  lco0  41981
  Copyright terms: Public domain W3C validator