Theorem 2th 266

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 211	1 ⊢ (𝜑 ↔ 𝜓)

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  monothetic  268  2false  377  dftru2  1565  bitru  1569  vjust  3455  vn0  4297  pwv  4862  int0  4920  0iin  5021  dfpo2  6283  orduninsuc  7823  fo1st  7990  fo2nd  7991  1st2val  7998  2nd2val  7999  eqer  8715  ener  8982  ruv  9556  acncc  10397  grothac  10788  grothtsk  10793  hashneq0  14377  rexfiuz  15375  sa-abvi  32646  signswch  34855  satfdm  35719  fobigcup  36248  elhf2  36525  limsucncmpi  36805  bj-vjust  37540  ruvALT  43251  oaordnrex  43872  omnord1ex  43881  oenord1ex  43892  uunT1  45355  nabctnabc  47525  clifte  47529  cliftet  47530  clifteta  47531  cliftetb  47532  confun5  47537  pldofph  47539  icht  48058  lco0  49049  line2ylem  49373