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  3431  vn0  4286  pwv  4848  int0  4905  0iin  5007  dfpo2  6255  orduninsuc  7788  fo1st  7956  fo2nd  7957  1st2val  7964  2nd2val  7965  eqer  8674  ener  8942  ruv  9516  acncc  10356  grothac  10747  grothtsk  10752  hashneq0  14320  rexfiuz  15304  sa-abvi  32532  signswch  34724  satfdm  35570  fobigcup  36099  elhf2  36376  limsucncmpi  36646  bj-vjust  37381  ruvALT  43119  oaordnrex  43744  omnord1ex  43753  oenord1ex  43764  uunT1  45227  nabctnabc  47394  clifte  47398  cliftet  47399  clifteta  47400  cliftetb  47401  confun5  47406  pldofph  47408  icht  47927  lco0  48918  line2ylem  49242