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  378  dftru2  1572  bitru  1576  vjust  3464  vn0OLD  4307  pwv  4873  int0  4931  0iin  5032  dfpo2  6298  orduninsuc  7839  fo1st  8006  fo2nd  8007  1st2val  8014  2nd2val  8015  eqer  8731  ener  8998  ruv  9570  acncc  10424  grothac  10815  grothtsk  10820  hashneq0  14400  rexfiuz  15399  sa-abvi  32736  signswch  34893  satfdm  35760  fobigcup  36289  elhf2  36566  limsucncmpi  36845  bj-vjust  37579  ruvALT  43293  oaordnrex  43914  omnord1ex  43923  oenord1ex  43934  uunT1  45380  nabctnabc  47557  clifte  47561  cliftet  47562  clifteta  47563  cliftetb  47564  confun5  47569  pldofph  47571  icht  48090  lco0  49092  line2ylem  49416