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  32422  signswch  34545  satfdm  35349  fobigcup  35881  elhf2  36156  limsucncmpi  36426  bj-vjust  37036  ruvALT  42650  oaordnrex  43277  omnord1ex  43286  oenord1ex  43297  uunT1  44762  nabctnabc  46925  clifte  46929  cliftet  46930  clifteta  46931  cliftetb  46932  confun5  46937  pldofph  46939  icht  47446  lco0  48409  line2ylem  48733