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  3451  vn0OLD  4292  pwv  4864  int0  4922  0iin  5022  dfpo2  6294  orduninsuc  7840  fo1st  8007  fo2nd  8008  1st2val  8015  2nd2val  8016  eqer  8734  ener  9008  ruv  9581  acncc  10443  grothac  10840  grothtsk  10845  hashneq0  14429  rexfiuz  15436  sa-abvi  32925  signswch  35070  satfdm  35949  fobigcup  36478  elhf2  36756  limsucncmpi  37065  bj-vjust  37800  ruvALT  43516  oaordnrex  44137  omnord1ex  44146  oenord1ex  44157  uunT1  45603  nabctnabc  47820  clifte  47824  cliftet  47825  clifteta  47826  cliftetb  47827  confun5  47832  pldofph  47834  icht  48353  lco0  49358  line2ylem  49682