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  3437  ab0orv  4334  pwv  4855  int0  4912  0iin  5013  dfpo2  6244  orduninsuc  7776  fo1st  7944  fo2nd  7945  1st2val  7952  2nd2val  7953  eqer  8661  ener  8926  ruv  9497  acncc  10334  grothac  10724  grothtsk  10729  hashneq0  14271  rexfiuz  15255  sa-abvi  32387  signswch  34529  satfdm  35346  fobigcup  35878  elhf2  36153  limsucncmpi  36423  bj-vjust  37033  ruvALT  42646  oaordnrex  43272  omnord1ex  43281  oenord1ex  43292  uunT1  44757  nabctnabc  46919  clifte  46923  cliftet  46924  clifteta  46925  cliftetb  46926  confun5  46931  pldofph  46933  icht  47440  lco0  48416  line2ylem  48740