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 205

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 206

This theorem is referenced by:  an33rean  1484  xorass  1515  cbvaldvaw  2042  sbievw2  2100  sbco4lem  2273  sbco4lemOLD  2274  cbvexv1  2339  cbvex  2399  sbco2d  2512  sbcom  2514  sb7f  2525  eq2tri  2800  clelsb2OLD  2863  clelsb1fw  2908  clelsb1f  2909  cbvraldva  3237  rexcom  3288  cbvrexfw  3303  cbvraldva2  3345  cbvrexdva2OLD  3347  sbralie  3355  ceqsralt  3506  gencbvex  3534  gencbval  3536  ceqsrexbv  3642  ceqsralbv  3643  euind  3718  reuind  3747  sbccomlem  3862  sbccom  3863  csbcom  4415  difcom  4484  eqsn  4828  uniintsn  4987  disjxun  5142  reusv2lem4  5395  exss  5459  opab0  5550  opelinxp  5750  eqbrriv  5786  dm0rn0  5919  elidinxp  6036  qfto  6114  rninxp  6170  coeq0  6246  fununi  6615  dffv2  6975  fndmin  7034  fnprb  7197  fntpb  7198  dfoprab2  7454  frpoins3xp3g  8114  dfer2  8692  eceqoveq  8804  euen1  9014  xpsnen  9043  xpassen  9054  marypha2lem3  9419  rankuni  9845  card1  9950  alephislim  10065  dfacacn  10123  kmlem4  10135  ac6num  10461  zorn2lem4  10481  mappsrpr  11090  sqeqori  14165  trclublem  14929  fprodle  15927  vdwmc2  16899  txflf  23479  metustid  24032  caucfil  24769  ovolgelb  24966  dfcgra2  28048  axcontlem5  28193  frgr3v  29495  nmoubi  29990  hvsubaddi  30284  hlimeui  30458  omlsilem  30620  pjoml3i  30804  hodsi  30993  nmopub  31126  nmfnleub  31143  nmopcoadj0i  31321  pjin3i  31412  or3dir  31667  ralcom4f  31674  rexcom4f  31675  uniinn0  31748  ordtconnlem1  32835  bnj62  33662  bnj610  33689  bnj1143  33732  bnj1533  33794  bnj543  33835  bnj545  33837  bnj594  33854  cusgracyclt3v  34078  xpab  34626  brsuccf  34844  brfullfun  34851  filnetlem4  35171  icorempo  36137  poimirlem13  36406  poimirlem14  36407  poimirlem21  36414  poimirlem22  36415  poimir  36426  sbccom2lem  36898  alrmomorn  37133  dfeldisj5  37497  mpet2  37616  isltrn2N  38897  moxfr  41301  ifporcor  42084  ifpancor  42086  ifpbicor  42097  ifpnorcor  42102  ifpnancor  42103  ifpororb  42127  minregex  42156  relexp0eq  42323  hashnzfzclim  42952  pm11.6  43022  sbc3or  43164  cbvexsv  43179  dfich2  45999  ichbi12i  46001  sprvalpwn0  46024  copisnmnd  46452