Theorem 2th 256

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

Syntax hints:   ↔ wb 198

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 199

This theorem is referenced by:  monothetic  258  2false  367  trujustOLD  1661  dftru2  1664  bitru  1668  vjust  3415  dfnul2  4146  dfnul3  4147  pwv  4655  int0  4711  0iin  4798  orduninsuc  7304  fo1st  7448  fo2nd  7449  1st2val  7456  2nd2val  7457  eqer  8044  ener  8269  ruv  8776  acncc  9577  grothac  9967  grothtsk  9972  hashneq0  13445  rexfiuz  14464  sa-abvi  29857  signswch  31185  dfpo2  32187  domep  32236  fobigcup  32546  elhf2  32821  limsucncmpi  32977  bj-vjust  33311  bj-df-v  33538  uunT1  39834  nabctnabc  41892  clifte  41896  cliftet  41897  clifteta  41898  cliftetb  41899  confun5  41904  pldofph  41906  lco0  43063  line2ylem  43303