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  374  dftru2  1538  bitru  1542  vjust  3462  dfnul3OLD  4328  ab0orv  4380  pwv  4906  int0  4966  0iin  5068  dfpo2  6302  orduninsuc  7848  fo1st  8014  fo2nd  8015  1st2val  8022  2nd2val  8023  eqer  8760  ener  9022  ruv  9627  acncc  10465  grothac  10855  grothtsk  10860  hashneq0  14359  rexfiuz  15330  sa-abvi  32325  signswch  34324  satfdm  35110  fobigcup  35627  elhf2  35902  limsucncmpi  36060  bj-vjust  36665  ruvALT  42228  oaordnrex  42866  omnord1ex  42875  oenord1ex  42886  uunT1  44361  nabctnabc  46451  clifte  46455  cliftet  46456  clifteta  46457  cliftetb  46458  confun5  46463  pldofph  46465  icht  46929  lco0  47681  line2ylem  48010