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  2037  sbievw2  2098  sbco4lemOLD  2174  cbvexv1  2344  cbvex  2404  sbco2d  2517  sbcom  2519  sb7f  2530  eq2tri  2804  clelsb2OLD  2870  clelsb1fw  2909  clelsb1f  2910  cbvraldva  3239  rexcom  3290  cbvrexfw  3305  cbvraldva2  3348  cbvrexdva2OLD  3350  sbralie  3358  ceqsralt  3516  gencbvex  3541  gencbval  3543  ceqsrexbv  3656  ceqsralbv  3657  euind  3730  reuind  3759  sbccomlem  3869  sbccomlemOLD  3870  sbccom  3871  csbcom  4420  difcom  4489  eqsn  4829  uniintsn  4985  disjxun  5141  reusv2lem4  5401  exss  5468  opab0  5559  opelinxp  5765  eqbrriv  5801  dm0rn0  5935  elidinxp  6062  qfto  6141  rninxp  6199  coeq0  6275  fununi  6641  dffv2  7004  fndmin  7065  fnprb  7228  fntpb  7229  dfoprab2  7491  frpoins3xp3g  8166  dfer2  8746  eceqoveq  8862  euen1  9067  xpsnen  9095  xpassen  9106  marypha2lem3  9477  rankuni  9903  card1  10008  alephislim  10123  dfacacn  10182  kmlem4  10194  ac6num  10519  zorn2lem4  10539  mappsrpr  11148  sqeqori  14253  trclublem  15034  fprodle  16032  vdwmc2  17017  txflf  24014  metustid  24567  caucfil  25317  ovolgelb  25515  dfcgra2  28838  axcontlem5  28983  frgr3v  30294  nmoubi  30791  hvsubaddi  31085  hlimeui  31259  omlsilem  31421  pjoml3i  31605  hodsi  31794  nmopub  31927  nmfnleub  31944  nmopcoadj0i  32122  pjin3i  32213  an42ds  32469  or3dir  32479  ralcom4f  32486  rexcom4f  32487  uniinn0  32563  ordtconnlem1  33923  bnj62  34734  bnj610  34761  bnj1143  34804  bnj1533  34866  bnj543  34907  bnj545  34909  bnj594  34926  cusgracyclt3v  35161  xpab  35726  brsuccf  35942  brfullfun  35949  in-ax8  36225  filnetlem4  36382  icorempo  37352  poimirlem13  37640  poimirlem14  37641  poimirlem21  37648  poimirlem22  37649  poimir  37660  sbccom2lem  38131  alrmomorn  38359  dfeldisj5  38722  mpet2  38841  isltrn2N  40122  moxfr  42703  ifporcor  43475  ifpancor  43477  ifpbicor  43488  ifpnorcor  43493  ifpnancor  43494  ifpororb  43518  minregex  43547  relexp0eq  43714  hashnzfzclim  44341  pm11.6  44411  sbc3or  44552  cbvexsv  44567  dfich2  47445  ichbi12i  47447  sprvalpwn0  47470  copisnmnd  48085