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  3448  ab0orv  4346  pwv  4868  int0  4926  0iin  5028  dfpo2  6269  orduninsuc  7819  fo1st  7988  fo2nd  7989  1st2val  7996  2nd2val  7997  eqer  8707  ener  8972  ruv  9555  acncc  10393  grothac  10783  grothtsk  10788  hashneq0  14329  rexfiuz  15314  sa-abvi  32372  signswch  34552  satfdm  35356  fobigcup  35888  elhf2  36163  limsucncmpi  36433  bj-vjust  37043  ruvALT  42657  oaordnrex  43284  omnord1ex  43293  oenord1ex  43304  uunT1  44769  nabctnabc  46932  clifte  46936  cliftet  46937  clifteta  46938  cliftetb  46939  confun5  46944  pldofph  46946  icht  47453  lco0  48416  line2ylem  48740