Theorem 2th 263

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

Syntax hints:   ↔ wb 205

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 206

This theorem is referenced by:  monothetic  265  2false  376  dftru2  1544  bitru  1548  vjust  3433  dfnul3OLD  4262  ab0orv  4312  pwv  4836  int0  4893  0iin  4993  domepOLD  5833  dfpo2  6199  orduninsuc  7690  fo1st  7851  fo2nd  7852  1st2val  7859  2nd2val  7860  eqer  8533  ener  8787  ruv  9361  acncc  10196  grothac  10586  grothtsk  10591  hashneq0  14079  rexfiuz  15059  sa-abvi  30805  signswch  32540  satfdm  33331  fobigcup  34202  elhf2  34477  limsucncmpi  34634  bj-vjust  35226  ruvALT  40168  uunT1  42400  nabctnabc  44426  clifte  44430  cliftet  44431  clifteta  44432  cliftetb  44433  confun5  44438  pldofph  44440  icht  44904  lco0  45768  line2ylem  46097