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  1575  bitru  1579  sbt  2100  vjust  3456  vn0OLD  4299  pwv  4869  int0  4927  0iin  5028  dfpo2  6297  orduninsuc  7835  fo1st  8002  fo2nd  8003  1st2val  8010  2nd2val  8011  eqer  8727  ener  8994  ruv  9566  acncc  10419  grothac  10810  grothtsk  10815  hashneq0  14396  rexfiuz  15395  sa-abvi  32795  signswch  34948  satfdm  35861  fobigcup  36390  elhf2  36667  limsucncmpi  36976  bj-vjust  37711  ruvALT  43421  oaordnrex  44042  omnord1ex  44051  oenord1ex  44062  uunT1  45508  nabctnabc  47688  clifte  47692  cliftet  47693  clifteta  47694  cliftetb  47695  confun5  47700  pldofph  47702  icht  48221  lco0  49227  line2ylem  49551