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  1546  bitru  1550  sbt  2071  vjust  3441  vn0  4297  pwv  4860  int0  4917  0iin  5019  dfpo2  6254  orduninsuc  7785  fo1st  7953  fo2nd  7954  1st2val  7961  2nd2val  7962  eqer  8671  ener  8938  ruv  9510  acncc  10350  grothac  10741  grothtsk  10746  hashneq0  14287  rexfiuz  15271  sa-abvi  32518  signswch  34718  satfdm  35563  fobigcup  36092  elhf2  36369  limsucncmpi  36639  bj-vjust  37256  ruvALT  42922  oaordnrex  43547  omnord1ex  43556  oenord1ex  43567  uunT1  45030  nabctnabc  47187  clifte  47191  cliftet  47192  clifteta  47193  cliftetb  47194  confun5  47199  pldofph  47201  icht  47708  lco0  48683  line2ylem  49007