Theorem 2th 267

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

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  monothetic  269  2false  379  dftru2  1543  bitru  1547  vjust  3442  dfnul3  4246  pwv  4797  int0  4852  0iin  4950  domepOLD  5758  orduninsuc  7538  fo1st  7691  fo2nd  7692  1st2val  7699  2nd2val  7700  eqer  8307  ener  8539  ruv  9050  acncc  9851  grothac  10241  grothtsk  10246  hashneq0  13721  rexfiuz  14699  sa-abvi  30226  signswch  31941  satfdm  32729  dfpo2  33104  fobigcup  33474  elhf2  33749  limsucncmpi  33906  bj-df-v  34471  uunT1  41486  nabctnabc  43524  clifte  43528  cliftet  43529  clifteta  43530  cliftetb  43531  confun5  43536  pldofph  43538  icht  43969  lco0  44836  line2ylem  45165