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 ⊢ (𝜒 ↔ 𝜃)

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  an33rean  1514  an42ds  1519  xorass  1544  cbvaldvaw  2070  sbievw2  2134  cbvexv1  2371  cbvex  2428  sbco2d  2541  sbcom  2543  sb7f  2554  eq2tri  2822  clelsb1fw  2926  clelsb1f  2927  cbvraldva  3242  rexcom  3291  cbvrexfw  3303  sbralie  3338  sbralieOLD  3340  ceqsralt  3484  gencbvex  3506  gencbval  3508  ceqsrexbv  3609  ceqsralbv  3610  euind  3681  reuind  3710  sbccomlem  3816  sbccom  3817  csbcom  4377  difcom  4443  eqsn  4784  uniintsn  4944  disjxun  5100  reusv2lem4  5362  exss  5430  eqvinot  5456  opab0  5528  opelinxp  5730  eqbrriv  5766  dm0rn0  5905  dm0rn0OLD  5906  elidinxp  6035  qfto  6114  xpdifcnvepel  6159  rninxp  6170  coeq0  6257  fununi  6615  dffv2  6980  fndmin  7044  fnprb  7214  fntpb  7215  dfoprab2  7478  frpoins3xp3g  8160  dfer2  8721  eceqoveq  8846  euen1  9057  xpsnen  9083  xpassen  9093  marypha2lem3  9432  rankuni  9882  card1  10052  alephislim  10165  dfacacn  10223  kmlem4  10235  ac6num  10560  zorn2lem4  10580  mappsrpr  11196  sqeqori  14361  trclublem  15153  fprodle  16168  vdwmc2  17162  txflf  24330  metustid  24878  caucfil  25609  ovolgelb  25806  dfcgra2  29343  axcontlem5  29551  frgr3v  30881  nmoubi  31379  hvsubaddi  31673  hlimeui  31847  omlsilem  32009  pjoml3i  32193  hodsi  32382  nmopub  32515  nmfnleub  32532  nmopcoadj0i  32710  pjin3i  32801  or3dir  33105  ralcom4f  33111  rexcom4f  33112  uniinn0  33194  extdgfialglem1  34370  ordtconnlem1  34602  bnj62  35397  bnj610  35424  bnj1143  35466  bnj1533  35528  bnj543  35569  bnj545  35571  bnj594  35588  r1omhf  35783  cusgracyclt3v  35997  xpab  36583  lemsuccf  36795  brfullfun  36804  in-ax8  37105  filnetlem4  37261  mh-unprimbi  37424  mh-infprim2bi  37427  bj-alnnf  37731  icorempo  38367  poimirlem13  38644  poimirlem14  38645  poimirlem21  38652  poimirlem22  38653  poimir  38664  sbccom2lem  39149  alrmomorn  39383  raldmqseu  39390  qseq  39758  dfeldisj5  39838  qmapeldisjsim  39885  mpet2  39979  isltrn2N  41270  moxfr  43796  ifporcor  44556  ifpancor  44558  ifpbicor  44569  ifpnorcor  44574  ifpnancor  44575  ifpororb  44599  minregex  44628  relexp0eq  44794  hashnzfzclim  45399  pm11.6  45469  sbc3or  45608  cbvexsv  45623  dfich2  48633  ichbi12i  48635  sprvalpwn0  48658  copisnmnd  49359  veronesevrowd  51147