Theorem 2th 265

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 210	1 ⊢ (𝜑 ↔ 𝜓)

Syntax hints:   ↔ wb 207

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 208

This theorem is referenced by:  monothetic  267  2false  376  dftru2  1552  bitru  1556  sbt  2077  vjust  3432  vn0  4273  pwv  4835  int0  4892  0iin  4993  dfpo2  6247  orduninsuc  7783  fo1st  7951  fo2nd  7952  1st2val  7959  2nd2val  7960  eqer  8670  ener  8938  ruv  9513  acncc  10353  grothac  10744  grothtsk  10749  hashneq0  14317  rexfiuz  15301  sa-abvi  32532  signswch  34745  satfdm  35597  fobigcup  36126  elhf2  36403  limsucncmpi  36673  bj-vjust  37408  ruvALT  43119  oaordnrex  43740  omnord1ex  43749  oenord1ex  43760  uunT1  45223  nabctnabc  47394  clifte  47398  cliftet  47399  clifteta  47400  cliftetb  47401  confun5  47406  pldofph  47408  icht  47927  lco0  48918  line2ylem  49242