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  1545  bitru  1549  vjust  3481  ab0orv  4383  pwv  4904  int0  4962  0iin  5064  dfpo2  6316  orduninsuc  7864  fo1st  8034  fo2nd  8035  1st2val  8042  2nd2val  8043  eqer  8781  ener  9041  ruv  9642  acncc  10480  grothac  10870  grothtsk  10875  hashneq0  14403  rexfiuz  15386  sa-abvi  32462  signswch  34576  satfdm  35374  fobigcup  35901  elhf2  36176  limsucncmpi  36446  bj-vjust  37056  ruvALT  42679  oaordnrex  43308  omnord1ex  43317  oenord1ex  43328  uunT1  44800  nabctnabc  46943  clifte  46947  cliftet  46948  clifteta  46949  cliftetb  46950  confun5  46955  pldofph  46957  icht  47439  lco0  48344  line2ylem  48672