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  1483  xorass  1512  cbvaldvaw  2037  sbievw2  2098  sbco4lemOLD  2175  sbco4lemOLDOLD  2282  cbvexv1  2348  cbvex  2407  sbco2d  2520  sbcom  2522  sb7f  2533  eq2tri  2807  clelsb2OLD  2873  clelsb1fw  2912  clelsb1f  2913  cbvraldva  3245  rexcom  3296  cbvrexfw  3311  cbvraldva2  3356  cbvrexdva2OLD  3358  sbralie  3366  ceqsralt  3524  gencbvex  3553  gencbval  3555  ceqsrexbv  3669  ceqsralbv  3670  euind  3746  reuind  3775  sbccomlem  3891  sbccomlemOLD  3892  sbccom  3893  csbcom  4443  difcom  4512  eqsn  4854  uniintsn  5009  disjxun  5164  reusv2lem4  5419  exss  5483  opab0  5573  opelinxp  5779  eqbrriv  5815  dm0rn0  5949  elidinxp  6073  qfto  6153  rninxp  6210  coeq0  6286  fununi  6653  dffv2  7017  fndmin  7078  fnprb  7245  fntpb  7246  dfoprab2  7508  frpoins3xp3g  8182  dfer2  8764  eceqoveq  8880  euen1  9091  xpsnen  9121  xpassen  9132  marypha2lem3  9506  rankuni  9932  card1  10037  alephislim  10152  dfacacn  10211  kmlem4  10223  ac6num  10548  zorn2lem4  10568  mappsrpr  11177  sqeqori  14263  trclublem  15044  fprodle  16044  vdwmc2  17026  txflf  24035  metustid  24588  caucfil  25336  ovolgelb  25534  dfcgra2  28856  axcontlem5  29001  frgr3v  30307  nmoubi  30804  hvsubaddi  31098  hlimeui  31272  omlsilem  31434  pjoml3i  31618  hodsi  31807  nmopub  31940  nmfnleub  31957  nmopcoadj0i  32135  pjin3i  32226  an42ds  32479  or3dir  32489  ralcom4f  32496  rexcom4f  32497  uniinn0  32573  ordtconnlem1  33870  bnj62  34696  bnj610  34723  bnj1143  34766  bnj1533  34828  bnj543  34869  bnj545  34871  bnj594  34888  cusgracyclt3v  35124  xpab  35688  brsuccf  35905  brfullfun  35912  in-ax8  36190  filnetlem4  36347  icorempo  37317  poimirlem13  37593  poimirlem14  37594  poimirlem21  37601  poimirlem22  37602  poimir  37613  sbccom2lem  38084  alrmomorn  38314  dfeldisj5  38677  mpet2  38796  isltrn2N  40077  moxfr  42648  ifporcor  43424  ifpancor  43426  ifpbicor  43437  ifpnorcor  43442  ifpnancor  43443  ifpororb  43467  minregex  43496  relexp0eq  43663  hashnzfzclim  44291  pm11.6  44361  sbc3or  44503  cbvexsv  44518  dfich2  47332  ichbi12i  47334  sprvalpwn0  47357  copisnmnd  47892