Theorem 2th 254

Description: Two truths are equivalent. (Contributed by NM, 18-Aug-1993.)

Hypotheses

Ref	Expression
2th.1	|- ph
2th.2	|- ps

Assertion

Ref	Expression
2th	|- ( ph <-> ps )

Proof of Theorem 2th

Step	Hyp	Ref	Expression
1		2th.2	. . 3 |- ps
2	1	a1i 11	. 2 |- ( ph -> ps )
3		2th.1	. . 3 |- ph
4	3	a1i 11	. 2 |- ( ps -> ph )
5	2, 4	impbii 199	1 |- ( ph <-> ps )

Syntax hints:   <-> wb 196

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 197

This theorem is referenced by:  2false  365  trujust  1485  dftru2  1491  bitru  1496  vjust  3201  dfnul2  3917  dfnul3  3918  rab0OLD  3956  pwv  4433  int0  4490  int0OLD  4491  0iin  4578  snnexOLD  6967  orduninsuc  7043  fo1st  7188  fo2nd  7189  1st2val  7194  2nd2val  7195  eqer  7777  eqerOLD  7778  ener  8002  enerOLD  8003  ruv  8507  acncc  9262  grothac  9652  grothtsk  9657  hashneq0  13155  rexfiuz  14087  foo3  29302  signswch  30638  dfpo2  31645  domep  31698  fobigcup  32007  elhf2  32282  limsucncmpi  32444  bj-vjust  32786  bj-df-v  33016  uunT1  39007  nabctnabc  41098  clifte  41102  cliftet  41103  clifteta  41104  cliftetb  41105  confun5  41110  pldofph  41112  lco0  42216