Theorem 2th 717

Description: Two truths are equivalent.

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 8	. 2 |- (ph -> ps)
3		2th.1	. . 3 |- ph
4	3	a1i 8	. 2 |- (ps -> ph)
5	2, 4	impbi 157	1 |- (ph <-> ps)

Syntax hints:   <-> wb 146

This theorem is referenced by:  dfnul2 2278  dfnul3 2279  pwv 2497  int0 2542  0iin 2601  orduninsuc 3109  dmi 3321  fo1st 4081  fo2nd 4082  1st2val 4085  2nd2val 4086  jech9.3 4646  nn0ltp1let 6082  efifolem2 8657  1ded 10551

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

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain