Theorem 3bitr3i 338

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

Hypotheses

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

Assertion

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

Proof of Theorem 3bitr3i

Step	Hyp	Ref	Expression
1		3bitr3i.2	. . 3 |- (ph <-> ch)
2		3bitr3i.1	. . 3 |- (ph <-> ps)
3	1, 2	bitr3i 309	. 2 |- (ch <-> ps)
4		3bitr3i.3	. 2 |- (ps <-> th)
5	3, 4	bitri 306	1 |- (ch <-> th)

Syntax hints:   <-> wb 231

This theorem is referenced by:  pm4.78OLD 652  an12 901  an13OLD 907  xorOLD 1035  xor2OLD 1038  19.35 1741  sbco2d 1932  cbval2 1995  cbvex2 1996  equsb3 2011  sbcom2 2019  dfsb7 2024  sb7f 2025  2eu6 2146  eq2tri 2232  eqsb3 2268  r19.35 2509  2ralor 2526  ralcom4 2587  rexcom4 2588  ceqsralt 2592  gencbvex 2610  gencbval 2612  euind 2716  2reuswap 2726  reuind 2727  sbccomglem 2789  difcom 3187  sbss 3211  uniintsn 3466  exss 3711  elxp2 4184  elvvv 4219  eqbrriv 4246  dm0rn0 4330  rninxp 4499  fununi 4620  iunfopab 4677  dffv2 4859  dfoprab2 5051  dfer2 5520  0nelqs 5561  eceqopreq 5576  xpsnen 5701  xpcomen 5705  xpassen 5707  ordtypelem4 5962  rankuni 6110  cbvexsv 6146  alephislim 6230  kmlem4 6414  zorn2lem4 6438  distrlem5pr 6726  supsrlem5 6824  negcon1i 7162  elfzp1 8160  sqeqori 8393  sqr2irrlem4 8477  cjrebi 8531  cau5i 8672  cvganuzi 8678  climcmplem 8909  geoseri 9012  efcn 9204  isgrp2 9612  fbunfip 11278  hvsubaddi 11561  chocunii 11797  omlsilem 11869  pjoml3i 12152  hodsi 12328  nmopcoadj0i 12663  pjin3i 12756  bnj62 13378  bnj79 13384  bnj610 13493  bnj878 13734  bnj974 13788  bnj1050 13818  bnj1144 13870  bnj1306 13978  bnj1310 13979  bnj1492 14090  bnj594 14229  axfelem18 14963  eeeeanv 15233  negcmpprcal2 15237  ordtypelem4OLD 16463  2ralorOLD 16740  pm11.6 17434  isltrn2 18754

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 232

Copyright terms: Public domain