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

Theorem 2th 264
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 209 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 206
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 207
This theorem is referenced by:  monothetic  266  2false  375  dftru2  1545  bitru  1549  vjust  3481  ab0orv  4383  pwv  4904  int0  4962  0iin  5064  dfpo2  6316  orduninsuc  7864  fo1st  8034  fo2nd  8035  1st2val  8042  2nd2val  8043  eqer  8781  ener  9041  ruv  9642  acncc  10480  grothac  10870  grothtsk  10875  hashneq0  14403  rexfiuz  15386  sa-abvi  32462  signswch  34576  satfdm  35374  fobigcup  35901  elhf2  36176  limsucncmpi  36446  bj-vjust  37056  ruvALT  42679  oaordnrex  43308  omnord1ex  43317  oenord1ex  43328  uunT1  44800  nabctnabc  46943  clifte  46947  cliftet  46948  clifteta  46949  cliftetb  46950  confun5  46955  pldofph  46957  icht  47439  lco0  48344  line2ylem  48672
  Copyright terms: Public domain W3C validator