Theorem 2th 718

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 2282  dfnul3 2283  pwv 2502  int0 2547  0iin 2606  orduninsuc 3114  dmi 3326  fo1st 4091  fo2nd 4092  1st2val 4095  2nd2val 4096  jech9.3 4666  nn0ltp1let 6127  efifolem2 8723  1ded 10671

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