Theorem 3bitr3i 303

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

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  an33rean  1503  an42ds  1509  xorass  1534  cbvaldvaw  2057  sbievw2  2131  sbco4lemOLD  2206  cbvexv1  2372  cbvex  2429  sbco2d  2542  sbcom  2544  sb7f  2555  eq2tri  2823  clelsb1fw  2927  clelsb1f  2928  cbvraldva  3241  rexcom  3290  cbvrexfw  3302  sbralie  3339  sbralieOLD  3341  ceqsralt  3487  gencbvex  3509  gencbval  3511  ceqsrexbv  3614  ceqsralbv  3615  euind  3685  reuind  3714  sbccomlem  3820  sbccomlemOLD  3821  sbccom  3822  csbcom  4371  difcom  4439  eqsn  4784  uniintsn  4940  disjxun  5095  reusv2lem4  5355  exss  5427  opab0  5521  opelinxp  5723  eqbrriv  5759  dm0rn0  5896  dm0rn0OLD  5897  elidinxp  6028  qfto  6103  rninxp  6159  coeq0  6237  fununi  6590  dffv2  6956  fndmin  7020  fnprb  7186  fntpb  7187  dfoprab2  7448  frpoins3xp3g  8114  dfer2  8672  eceqoveq  8797  euen1  9001  xpsnen  9026  xpassen  9036  marypha2lem3  9376  rankuni  9814  card1  9919  alephislim  10032  dfacacn  10091  kmlem4  10103  ac6num  10429  zorn2lem4  10449  mappsrpr  11059  sqeqori  14220  trclublem  15001  fprodle  16016  vdwmc2  17005  txflf  24053  metustid  24601  caucfil  25332  ovolgelb  25529  dfcgra2  28986  axcontlem5  29125  frgr3v  30433  nmoubi  30931  hvsubaddi  31225  hlimeui  31399  omlsilem  31561  pjoml3i  31745  hodsi  31934  nmopub  32067  nmfnleub  32084  nmopcoadj0i  32262  pjin3i  32353  or3dir  32617  ralcom4f  32624  rexcom4f  32625  uniinn0  32709  extdgfialglem1  33949  ordtconnlem1  34181  bnj62  34976  bnj610  35003  bnj1143  35045  bnj1533  35107  bnj543  35148  bnj545  35150  bnj594  35167  cusgracyclt3v  35466  xpab  36036  lemsuccf  36249  brfullfun  36258  in-ax8  36544  filnetlem4  36701  mh-unprimbi  36864  mh-infprim2bi  36867  bj-alnnf  37172  icorempo  37805  poimirlem13  38092  poimirlem14  38093  poimirlem21  38100  poimirlem22  38101  poimir  38112  sbccom2lem  38583  alrmomorn  38817  raldmqseu  38824  qseq  39192  dfeldisj5  39272  qmapeldisjsim  39319  mpet2  39413  isltrn2N  40704  moxfr  43233  ifporcor  43998  ifpancor  44000  ifpbicor  44011  ifpnorcor  44016  ifpnancor  44017  ifpororb  44041  minregex  44070  relexp0eq  44237  hashnzfzclim  44858  pm11.6  44928  sbc3or  45068  cbvexsv  45083  dfich2  48024  ichbi12i  48026  sprvalpwn0  48049  copisnmnd  48751