Theorem 3bitr3i 302

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

Syntax hints:   ↔ wb 207

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 208

This theorem is referenced by:  an33rean  1491  an42ds  1497  xorass  1522  cbvaldvaw  2045  sbievw2  2109  sbco4lemOLD  2184  cbvexv1  2350  cbvex  2407  sbco2d  2520  sbcom  2522  sb7f  2533  eq2tri  2802  clelsb1fw  2906  clelsb1f  2907  cbvraldva  3220  rexcom  3269  cbvrexfw  3281  sbralie  3318  sbralieOLD  3320  ceqsralt  3467  gencbvex  3490  gencbval  3492  ceqsrexbv  3601  ceqsralbv  3602  euind  3672  reuind  3701  sbccomlem  3808  sbccomlemOLD  3809  sbccom  3810  csbcom  4355  difcom  4423  eqsn  4767  uniintsn  4922  disjxun  5077  reusv2lem4  5337  exss  5409  opab0  5503  opelinxp  5705  eqbrriv  5741  dm0rn0  5873  dm0rn0OLD  5874  elidinxp  6003  qfto  6078  rninxp  6137  coeq0  6214  fununi  6567  dffv2  6929  fndmin  6993  fnprb  7159  fntpb  7160  dfoprab2  7421  frpoins3xp3g  8088  dfer2  8641  eceqoveq  8766  euen1  8971  xpsnen  8996  xpassen  9006  marypha2lem3  9347  rankuni  9785  card1  9890  alephislim  10003  dfacacn  10062  kmlem4  10074  ac6num  10399  zorn2lem4  10419  mappsrpr  11029  sqeqori  14174  trclublem  14955  fprodle  15959  vdwmc2  16948  txflf  23996  metustid  24544  caucfil  25275  ovolgelb  25472  dfcgra2  28923  axcontlem5  29062  frgr3v  30370  nmoubi  30868  hvsubaddi  31162  hlimeui  31336  omlsilem  31498  pjoml3i  31682  hodsi  31871  nmopub  32004  nmfnleub  32021  nmopcoadj0i  32199  pjin3i  32290  or3dir  32554  ralcom4f  32561  rexcom4f  32562  uniinn0  32646  extdgfialglem1  33883  ordtconnlem1  34115  bnj62  34910  bnj610  34937  bnj1143  34979  bnj1533  35041  bnj543  35082  bnj545  35084  bnj594  35101  cusgracyclt3v  35391  xpab  35961  lemsuccf  36174  brfullfun  36183  in-ax8  36459  filnetlem4  36616  mh-unprimbi  36779  mh-infprim2bi  36782  bj-alnnf  37087  icorempo  37720  poimirlem13  38007  poimirlem14  38008  poimirlem21  38015  poimirlem22  38016  poimir  38027  sbccom2lem  38498  alrmomorn  38732  raldmqseu  38739  qseq  39107  dfeldisj5  39187  qmapeldisjsim  39234  mpet2  39328  isltrn2N  40619  moxfr  43148  ifporcor  43913  ifpancor  43915  ifpbicor  43926  ifpnorcor  43931  ifpnancor  43932  ifpororb  43956  minregex  43985  relexp0eq  44152  hashnzfzclim  44773  pm11.6  44843  sbc3or  44983  cbvexsv  44998  dfich2  47940  ichbi12i  47942  sprvalpwn0  47965  copisnmnd  48667