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

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  monothetic  269  2false  378  dftru2  1575  bitru  1579  sbt  2105  vjust  3455  vn0OLD  4295  pwv  4578  int0  4927  0iin  5027  dfpo2  6325  orduninsuc  7888  fo1st  8055  fo2nd  8056  1st2val  8063  2nd2val  8064  eqer  8792  ener  9066  ruv  9639  elhf2  9947  acncc  10557  grothac  10954  grothtsk  10959  hashneq0  14549  rexfiuz  15559  sa-abvi  33144  signswch  35301  satfdm  36342  fobigcup  36877  limsucncmpi  37448  bj-vjust  38240  ruvALT  43946  oaordnrex  44558  omnord1ex  44567  oenord1ex  44578  uunT1  46022  nabctnabc  48274  clifte  48278  cliftet  48279  clifteta  48280  cliftetb  48281  confun5  48286  pldofph  48288  icht  48807  lco0  49870  line2ylem  50194