Theorem 3bitr2i 195

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

Hypotheses

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

Assertion

Ref	Expression
3bitr2i	|- (ph <-> th)

Proof of Theorem 3bitr2i

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

Syntax hints:   <-> wb 162

This theorem is referenced by:  pm5.17 728  2eu5 1694  2eu6 1695  exists1 1699  euxfr 2271  rmo4 2278  sspsstri 2543  difin 2658  symdif2OLD 2684  sbssOLD 2805  ssiinOLD 3124  dftr5 3232  pwundif 3394  posn 3418  uniuni 3617  eufromeq4 3642  eufromeq6 3644  reldm0 3987  imadisj 4096  elinisegOLD 4106  asymref2OLD 4122  intirr 4123  dfco2aOLD 4206  resco 4213  funcnv2 4285  funcnv3 4287  fncnv 4290  fun11 4291  fununi 4292  iunfopab 4353  fsn 4618  fnoprv 4757  fparlem1 4892  fparlem2 4893  fparlem3 4894  fparlem4 4895  ixp0x 5229  mapsnen 5299  kmlem4 5726  kmlem12 5734  kmlem14 5736  kmlem15 5737  kmlem16 5738  ltexprlem4 6093  infcvglem1 8277  eirrlem1 8446  ruclem2 8575  istps3 8672  axgroth4 9934  grothprim 9936  dford2 9973  pjtheui 10660  adjbd1o 11447  bnj33OLD 12194  bnj136 12260  bnj134 12270  bnj861 12586  bnj962 12648  bnj1144 12733  bnj1163 12747  bnj1533 12974  bnj849 13110  bnj983 13149  bnj1049 13186  bnj1070 13193  bnj1174 13234  bnj1284 13274  isprm2 13567  axacprim 13583  fundmpss 13629  frxp 13743  wfrlem8 13756  axfelem11 13831  andnand1 13878  and4com 13997  elicc3 15044  compfipin0 15118  is1stc3 15151  ufileu 15255  rnelfmlem 15274  prtlem70 15920  strdif 16478

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 163

Copyright terms: Public domain