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

Syntax hints:   ↔ wb 209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210

This theorem is referenced by:  monothetic  269  2false  378  dftru2  1572  bitru  1576  vjust  3462  vn0OLD  4305  pwv  4871  int0  4929  0iin  5030  dfpo2  6298  orduninsuc  7839  fo1st  8006  fo2nd  8007  1st2val  8014  2nd2val  8015  eqer  8731  ener  8998  ruv  9570  acncc  10424  grothac  10815  grothtsk  10820  hashneq0  14400  rexfiuz  15399  sa-abvi  32736  signswch  34893  satfdm  35794  fobigcup  36323  elhf2  36600  limsucncmpi  36879  bj-vjust  37614  ruvALT  43328  oaordnrex  43949  omnord1ex  43958  oenord1ex  43969  uunT1  45415  nabctnabc  47592  clifte  47596  cliftet  47597  clifteta  47598  cliftetb  47599  confun5  47604  pldofph  47606  icht  48125  lco0  49127  line2ylem  49451