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  3452  vn0OLD  4292  pwv  4864  int0  4922  0iin  5022  dfpo2  6299  orduninsuc  7854  fo1st  8021  fo2nd  8022  1st2val  8029  2nd2val  8030  eqer  8754  ener  9028  ruv  9602  elhf2  9910  acncc  10518  grothac  10915  grothtsk  10920  hashneq0  14508  rexfiuz  15515  sa-abvi  33045  signswch  35190  satfdm  36134  fobigcup  36662  limsucncmpi  37233  bj-vjust  37970  ruvALT  43680  oaordnrex  44296  omnord1ex  44305  oenord1ex  44316  uunT1  45761  nabctnabc  48000  clifte  48004  cliftet  48005  clifteta  48006  cliftetb  48007  confun5  48012  pldofph  48014  icht  48533  lco0  49538  line2ylem  49862