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  3451  ab0orv  4349  pwv  4871  int0  4929  0iin  5031  dfpo2  6272  orduninsuc  7822  fo1st  7991  fo2nd  7992  1st2val  7999  2nd2val  8000  eqer  8710  ener  8975  ruv  9562  acncc  10400  grothac  10790  grothtsk  10795  hashneq0  14336  rexfiuz  15321  sa-abvi  32379  signswch  34559  satfdm  35363  fobigcup  35895  elhf2  36170  limsucncmpi  36440  bj-vjust  37050  ruvALT  42664  oaordnrex  43291  omnord1ex  43300  oenord1ex  43311  uunT1  44776  nabctnabc  46936  clifte  46940  cliftet  46941  clifteta  46942  cliftetb  46943  confun5  46948  pldofph  46950  icht  47457  lco0  48420  line2ylem  48744