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 669  19.35 1073  2sb5 1333  2sb6 1334  2sb5rf 1336  2sb6rf 1337  moabs 1413  2eu4 1450  2eu7 1453  2eu8 1454  risset 1682  r19.23v 1738  r19.35 1756  rabid2 1767  gencbvex 1834  nss 2109  ssequn1 2196  unss 2200  difin 2241  ssundif 2340  eusn 2442  snss 2457  unipr 2510  uni0b 2518  iinuni 2610  dftr4 2680  nssss 2759  elxp2 3198  ralxpf 3215  opthprc 3216  xpsspw 3252  relun 3256  reluni 3260  inopab 3263  dmres 3372  intirr 3433  cnvi 3439  cnvsn 3441  imaco 3493  fvopab2 3782  fopab2 3814  fsn 3825  dfoprab5 4105  dfec2 4254  ecdmn0 4270  pw2en 4432  rankc1 4685  aceq1 4709  isinfcard 4867  infm3 6009  infmsup 6023  primet 6150  zmin 6175  elfzuzb 6416  crne0 6678  reef11 7357  efcnlem1 7367  tgss3t 7588  clsval2 7635  islp2 7697  dfms2 7749  cncfmet 7857  h1de2ctlem 9417  nonbool 9536  5oalem7 9545  pjnel 9608  ho01 9694  cvnbtwn3t 10153

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