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  vjust  3437  vn0  4292  pwv  4853  int0  4910  0iin  5010  dfpo2  6243  orduninsuc  7773  fo1st  7941  fo2nd  7942  1st2val  7949  2nd2val  7950  eqer  8658  ener  8923  ruv  9491  acncc  10331  grothac  10721  grothtsk  10726  hashneq0  14271  rexfiuz  15255  sa-abvi  32423  signswch  34574  satfdm  35413  fobigcup  35942  elhf2  36219  limsucncmpi  36489  bj-vjust  37099  ruvALT  42772  oaordnrex  43398  omnord1ex  43407  oenord1ex  43418  uunT1  44882  nabctnabc  47041  clifte  47045  cliftet  47046  clifteta  47047  cliftetb  47048  confun5  47053  pldofph  47055  icht  47562  lco0  48538  line2ylem  48862