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  1485  xorass  1515  cbvaldvaw  2038  sbievw2  2099  sbco4lemOLD  2175  cbvexv1  2340  cbvex  2397  sbco2d  2510  sbcom  2512  sb7f  2523  eq2tri  2791  clelsb1fw  2895  clelsb1f  2896  cbvraldva  3209  rexcom  3258  cbvrexfw  3271  cbvraldva2  3312  cbvrexdva2OLD  3314  sbralie  3317  sbralieOLD  3319  ceqsralt  3473  gencbvex  3498  gencbval  3500  ceqsrexbv  3613  ceqsralbv  3614  euind  3686  reuind  3715  sbccomlem  3823  sbccomlemOLD  3824  sbccom  3825  csbcom  4373  difcom  4442  eqsn  4783  uniintsn  4938  disjxun  5093  reusv2lem4  5343  exss  5410  opab0  5501  opelinxp  5703  eqbrriv  5738  dm0rn0  5871  elidinxp  5999  qfto  6074  rninxp  6132  coeq0  6208  fununi  6561  dffv2  6922  fndmin  6983  fnprb  7148  fntpb  7149  dfoprab2  7411  frpoins3xp3g  8081  dfer2  8633  eceqoveq  8756  euen1  8959  xpsnen  8985  xpassen  8995  marypha2lem3  9346  rankuni  9778  card1  9883  alephislim  9996  dfacacn  10055  kmlem4  10067  ac6num  10392  zorn2lem4  10412  mappsrpr  11021  sqeqori  14139  trclublem  14920  fprodle  15921  vdwmc2  16909  txflf  23909  metustid  24458  caucfil  25199  ovolgelb  25397  dfcgra2  28793  axcontlem5  28931  frgr3v  30237  nmoubi  30734  hvsubaddi  31028  hlimeui  31202  omlsilem  31364  pjoml3i  31548  hodsi  31737  nmopub  31870  nmfnleub  31887  nmopcoadj0i  32065  pjin3i  32156  an42ds  32412  or3dir  32422  ralcom4f  32429  rexcom4f  32430  uniinn0  32512  ordtconnlem1  33893  bnj62  34689  bnj610  34716  bnj1143  34759  bnj1533  34821  bnj543  34862  bnj545  34864  bnj594  34881  cusgracyclt3v  35131  xpab  35701  brsuccf  35917  brfullfun  35924  in-ax8  36200  filnetlem4  36357  icorempo  37327  poimirlem13  37615  poimirlem14  37616  poimirlem21  37623  poimirlem22  37624  poimir  37635  sbccom2lem  38106  alrmomorn  38328  qseq  38628  dfeldisj5  38701  mpet2  38820  isltrn2N  40102  moxfr  42668  ifporcor  43438  ifpancor  43440  ifpbicor  43451  ifpnorcor  43456  ifpnancor  43457  ifpororb  43481  minregex  43510  relexp0eq  43677  hashnzfzclim  44298  pm11.6  44368  sbc3or  44509  cbvexsv  44524  dfich2  47446  ichbi12i  47448  sprvalpwn0  47471  copisnmnd  48157