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  3479  ab0orv  4389  pwv  4909  int0  4967  0iin  5069  dfpo2  6318  orduninsuc  7864  fo1st  8033  fo2nd  8034  1st2val  8041  2nd2val  8042  eqer  8780  ener  9040  ruv  9640  acncc  10478  grothac  10868  grothtsk  10873  hashneq0  14400  rexfiuz  15383  sa-abvi  32472  signswch  34555  satfdm  35354  fobigcup  35882  elhf2  36157  limsucncmpi  36428  bj-vjust  37038  ruvALT  42656  oaordnrex  43285  omnord1ex  43294  oenord1ex  43305  uunT1  44778  nabctnabc  46881  clifte  46885  cliftet  46886  clifteta  46887  cliftetb  46888  confun5  46893  pldofph  46895  icht  47377  lco0  48273  line2ylem  48601