Theorem 2th 730

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	impbii 164	1 |- (ph <-> ps)

Syntax hints:   <-> wb 153

This theorem is referenced by:  dfnul2 2333  dfnul3 2334  pwv 2556  int0 2601  0iin 2660  snnex 2933  orduninsuc 3171  dmi 3383  snnexOLD 3933  fo1st 4149  fo2nd 4150  1st2val 4153  2nd2val 4154  fiprlemOLD 4494  ruv 4661  jech9.3 4728  nn0ltp1le 6209  efifolem2 8806  foo3 10454  inpc 10577  1ded 10753

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 154

Copyright terms: Public domain