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  dfbi 668  19.35 1071  2sb5 1330  2sb6 1331  2sb5rf 1333  2sb6rf 1334  moabs 1408  2eu4 1445  2eu7 1448  2eu8 1449  risset 1677  r19.23v 1733  r19.35 1751  rabid2 1762  gencbvex 1829  nss 2103  ssequn1 2190  unss 2194  difin 2235  ssundif 2334  eusn 2436  snss 2452  unipr 2505  uni0b 2513  iinuni 2605  dftr4 2675  nssss 2754  elxp2 3193  ralxpf 3210  opthprc 3211  xpsspw 3247  relun 3251  reluni 3255  inopab 3258  dmres 3364  intirr 3427  cnvi 3433  cnvsn 3435  imaco 3487  fvopab2 3776  fopab2 3808  fsn 3819  dfoprab5 4099  dfec2 4248  ecdmn0 4264  pw2en 4426  rankc1 4677  aceq1 4701  isinfcard 4859  infm3 6001  infmsup 6015  primet 6142  zmin 6167  elfzuzb 6408  crne0 6670  reef11 7349  efcnlem1 7359  tgss3t 7580  clsval2 7627  islp2 7688  dfms2 7738  cncfmet 7844  h1de2ctlem 9394  nonbool 9513  5oalem7 9522  pjnel 9585  ho01 9671  cvnbtwn3t 10125

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