Theorem 3bitr3i 302

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 278	. 2 ⊢ (𝜒 ↔ 𝜓)
4		3bitr3i.3	. 2 ⊢ (𝜓 ↔ 𝜃)
5	3, 4	bitri 276	1 ⊢ (𝜒 ↔ 𝜃)

Syntax hints:   ↔ wb 207

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 208

This theorem is referenced by:  xorass  1500  sbievw2  2076  sbco4lem  2251  cbvex  2375  cbvexvOLD  2379  cbval2OLD  2391  sbco2d  2510  sbcom  2512  sb7f  2523  sb7fALT  2572  eq2tri  2860  clelsb3vOLD  2913  clelsb3f  2955  clelsb3fOLD  2956  cbvraldva2  3409  cbvrexdva2  3410  cbvrexdva2OLD  3411  ralcom4OLD  3471  rexcom4OLD  3472  ceqsralt  3474  gencbvex  3495  gencbval  3497  ceqsrexbv  3591  euind  3654  reuind  3683  sbccomlem  3787  sbccom  3788  csbcom  4295  difcom  4354  eqsn  4675  uniintsn  4825  disjxun  4966  reusv2lem4  5200  exss  5254  opab0  5336  opelinxp  5524  eqbrriv  5557  dm0rn0  5686  elidinxp  5799  qfto  5864  rninxp  5919  coeq0  5990  fununi  6306  dffv2  6630  fndmin  6687  fnprb  6844  fntpb  6845  dfoprab2  7078  dfer2  8147  eceqoveq  8259  euen1  8434  xpsnen  8455  xpassen  8465  marypha2lem3  8754  rankuni  9145  card1  9250  alephislim  9362  dfacacn  9420  kmlem4  9432  ac6num  9754  zorn2lem4  9774  mappsrpr  10383  sqeqori  13430  trclublem  14193  fprodle  15187  vdwmc2  16148  txflf  22302  metustid  22851  caucfil  23573  ovolgelb  23768  dfcgra2  26302  axcontlem5  26441  frgr3v  27742  nmoubi  28236  hvsubaddi  28530  hlimeui  28704  omlsilem  28866  pjoml3i  29050  hodsi  29239  nmopub  29372  nmfnleub  29389  nmopcoadj0i  29567  pjin3i  29658  or3dir  29913  ralcom4f  29921  rexcom4f  29922  uniinn0  29987  ordtconnlem1  30780  bnj62  31603  bnj610  31631  bnj1143  31675  bnj1533  31736  bnj543  31777  bnj545  31779  bnj594  31796  cusgracyclt3v  32013  ceqsralv2  32566  brsuccf  33013  brfullfun  33020  filnetlem4  33340  bj-cbval2v  33674  icorempo  34184  poimirlem13  34457  poimirlem14  34458  poimirlem21  34465  poimirlem22  34466  poimir  34477  sbccom2lem  34955  alrmomorn  35165  dfeldisj5  35506  isltrn2N  36808  moxfr  38795  ifporcor  39333  ifpancor  39335  ifpbicor  39347  ifpnorcor  39352  ifpnancor  39353  ifpororb  39377  relexp0eq  39552  hashnzfzclim  40213  pm11.6  40283  sbc3or  40426  cbvexsv  40441  dfich2  43117  ichbi12i  43122  sprvalpwn0  43149  copisnmnd  43580