Theorem 2th 786

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

Syntax hints:   <-> wb 163

This theorem is referenced by:  vjust 2293  dfnul2 2877  dfnul3 2878  rab0 2894  pwv 3176  int0 3230  0iin 3313  snnex 3801  orduninsuc 3925  dmiOLD 4173  fo1st 5032  fo2nd 5033  1st2val 5038  2nd2val 5039  ruv 5704  jech9.3 5777  nn0ltp1le 7336  efifolem2 10077  foo3 12015  domep 13861  TFAid 14107  FTAid 14108  TFOid 14111  FTOid 14112  TTIid 14114  FTIid 14116  FFIid 14117  inpc 14619  1ded 15085  pm11.07 16321

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 164

Copyright terms: Public domain