Theorem 3bitr3 181

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

Hypotheses

Ref	Expression
3bitr3.1	⊢ (φ ↔ ψ)
3bitr3.2	⊢ (φ ↔ χ)
3bitr3.3	⊢ (ψ ↔ θ)

Assertion

Ref	Expression
3bitr3	⊢ (χ ↔ θ)

Proof of Theorem 3bitr3

Step	Hyp	Ref	Expression
1		3bitr3.2	. . 3 ⊢ (φ ↔ χ)
2		3bitr3.1	. . 3 ⊢ (φ ↔ ψ)
3	1, 2	bitr3 175	. 2 ⊢ (χ ↔ ψ)
4		3bitr3.3	. 2 ⊢ (ψ ↔ θ)
5	3, 4	bitr 173	1 ⊢ (χ ↔ θ)

Syntax hints:   ↔ wb 146

This theorem is referenced by:  pm4.78 354  an12 486  xor 673  xor2 675  19.35 1077  sbco2d 1258  cbval2 1318  cbvex2 1319  cbvald 1322  equsb3 1332  elsb3 1333  sbcom2 1336  dfsb7 1342  2eu6 1457  eq2tr 1536  r19.35 1762  reeanv 1781  gencbvex 1841  gencbval 1843  2reuswap 1940  sbccomglem 1991  dfpss3 2137  difcom 2349  iunn0 2612  exss 2775  opabid 2816  rabxfr 2908  elxp2 3209  eqbrriv 3258  dm0rn0 3336  cnvi 3453  rninxp 3488  fununi 3569  fcoi1 3651  dfoprab2 3997  dfer2 4268  0nelqs 4304  eceqopreq 4319  xpsnen 4441  xpcomen 4445  xpassen 4447  rankuni 4708  kmlem4 4778  zorn2lem4 4801  alephislim 4894  distrlem5pr 5143  supsrlem5 5241  negcon1 5419  ltsubadd 5606  elfzp1 6511  sqr2irrlem4 6728  cjreb 6781  cau5 6919  cvganuz 6925  climcmplem 7137  geoser 7234  efcn 7423  hvsubadd 8928  chocuni 9167  omlsilem 9239  pjoml3 9524  hods 9696  nmopcoadj0 10031  pjin3 10117  eeeeanv 10431

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