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  3460  ab0orv  4358  pwv  4880  int0  4938  0iin  5040  dfpo2  6285  orduninsuc  7838  fo1st  8008  fo2nd  8009  1st2val  8016  2nd2val  8017  eqer  8755  ener  9015  ruv  9616  acncc  10454  grothac  10844  grothtsk  10849  hashneq0  14382  rexfiuz  15366  sa-abvi  32424  signswch  34593  satfdm  35391  fobigcup  35918  elhf2  36193  limsucncmpi  36463  bj-vjust  37073  ruvALT  42692  oaordnrex  43319  omnord1ex  43328  oenord1ex  43339  uunT1  44804  nabctnabc  46960  clifte  46964  cliftet  46965  clifteta  46966  cliftetb  46967  confun5  46972  pldofph  46974  icht  47466  lco0  48403  line2ylem  48731