Theorem 3bitr3 181

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

Hypotheses

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

Assertion

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

Proof of Theorem 3bitr3

Step	Hyp	Ref	Expression
1		3bitr3.2	. . 3 |- (ph <-> ch)
2		3bitr3.1	. . 3 |- (ph <-> ps)
3	1, 2	bitr3 175	. 2 |- (ch <-> ps)
4		3bitr3.3	. 2 |- (ps <-> th)
5	3, 4	bitr 173	1 |- (ch <-> th)

Syntax hints:   <-> wb 146

This theorem is referenced by:  pm4.78 354  an12 483  xor 669  xor2 671  19.35 1071  sbco2d 1251  cbval2 1311  cbvex2 1312  cbvald 1315  equsb3 1325  elsb3 1326  sbcom2 1329  dfsb7 1335  2eu6 1447  eq2tr 1525  r19.35 1751  reeanv 1770  gencbvex 1829  gencbval 1831  2reuswap 1927  sbccomglem 1978  dfpss3 2124  difcom 2335  iunn0 2597  exss 2759  opabid 2799  rabxfr 2892  elxp2 3193  eqbrriv 3242  dm0rn0 3319  cnvi 3433  rninxp 3468  fununi 3549  fcoi1 3630  dfoprab2 3976  dfer2 4246  0nelqs 4282  eceqopreq 4297  xpsnen 4415  xpcomen 4419  xpassen 4421  rankuni 4670  kmlem4 4740  zorn2lem4 4763  alephislim 4855  distrlem5pr 5103  supsrlem5 5201  negcon1 5379  ltsubadd 5568  elfzp1 6442  sqr2irrlem4 6657  cjreb 6716  cau5 6856  cvganuz 6862  climcmplem 7073  geoser 7169  efcn 7363  hvsubadd 8854  chocuni 9088  omlsilem 9159  pjoml3 9446  hods 9618  pjin3 10032  eeeeanv 10336

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