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 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  266  2false  376  dftru2  1547  bitru  1551  vjust  3476  dfnul3OLD  4328  ab0orv  4378  pwv  4905  int0  4966  0iin  5067  dfpo2  6293  orduninsuc  7829  fo1st  7992  fo2nd  7993  1st2val  8000  2nd2val  8001  eqer  8735  ener  8994  ruv  9594  acncc  10432  grothac  10822  grothtsk  10827  hashneq0  14321  rexfiuz  15291  sa-abvi  31684  signswch  33561  satfdm  34349  fobigcup  34861  elhf2  35136  limsucncmpi  35319  bj-vjust  35925  ruvALT  41017  oaordnrex  42031  omnord1ex  42040  oenord1ex  42051  uunT1  43527  nabctnabc  45628  clifte  45632  cliftet  45633  clifteta  45634  cliftetb  45635  confun5  45640  pldofph  45642  icht  46107  lco0  47062  line2ylem  47391