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  2343  cbvex  2403  sbco2d  2516  sbcom  2518  sb7f  2529  eq2tri  2797  clelsb2OLD  2863  clelsb1fw  2902  clelsb1f  2903  cbvraldva  3222  rexcom  3271  cbvrexfw  3285  cbvraldva2  3327  cbvrexdva2OLD  3329  sbralie  3337  ceqsralt  3495  gencbvex  3520  gencbval  3522  ceqsrexbv  3635  ceqsralbv  3636  euind  3707  reuind  3736  sbccomlem  3844  sbccomlemOLD  3845  sbccom  3846  csbcom  4395  difcom  4464  eqsn  4805  uniintsn  4961  disjxun  5117  reusv2lem4  5371  exss  5438  opab0  5529  opelinxp  5734  eqbrriv  5770  dm0rn0  5904  elidinxp  6031  qfto  6110  rninxp  6168  coeq0  6244  fununi  6611  dffv2  6974  fndmin  7035  fnprb  7200  fntpb  7201  dfoprab2  7465  frpoins3xp3g  8140  dfer2  8720  eceqoveq  8836  euen1  9041  xpsnen  9069  xpassen  9080  marypha2lem3  9449  rankuni  9877  card1  9982  alephislim  10097  dfacacn  10156  kmlem4  10168  ac6num  10493  zorn2lem4  10513  mappsrpr  11122  sqeqori  14232  trclublem  15014  fprodle  16012  vdwmc2  16999  txflf  23944  metustid  24493  caucfil  25235  ovolgelb  25433  dfcgra2  28809  axcontlem5  28947  frgr3v  30256  nmoubi  30753  hvsubaddi  31047  hlimeui  31221  omlsilem  31383  pjoml3i  31567  hodsi  31756  nmopub  31889  nmfnleub  31906  nmopcoadj0i  32084  pjin3i  32175  an42ds  32431  or3dir  32441  ralcom4f  32448  rexcom4f  32449  uniinn0  32531  ordtconnlem1  33955  bnj62  34751  bnj610  34778  bnj1143  34821  bnj1533  34883  bnj543  34924  bnj545  34926  bnj594  34943  cusgracyclt3v  35178  xpab  35743  brsuccf  35959  brfullfun  35966  in-ax8  36242  filnetlem4  36399  icorempo  37369  poimirlem13  37657  poimirlem14  37658  poimirlem21  37665  poimirlem22  37666  poimir  37677  sbccom2lem  38148  alrmomorn  38376  dfeldisj5  38739  mpet2  38858  isltrn2N  40139  moxfr  42715  ifporcor  43486  ifpancor  43488  ifpbicor  43499  ifpnorcor  43504  ifpnancor  43505  ifpororb  43529  minregex  43558  relexp0eq  43725  hashnzfzclim  44346  pm11.6  44416  sbc3or  44557  cbvexsv  44572  dfich2  47472  ichbi12i  47474  sprvalpwn0  47497  copisnmnd  48144