Theorem 3bitr3i 304

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

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  an33rean  1511  an42ds  1517  xorass  1542  cbvaldvaw  2065  sbievw2  2139  sbco4lemOLD  2214  cbvexv1  2380  cbvex  2437  sbco2d  2550  sbcom  2552  sb7f  2563  eq2tri  2831  clelsb1fw  2935  clelsb1f  2936  cbvraldva  3251  rexcom  3300  cbvrexfw  3312  sbralie  3349  sbralieOLD  3351  ceqsralt  3497  gencbvex  3519  gencbval  3521  ceqsrexbv  3624  ceqsralbv  3625  euind  3696  reuind  3725  sbccomlem  3831  sbccomlemOLD  3832  sbccom  3833  csbcom  4391  difcom  4454  eqsn  4799  uniintsn  4954  disjxun  5111  reusv2lem4  5375  exss  5447  opab0  5542  opelinxp  5744  eqbrriv  5780  dm0rn0  5917  dm0rn0OLD  5918  elidinxp  6049  qfto  6124  xpdifcnvepel  6169  rninxp  6180  coeq0  6260  fununi  6614  dffv2  6979  fndmin  7043  fnprb  7209  fntpb  7210  dfoprab2  7471  frpoins3xp3g  8139  dfer2  8697  eceqoveq  8822  euen1  9026  xpsnen  9051  xpassen  9061  marypha2lem3  9399  rankuni  9837  card1  9956  alephislim  10069  dfacacn  10127  kmlem4  10139  ac6num  10465  zorn2lem4  10485  mappsrpr  11095  sqeqori  14252  trclublem  15034  fprodle  16052  vdwmc2  17041  txflf  24134  metustid  24682  caucfil  25413  ovolgelb  25610  dfcgra2  29100  axcontlem5  29261  frgr3v  30569  nmoubi  31067  hvsubaddi  31361  hlimeui  31535  omlsilem  31697  pjoml3i  31881  hodsi  32070  nmopub  32203  nmfnleub  32220  nmopcoadj0i  32398  pjin3i  32489  or3dir  32751  ralcom4f  32757  rexcom4f  32758  uniinn0  32840  extdgfialglem1  34029  ordtconnlem1  34261  bnj62  35056  bnj610  35083  bnj1143  35125  bnj1533  35187  bnj543  35228  bnj545  35230  bnj594  35247  cusgracyclt3v  35583  xpab  36153  lemsuccf  36366  brfullfun  36375  in-ax8  36661  filnetlem4  36817  mh-unprimbi  36980  mh-infprim2bi  36983  bj-alnnf  37287  icorempo  37922  poimirlem13  38209  poimirlem14  38210  poimirlem21  38217  poimirlem22  38218  poimir  38229  sbccom2lem  38700  alrmomorn  38934  raldmqseu  38941  qseq  39309  dfeldisj5  39389  qmapeldisjsim  39436  mpet2  39530  isltrn2N  40821  moxfr  43352  ifporcor  44117  ifpancor  44119  ifpbicor  44130  ifpnorcor  44135  ifpnancor  44136  ifpororb  44160  minregex  44189  relexp0eq  44356  hashnzfzclim  44961  pm11.6  45031  sbc3or  45170  cbvexsv  45185  dfich2  48133  ichbi12i  48135  sprvalpwn0  48158  copisnmnd  48860