Theorem 3bitr3 156

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 153	. 2 |- (ch <-> ps)
4		3bitr3.3	. 2 |- (ps <-> th)
5	3, 4	bitr 151	1 |- (ch <-> th)

Syntax hints:   <-> wb 127

This theorem is referenced by:  an12 370  xor 500  19.35 754  sbco2d 914  cbval2 974  cbvex2 975  cbvald 977  sb7 991  sbcom2 992  cleq2tr 1148  r19.35 1298  reeanv 1316  2reuswap 1341  gencbvex 1372  gencbval 1373  dfpss3 1558  exss 1881  pwpw0 1883  iunn0 2029  opabid 2099  elxp2 2443  dm0rn0 2549  cnvi 2634  fununi 2705  fcoi1 2765  dfoprab2 3021  er2 3201  0nelqs 3234  eceqopreq 3249  xpsnen 3339  xpcomen 3343  xpassen 3344  kmlem4 3583  alephislim 3688  distrlem5pr 3925  supsrlem5 4023  negcon1 4165  negne0 4379  nnwos 4610  sqr2irrlem4 4780  cjre 4811  hvsubadd 5038  chocuni 5179  omlsilem 5249  pjoml3 5496  hods 5606  pjin3 5648

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128

metamath.org