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  1542  bitru  1546  vjust  3489  dfnul3OLD  4358  ab0orv  4406  pwv  4928  int0  4986  0iin  5087  dfpo2  6327  orduninsuc  7880  fo1st  8050  fo2nd  8051  1st2val  8058  2nd2val  8059  eqer  8799  ener  9061  ruv  9671  acncc  10509  grothac  10899  grothtsk  10904  hashneq0  14413  rexfiuz  15396  sa-abvi  32475  signswch  34538  satfdm  35337  fobigcup  35864  elhf2  36139  limsucncmpi  36411  bj-vjust  37021  ruvALT  42624  oaordnrex  43257  omnord1ex  43266  oenord1ex  43277  uunT1  44751  nabctnabc  46846  clifte  46850  cliftet  46851  clifteta  46852  cliftetb  46853  confun5  46858  pldofph  46860  icht  47326  lco0  48156  line2ylem  48485