Theorem 3bitr4r 184

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 176	. 2 |- (ph <-> th)
5	1, 4	bitr2 174	1 |- (th <-> ch)

Syntax hints:   <-> wb 146

This theorem is referenced by:  or12 258  dfbi3 670  19.35 1075  2sb5 1335  2sb6 1336  2sb5rf 1338  2sb6rf 1339  moabs 1415  2eu4 1452  2eu7 1455  2eu8 1456  risset 1685  r19.23v 1741  r19.35 1759  rabid2 1770  gencbvex 1838  nss 2113  ssequn1 2200  unss 2204  difin 2245  ssundif 2344  eusn 2446  snss 2461  unipr 2515  uni0b 2523  iinuni 2615  dftr4 2685  nssss 2764  elxp2 3203  ralxpf 3220  opthprc 3221  xpsspw 3257  relun 3261  reluni 3265  inopab 3268  dmres 3380  intirr 3441  cnvi 3447  cnvsn 3449  imaco 3501  fvopab2 3791  fopab2 3823  fsn 3834  dfoprab5 4115  dfec2 4264  ecdmn0 4280  pw2en 4446  rankc1 4705  aceq1 4729  isinfcard 4887  infm3 6054  infmsup 6068  primet 6195  zmin 6219  elfzuzb 6476  crne0 6739  reef11 7408  efcnlem1 7419  tgss3t 7638  clsval2 7685  islp2 7747  dfms2 7799  cncfmet 7905  h1de2ctlem 9478  nonbool 9596  5oalem7 9605  pjnel 9668  ho01 9754  cvnbtwn3t 10215

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