Theorem 3bitr3i 304

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

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  an33rean  1514  an42ds  1520  xorass  1545  cbvaldvaw  2071  sbievw2  2136  sbco4lemOLD  2211  cbvexv1  2377  cbvex  2434  sbco2d  2547  sbcom  2549  sb7f  2560  eq2tri  2828  clelsb1fw  2932  clelsb1f  2933  cbvraldva  3248  rexcom  3297  cbvrexfw  3309  sbralie  3345  sbralieOLD  3347  ceqsralt  3492  gencbvex  3514  gencbval  3516  ceqsrexbv  3618  ceqsralbv  3619  euind  3690  reuind  3719  sbccomlem  3825  sbccomlemOLD  3826  sbccom  3827  csbcom  4388  difcom  4454  eqsn  4800  uniintsn  4955  disjxun  5112  reusv2lem4  5377  exss  5449  opab0  5544  opelinxp  5746  eqbrriv  5782  dm0rn0  5919  dm0rn0OLD  5920  elidinxp  6051  qfto  6126  xpdifcnvepel  6171  rninxp  6182  coeq0  6262  fununi  6618  dffv2  6983  fndmin  7047  fnprb  7213  fntpb  7214  dfoprab2  7481  frpoins3xp3g  8146  dfer2  8704  eceqoveq  8829  euen1  9033  xpsnen  9059  xpassen  9069  marypha2lem3  9407  rankuni  9845  card1  9973  alephislim  10086  dfacacn  10144  kmlem4  10156  ac6num  10481  zorn2lem4  10501  mappsrpr  11111  sqeqori  14270  trclublem  15058  fprodle  16076  vdwmc2  17064  txflf  24200  metustid  24748  caucfil  25479  ovolgelb  25676  dfcgra2  29178  axcontlem5  29355  frgr3v  30663  nmoubi  31161  hvsubaddi  31455  hlimeui  31629  omlsilem  31791  pjoml3i  31975  hodsi  32164  nmopub  32297  nmfnleub  32314  nmopcoadj0i  32492  pjin3i  32583  or3dir  32845  ralcom4f  32851  rexcom4f  32852  uniinn0  32934  extdgfialglem1  34113  ordtconnlem1  34345  bnj62  35141  bnj610  35168  bnj1143  35210  bnj1533  35272  bnj543  35313  bnj545  35315  bnj594  35332  cusgracyclt3v  35669  xpab  36239  lemsuccf  36452  brfullfun  36461  in-ax8  36777  filnetlem4  36933  mh-unprimbi  37096  mh-infprim2bi  37099  bj-alnnf  37403  icorempo  38038  poimirlem13  38325  poimirlem14  38326  poimirlem21  38333  poimirlem22  38334  poimir  38345  sbccom2lem  38814  alrmomorn  39048  raldmqseu  39055  qseq  39423  dfeldisj5  39503  qmapeldisjsim  39550  mpet2  39644  isltrn2N  40935  moxfr  43464  ifporcor  44229  ifpancor  44231  ifpbicor  44242  ifpnorcor  44247  ifpnancor  44248  ifpororb  44272  minregex  44301  relexp0eq  44468  hashnzfzclim  45073  pm11.6  45143  sbc3or  45282  cbvexsv  45297  dfich2  48248  ichbi12i  48250  sprvalpwn0  48273  copisnmnd  48975