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  3496  gencbval  3498  ceqsrexbv  3611  ceqsralbv  3612  euind  3683  reuind  3712  sbccomlem  3820  sbccomlemOLD  3821  sbccom  3822  csbcom  4370  difcom  4439  eqsn  4781  uniintsn  4935  disjxun  5089  reusv2lem4  5339  exss  5403  opab0  5494  opelinxp  5696  eqbrriv  5731  dm0rn0  5864  dm0rn0OLD  5865  elidinxp  5993  qfto  6068  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  23922  metustid  24470  caucfil  25211  ovolgelb  25409  dfcgra2  28809  axcontlem5  28947  frgr3v  30253  nmoubi  30750  hvsubaddi  31044  hlimeui  31218  omlsilem  31380  pjoml3i  31564  hodsi  31753  nmopub  31886  nmfnleub  31903  nmopcoadj0i  32081  pjin3i  32172  or3dir  32437  ralcom4f  32444  rexcom4f  32445  uniinn0  32528  extdgfialglem1  33703  ordtconnlem1  33935  bnj62  34730  bnj610  34757  bnj1143  34800  bnj1533  34862  bnj543  34903  bnj545  34905  bnj594  34922  cusgracyclt3v  35198  xpab  35768  brsuccf  35981  brfullfun  35988  in-ax8  36264  filnetlem4  36421  icorempo  37391  poimirlem13  37679  poimirlem14  37680  poimirlem21  37687  poimirlem22  37688  poimir  37699  sbccom2lem  38170  alrmomorn  38392  qseq  38692  dfeldisj5  38765  mpet2  38884  isltrn2N  40165  moxfr  42731  ifporcor  43501  ifpancor  43503  ifpbicor  43514  ifpnorcor  43519  ifpnancor  43520  ifpororb  43544  minregex  43573  relexp0eq  43740  hashnzfzclim  44361  pm11.6  44431  sbc3or  44571  cbvexsv  44586  dfich2  47495  ichbi12i  47497  sprvalpwn0  47520  copisnmnd  48206