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

Step	Hyp	Ref	Expression
1		2th.2	. . 3 ⊢ 𝜓
2	1	a1i 11	. 2 ⊢ (𝜑 → 𝜓)
3		2th.1	. . 3 ⊢ 𝜑
4	3	a1i 11	. 2 ⊢ (𝜓 → 𝜑)
5	2, 4	impbii 209	1 ⊢ (𝜑 ↔ 𝜓)

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  1547  bitru  1551  sbt  2072  vjust  3430  vn0  4285  pwv  4847  int0  4904  0iin  5006  dfpo2  6260  orduninsuc  7794  fo1st  7962  fo2nd  7963  1st2val  7970  2nd2val  7971  eqer  8680  ener  8948  ruv  9522  acncc  10362  grothac  10753  grothtsk  10758  hashneq0  14326  rexfiuz  15310  sa-abvi  32514  signswch  34705  satfdm  35551  fobigcup  36080  elhf2  36357  limsucncmpi  36627  bj-vjust  37362  ruvALT  43102  oaordnrex  43723  omnord1ex  43732  oenord1ex  43743  uunT1  45206  nabctnabc  47379  clifte  47383  cliftet  47384  clifteta  47385  cliftetb  47386  confun5  47391  pldofph  47393  icht  47912  lco0  48903  line2ylem  49227