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  2346  cbvex  2403  sbco2d  2516  sbcom  2518  sb7f  2529  eq2tri  2798  clelsb1fw  2902  clelsb1f  2903  cbvraldva  3217  rexcom  3266  cbvrexfw  3278  sbralie  3315  sbralieOLD  3317  ceqsralt  3464  gencbvex  3487  gencbval  3489  ceqsrexbv  3598  ceqsralbv  3599  euind  3670  reuind  3699  sbccomlem  3807  sbccomlemOLD  3808  sbccom  3809  csbcom  4360  difcom  4428  eqsn  4772  uniintsn  4927  disjxun  5083  reusv2lem4  5343  exss  5415  opab0  5509  opelinxp  5711  eqbrriv  5747  dm0rn0  5879  dm0rn0OLD  5880  elidinxp  6009  qfto  6084  rninxp  6143  coeq0  6220  fununi  6573  dffv2  6935  fndmin  6997  fnprb  7163  fntpb  7164  dfoprab2  7425  frpoins3xp3g  8091  dfer2  8644  eceqoveq  8769  euen1  8974  xpsnen  8999  xpassen  9009  marypha2lem3  9350  rankuni  9787  card1  9892  alephislim  10005  dfacacn  10064  kmlem4  10076  ac6num  10401  zorn2lem4  10421  mappsrpr  11031  sqeqori  14176  trclublem  14957  fprodle  15961  vdwmc2  16950  txflf  23971  metustid  24519  caucfil  25250  ovolgelb  25447  dfcgra2  28898  axcontlem5  29037  frgr3v  30345  nmoubi  30843  hvsubaddi  31137  hlimeui  31311  omlsilem  31473  pjoml3i  31657  hodsi  31846  nmopub  31979  nmfnleub  31996  nmopcoadj0i  32174  pjin3i  32265  or3dir  32529  ralcom4f  32536  rexcom4f  32537  uniinn0  32620  extdgfialglem1  33836  ordtconnlem1  34068  bnj62  34863  bnj610  34890  bnj1143  34932  bnj1533  34994  bnj543  35035  bnj545  35037  bnj594  35054  cusgracyclt3v  35338  xpab  35908  lemsuccf  36121  brfullfun  36130  in-ax8  36406  filnetlem4  36563  mh-unprimbi  36726  mh-infprim2bi  36729  bj-alnnf  37034  icorempo  37667  poimirlem13  37954  poimirlem14  37955  poimirlem21  37962  poimirlem22  37963  poimir  37974  sbccom2lem  38445  alrmomorn  38679  raldmqseu  38686  qseq  39054  dfeldisj5  39134  qmapeldisjsim  39181  mpet2  39275  isltrn2N  40566  moxfr  43124  ifporcor  43889  ifpancor  43891  ifpbicor  43902  ifpnorcor  43907  ifpnancor  43908  ifpororb  43932  minregex  43961  relexp0eq  44128  hashnzfzclim  44749  pm11.6  44819  sbc3or  44959  cbvexsv  44974  dfich2  47918  ichbi12i  47920  sprvalpwn0  47943  copisnmnd  48645