Theorem 2th 254

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

Syntax hints:   ↔ wb 196

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 197

This theorem is referenced by:  2false  364  trujust  1632  dftru2  1638  bitru  1643  vjust  3339  dfnul2  4058  dfnul3  4059  rab0OLD  4097  pwv  4583  int0  4640  int0OLD  4641  0iin  4728  snnexOLD  7130  orduninsuc  7206  fo1st  7351  fo2nd  7352  1st2val  7359  2nd2val  7360  eqer  7944  ener  8166  ruv  8670  acncc  9452  grothac  9842  grothtsk  9847  hashneq0  13345  rexfiuz  14284  foo3  29609  signswch  30945  dfpo2  31950  domep  32001  fobigcup  32311  elhf2  32586  limsucncmpi  32748  bj-vjust  33090  bj-df-v  33320  uunT1  39507  nabctnabc  41602  clifte  41606  cliftet  41607  clifteta  41608  cliftetb  41609  confun5  41614  pldofph  41616  lco0  42724