Theorem 3bitr4ri 201

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

Hypotheses

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

Assertion

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

Proof of Theorem 3bitr4ri

Step	Hyp	Ref	Expression
1		3bitr4i.2	. 2 |- (ch <-> ph)
2		3bitr4i.1	. . 3 |- (ph <-> ps)
3		3bitr4i.3	. . 3 |- (th <-> ps)
4	2, 3	bitr4i 193	. 2 |- (ph <-> th)
5	1, 4	bitr2i 191	1 |- (th <-> ch)

Syntax hints:   <-> wb 163

This theorem is referenced by:  or12 278  dfbi3 733  nic-justbi 1234  nic-ax 1239  19.35 1426  2sb5 1725  2sb6 1726  2sb5rf 1728  2sb6rf 1729  moabs 1811  2eu4 1856  2eu7 1859  2eu8 1860  risset 2145  r19.23OLD 2207  r19.35 2231  rabid2OLD 2255  gencbvexOLD 2335  nssOLD 2671  ssequn1OLD 2776  unss 2780  difinOLD 2832  undif3 2854  unab 2859  inab 2861  difab 2863  ssundif 2955  euabsn 3095  snss 3122  pwpr 3174  unipr 3191  uni0b 3203  iinuni 3330  nssssOLD 3510  posn 3603  elxp2 4019  ralxpf 4043  opthprc 4046  xpsspw 4093  relun 4097  inopab 4108  dmres 4234  intirrOLD 4313  cnviOLD 4321  cnvsn 4373  imaco 4403  fvopab2 4754  fopab2 4796  fsn 4807  fparlem3 5083  fparlem4 5084  fsplit 5086  dfec2 5321  ecdmn0 5338  pw2en 5505  rankc1 5816  aceq1 5891  isinfcard 6035  infm3 7263  infmsup 7277  prime 7407  zmin 7432  elfzuzb 7646  crne0i 7989  reef11i 8673  efcnlem1 8684  tgss3 8908  clsval2 8961  islp2 9023  dfms2 9076  cncfmet 9183  axgroth6 10137  extbas1 10291  h1de2ctlem 11111  nonbooli 11231  5oalem7 11240  pjneli 11303  ho01i 11391  cvnbtwn3 11860  bnj345OLD 12188  bnj367OLD 12211  bnj14OLD 12382  bnj971 12860  bnj1087 12909  bnj1185 12967  bnj543 13269  bnj916 13332  divalgb 13707  untuni 13797  dffr5 13831  axfelem15 14045  anddi2 14268  elicc3 15362  opabex3 15701  iscring2 16146  prtlem70 16238  prtlem100 16244  n0el 16248  prtlem15 16281  prter2 16285  ishlat 17018

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