Theorem 3bitr3i 301

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 277	. 2 ⊢ (𝜒 ↔ 𝜓)
4		3bitr3i.3	. 2 ⊢ (𝜓 ↔ 𝜃)
5	3, 4	bitri 275	1 ⊢ (𝜒 ↔ 𝜃)

Syntax hints:   ↔ wb 206

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 207

This theorem is referenced by:  an33rean  1486  an42ds  1492  xorass  1517  cbvaldvaw  2040  sbievw2  2104  sbco4lemOLD  2180  cbvexv1  2347  cbvex  2404  sbco2d  2517  sbcom  2519  sb7f  2530  eq2tri  2799  clelsb1fw  2903  clelsb1f  2904  cbvraldva  3218  rexcom  3267  cbvrexfw  3279  cbvraldva2  3320  sbralie  3324  sbralieOLD  3326  ceqsralt  3477  gencbvex  3501  gencbval  3503  ceqsrexbv  3612  ceqsralbv  3613  euind  3684  reuind  3713  sbccomlem  3821  sbccomlemOLD  3822  sbccom  3823  csbcom  4374  difcom  4443  eqsn  4787  uniintsn  4942  disjxun  5098  reusv2lem4  5348  exss  5418  opab0  5510  opelinxp  5712  eqbrriv  5748  dm0rn0  5881  dm0rn0OLD  5882  elidinxp  6011  qfto  6086  rninxp  6145  coeq0  6222  fununi  6575  dffv2  6937  fndmin  6999  fnprb  7164  fntpb  7165  dfoprab2  7426  frpoins3xp3g  8093  dfer2  8646  eceqoveq  8771  euen1  8976  xpsnen  9001  xpassen  9011  marypha2lem3  9352  rankuni  9787  card1  9892  alephislim  10005  dfacacn  10064  kmlem4  10076  ac6num  10401  zorn2lem4  10421  mappsrpr  11031  sqeqori  14149  trclublem  14930  fprodle  15931  vdwmc2  16919  txflf  23962  metustid  24510  caucfil  25251  ovolgelb  25449  dfcgra2  28914  axcontlem5  29053  frgr3v  30362  nmoubi  30859  hvsubaddi  31153  hlimeui  31327  omlsilem  31489  pjoml3i  31673  hodsi  31862  nmopub  31995  nmfnleub  32012  nmopcoadj0i  32190  pjin3i  32281  or3dir  32545  ralcom4f  32552  rexcom4f  32553  uniinn0  32636  extdgfialglem1  33869  ordtconnlem1  34101  bnj62  34896  bnj610  34923  bnj1143  34965  bnj1533  35027  bnj543  35068  bnj545  35070  bnj594  35087  cusgracyclt3v  35369  xpab  35939  lemsuccf  36152  brfullfun  36161  in-ax8  36437  filnetlem4  36594  bj-df-sb  36894  bj-alnnf  36977  icorempo  37603  poimirlem13  37881  poimirlem14  37882  poimirlem21  37889  poimirlem22  37890  poimir  37901  sbccom2lem  38372  alrmomorn  38606  raldmqseu  38613  qseq  38981  dfeldisj5  39061  qmapeldisjsim  39108  mpet2  39202  isltrn2N  40493  moxfr  43046  ifporcor  43815  ifpancor  43817  ifpbicor  43828  ifpnorcor  43833  ifpnancor  43834  ifpororb  43858  minregex  43887  relexp0eq  44054  hashnzfzclim  44675  pm11.6  44745  sbc3or  44885  cbvexsv  44900  dfich2  47815  ichbi12i  47817  sprvalpwn0  47840  copisnmnd  48526