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 484  xor 671  xor2 673  19.35 1075  sbco2d 1256  cbval2 1316  cbvex2 1317  cbvald 1320  equsb3 1330  elsb3 1331  sbcom2 1334  dfsb7 1340  2eu6 1454  eq2tr 1533  r19.35 1759  reeanv 1778  gencbvex 1838  gencbval 1840  2reuswap 1937  sbccomglem 1988  dfpss3 2134  difcom 2345  iunn0 2607  exss 2769  opabid 2810  rabxfr 2902  elxp2 3203  eqbrriv 3252  dm0rn0 3330  cnvi 3447  rninxp 3482  fununi 3563  fcoi1 3645  dfoprab2 3991  dfer2 4262  0nelqs 4298  eceqopreq 4313  xpsnen 4435  xpcomen 4439  xpassen 4441  rankuni 4698  kmlem4 4768  zorn2lem4 4791  alephislim 4883  distrlem5pr 5131  supsrlem5 5229  negcon1 5407  ltsubadd 5594  elfzp1 6510  sqr2irrlem4 6727  cjreb 6781  cau5 6919  cvganuz 6925  climcmplem 7137  geoser 7234  efcn 7423  hvsubadd 8933  chocuni 9172  omlsilem 9244  pjoml3 9529  hods 9701  nmopcoadj0 10036  pjin3 10122  eeeeanv 10436

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