Theorem 3bitr4r 159

Description: A chained inference from transitive law for logical equivalence.

Hypotheses

Ref	Expression
3bitr4.1	|- (ph <-> ps)
3bitr4.2	|- (ch <-> ph)
3bitr4.3	|- (th <-> ps)

Assertion

Ref	Expression
3bitr4r	|- (th <-> ch)

Proof of Theorem 3bitr4r

Step	Hyp	Ref	Expression
1		3bitr4.2	. 2 |- (ch <-> ph)
2		3bitr4.1	. . 3 |- (ph <-> ps)
3		3bitr4.3	. . 3 |- (th <-> ps)
4	2, 3	bitr4 154	. 2 |- (ph <-> th)
5	1, 4	bitr2 152	1 |- (th <-> ch)

Syntax hints:   <-> wb 127

This theorem is referenced by:  or12 217  dfbi 499  biass 511  19.35 754  moabs 1041  risset 1235  r19.23v 1282  r19.35 1298  rabid2 1309  gencbvex 1372  nss 1550  ssequn1 1628  unss 1632  difin 1670  snss 1849  nssss 1866  eusn 1913  unpr 1930  uni0b 1939  iinuni 2036  dftr4 2046  elxp2 2443  opthprc 2457  xpex 2488  relun 2490  reluni 2493  inopab 2495  dmres 2584  intirr 2628  cnvi 2634  cnvsn 2636  fvopab2 2878  fopab2 2891  fsn 2895  ec2 3203  ecdmn0 3217  pw2en 3348  aceq1 3552  isinfcard 3692  zmin 4617  h1de2ctlem 5460  5oalem7 5550  pjnel 5665  cvnbtwn3t 5720

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

This theorem depends on definitions:  df-bi 128

metamath.org