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  1546  bitru  1550  sbt  2071  vjust  3439  vn0  4295  pwv  4858  int0  4915  0iin  5017  dfpo2  6252  orduninsuc  7783  fo1st  7951  fo2nd  7952  1st2val  7959  2nd2val  7960  eqer  8669  ener  8936  ruv  9508  acncc  10348  grothac  10739  grothtsk  10744  hashneq0  14285  rexfiuz  15269  sa-abvi  32467  signswch  34667  satfdm  35512  fobigcup  36041  elhf2  36318  limsucncmpi  36588  bj-vjust  37199  ruvALT  42854  oaordnrex  43479  omnord1ex  43488  oenord1ex  43499  uunT1  44962  nabctnabc  47119  clifte  47123  cliftet  47124  clifteta  47125  cliftetb  47126  confun5  47131  pldofph  47133  icht  47640  lco0  48615  line2ylem  48939