Theorem 3bitr3i 290

Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 19-Aug-1993.)

Hypotheses

Ref	Expression
3bitr3i.1	⊢ (𝜑 ↔ 𝜓)
3bitr3i.2	⊢ (𝜑 ↔ 𝜒)
3bitr3i.3	⊢ (𝜓 ↔ 𝜃)

Assertion

Ref	Expression
3bitr3i	⊢ (𝜒 ↔ 𝜃)

Proof of Theorem 3bitr3i

Step	Hyp	Ref	Expression
1		3bitr3i.2	. . 3 ⊢ (𝜑 ↔ 𝜒)
2		3bitr3i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	bitr3i 266	. 2 ⊢ (𝜒 ↔ 𝜓)
4		3bitr3i.3	. 2 ⊢ (𝜓 ↔ 𝜃)
5	3, 4	bitri 264	1 ⊢ (𝜒 ↔ 𝜃)

Syntax hints:   ↔ wb 196

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

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  an12  838  xorass  1468  cbval2  2279  cbvaldva  2281  sbco2d  2416  sbcom  2418  equsb3  2432  equsb3ALT  2433  elsb3  2434  elsb4  2435  sb7f  2453  sbco4lem  2465  eq2tri  2683  eqsb3  2728  clelsb3  2729  clelsb3f  2768  r19.35  3084  ralcom4  3224  rexcom4  3225  ceqsralt  3229  gencbvex  3250  gencbval  3252  ceqsrexbv  3337  euind  3393  reuind  3411  sbccomlem  3508  sbccom  3509  csbcom  3994  difcom  4053  eqsn  4361  uniintsn  4514  disjxun  4651  reusv2lem4  4872  exss  4931  opab0  5007  elxp2OLD  5133  eqbrriv  5215  dm0rn0  5342  dfres2  5453  qfto  5517  rninxp  5573  coeq0  5644  fununi  5964  dffv2  6271  fndmin  6324  fnprb  6472  fntpb  6473  dfoprab2  6701  dfer2  7743  eceqoveq  7853  euen1  8026  xpsnen  8044  xpassen  8054  marypha2lem3  8343  rankuni  8726  card1  8794  alephislim  8906  dfacacn  8963  kmlem4  8975  ac6num  9301  zorn2lem4  9321  fpwwe2lem8  9459  fpwwe2lem12  9463  mappsrpr  9929  sqeqori  12976  trclublem  13734  fprodle  14727  vdwmc2  15683  txflf  21810  metustid  22359  caucfil  23081  ovolgelb  23248  dfcgra2  25721  axcontlem5  25848  frgr3v  27139  nmoubi  27627  hvsubaddi  27923  hlimeui  28097  omlsilem  28261  pjoml3i  28445  hodsi  28634  nmopub  28767  nmfnleub  28784  nmopcoadj0i  28962  pjin3i  29053  or3dir  29308  ralcom4f  29316  rexcom4f  29317  uniinn0  29366  ordtconnlem1  29970  bnj62  30786  bnj610  30817  bnj1143  30861  bnj1533  30922  bnj543  30963  bnj545  30965  bnj594  30982  ceqsralv2  31607  br1steq  31670  br2ndeq  31671  brsuccf  32048  brfullfun  32055  filnetlem4  32376  bj-ssbcom3lem  32650  bj-cbval2v  32737  bj-clelsb3  32848  icorempt2  33199  poimirlem13  33422  poimirlem14  33423  poimirlem21  33430  poimirlem22  33431  poimir  33442  sbccom2lem  33929  eldmqsres  34051  opelinxp  34111  alrmomo  34123  isltrn2N  35406  moxfr  37255  ifporcor  37806  ifpancor  37808  ifpbicor  37820  ifpnorcor  37825  ifpnancor  37826  ifpororb  37850  relexp0eq  37993  hashnzfzclim  38521  pm11.6  38592  sbc3or  38738  cbvexsv  38762  sprvalpwn0  41733  copisnmnd  41809