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  3443  vn0  4299  pwv  4862  int0  4919  0iin  5021  dfpo2  6262  orduninsuc  7795  fo1st  7963  fo2nd  7964  1st2val  7971  2nd2val  7972  eqer  8682  ener  8950  ruv  9522  acncc  10362  grothac  10753  grothtsk  10758  hashneq0  14299  rexfiuz  15283  sa-abvi  32531  signswch  34739  satfdm  35585  fobigcup  36114  elhf2  36391  limsucncmpi  36661  bj-vjust  37303  ruvALT  43027  oaordnrex  43652  omnord1ex  43661  oenord1ex  43672  uunT1  45135  nabctnabc  47291  clifte  47295  cliftet  47296  clifteta  47297  cliftetb  47298  confun5  47303  pldofph  47305  icht  47812  lco0  48787  line2ylem  49111