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  2103  vjust  3458  vn0OLD  4299  pwv  4871  int0  4929  0iin  5030  dfpo2  6301  orduninsuc  7845  fo1st  8012  fo2nd  8013  1st2val  8020  2nd2val  8021  eqer  8737  ener  9004  ruv  9577  acncc  10439  grothac  10832  grothtsk  10837  hashneq0  14420  rexfiuz  15425  sa-abvi  32868  signswch  35015  satfdm  35900  fobigcup  36429  elhf2  36706  limsucncmpi  37015  bj-vjust  37750  ruvALT  43461  oaordnrex  44082  omnord1ex  44091  oenord1ex  44102  uunT1  45548  nabctnabc  47728  clifte  47732  cliftet  47733  clifteta  47734  cliftetb  47735  confun5  47740  pldofph  47742  icht  48261  lco0  49266  line2ylem  49590