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  an42ds  1491  xorass  1516  cbvaldvaw  2039  sbievw2  2101  sbco4lemOLD  2177  cbvexv1  2342  cbvex  2399  sbco2d  2512  sbcom  2514  sb7f  2525  eq2tri  2793  clelsb1fw  2898  clelsb1f  2899  cbvraldva  3212  rexcom  3261  cbvrexfw  3273  cbvraldva2  3314  sbralie  3318  sbralieOLD  3320  ceqsralt  3471  gencbvex  3495  gencbval  3497  ceqsrexbv  3606  ceqsralbv  3607  euind  3678  reuind  3707  sbccomlem  3815  sbccomlemOLD  3816  sbccom  3817  csbcom  4367  difcom  4436  eqsn  4778  uniintsn  4933  disjxun  5087  reusv2lem4  5337  exss  5401  opab0  5492  opelinxp  5694  eqbrriv  5730  dm0rn0  5863  dm0rn0OLD  5864  elidinxp  5992  qfto  6067  rninxp  6126  coeq0  6203  fununi  6556  dffv2  6917  fndmin  6978  fnprb  7142  fntpb  7143  dfoprab2  7404  frpoins3xp3g  8071  dfer2  8623  eceqoveq  8746  euen1  8949  xpsnen  8974  xpassen  8984  marypha2lem3  9321  rankuni  9756  card1  9861  alephislim  9974  dfacacn  10033  kmlem4  10045  ac6num  10370  zorn2lem4  10390  mappsrpr  10999  sqeqori  14121  trclublem  14902  fprodle  15903  vdwmc2  16891  txflf  23921  metustid  24469  caucfil  25210  ovolgelb  25408  dfcgra2  28808  axcontlem5  28946  frgr3v  30255  nmoubi  30752  hvsubaddi  31046  hlimeui  31220  omlsilem  31382  pjoml3i  31566  hodsi  31755  nmopub  31888  nmfnleub  31905  nmopcoadj0i  32083  pjin3i  32174  or3dir  32439  ralcom4f  32446  rexcom4f  32447  uniinn0  32530  extdgfialglem1  33705  ordtconnlem1  33937  bnj62  34732  bnj610  34759  bnj1143  34802  bnj1533  34864  bnj543  34905  bnj545  34907  bnj594  34924  cusgracyclt3v  35200  xpab  35770  lemsuccf  35983  brfullfun  35992  in-ax8  36268  filnetlem4  36425  icorempo  37395  poimirlem13  37672  poimirlem14  37673  poimirlem21  37680  poimirlem22  37681  poimir  37692  sbccom2lem  38163  alrmomorn  38389  qseq  38745  dfeldisj5  38818  mpet2  38937  isltrn2N  40218  moxfr  42784  ifporcor  43554  ifpancor  43556  ifpbicor  43567  ifpnorcor  43572  ifpnancor  43573  ifpororb  43597  minregex  43626  relexp0eq  43793  hashnzfzclim  44414  pm11.6  44484  sbc3or  44624  cbvexsv  44639  dfich2  47557  ichbi12i  47559  sprvalpwn0  47582  copisnmnd  48268