Theorem 2th 264

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

Syntax hints:   ↔ wb 205

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 206

This theorem is referenced by:  monothetic  266  2false  376  dftru2  1547  bitru  1551  vjust  3476  dfnul3OLD  4329  ab0orv  4379  pwv  4906  int0  4967  0iin  5068  dfpo2  6296  orduninsuc  7832  fo1st  7995  fo2nd  7996  1st2val  8003  2nd2val  8004  eqer  8738  ener  8997  ruv  9597  acncc  10435  grothac  10825  grothtsk  10830  hashneq0  14324  rexfiuz  15294  sa-abvi  31696  signswch  33572  satfdm  34360  fobigcup  34872  elhf2  35147  limsucncmpi  35330  bj-vjust  35936  ruvALT  41411  oaordnrex  42045  omnord1ex  42054  oenord1ex  42065  uunT1  43541  nabctnabc  45641  clifte  45645  cliftet  45646  clifteta  45647  cliftetb  45648  confun5  45653  pldofph  45655  icht  46120  lco0  47108  line2ylem  47437