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  3445  ab0orv  4342  pwv  4864  int0  4922  0iin  5023  dfpo2  6257  orduninsuc  7799  fo1st  7967  fo2nd  7968  1st2val  7975  2nd2val  7976  eqer  8684  ener  8949  ruv  9531  acncc  10369  grothac  10759  grothtsk  10764  hashneq0  14305  rexfiuz  15290  sa-abvi  32345  signswch  34525  satfdm  35329  fobigcup  35861  elhf2  36136  limsucncmpi  36406  bj-vjust  37016  ruvALT  42630  oaordnrex  43257  omnord1ex  43266  oenord1ex  43277  uunT1  44742  nabctnabc  46905  clifte  46909  cliftet  46910  clifteta  46911  cliftetb  46912  confun5  46917  pldofph  46919  icht  47426  lco0  48389  line2ylem  48713