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  1574  bitru  1578  sbt  2102  vjust  3451  vn0OLD  4291  pwv  4574  int0  4921  0iin  5021  dfpo2  6302  orduninsuc  7858  fo1st  8025  fo2nd  8026  1st2val  8033  2nd2val  8034  eqer  8762  ener  9036  ruv  9609  elhf2  9917  acncc  10525  grothac  10922  grothtsk  10927  hashneq0  14515  rexfiuz  15524  sa-abvi  33096  signswch  35240  satfdm  36252  fobigcup  36786  limsucncmpi  37357  bj-vjust  38106  ruvALT  43817  oaordnrex  44434  omnord1ex  44443  oenord1ex  44454  uunT1  45898  nabctnabc  48137  clifte  48141  cliftet  48142  clifteta  48143  cliftetb  48144  confun5  48149  pldofph  48151  icht  48670  lco0  49675  line2ylem  49999