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

Theorem 2th 265
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 210 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 207
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 208
This theorem is referenced by:  monothetic  267  2false  377  dftru2  1533  bitru  1537  vjust  3493  dfnul2OLD  4291  dfnul3  4292  pwv  4827  int0  4881  0iin  4978  domepOLD  5787  orduninsuc  7547  fo1st  7698  fo2nd  7699  1st2val  7706  2nd2val  7707  eqer  8313  ener  8544  ruv  9054  acncc  9850  grothac  10240  grothtsk  10245  hashneq0  13713  rexfiuz  14695  sa-abvi  30147  signswch  31730  satfdm  32513  dfpo2  32888  fobigcup  33258  elhf2  33533  limsucncmpi  33690  bj-df-v  34241  uunT1  40991  nabctnabc  43044  clifte  43048  cliftet  43049  clifteta  43050  cliftetb  43051  confun5  43056  pldofph  43058  lco0  44410  line2ylem  44666
  Copyright terms: Public domain W3C validator