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  1515  an42ds  1520  xorass  1545  cbvaldvaw  2073  sbievw2  2137  cbvexv1  2375  cbvex  2431  sbco2d  2544  sbcom  2546  sb7f  2557  eq2tri  2825  clelsb1fw  2930  clelsb1f  2931  cbvraldva  3246  rexcom  3295  cbvrexfw  3307  sbralie  3342  sbralieOLD  3344  ceqsralt  3488  gencbvex  3510  gencbval  3512  ceqsrexbv  3613  ceqsralbv  3614  euind  3685  reuind  3714  sbccomlem  3821  sbccom  3822  csbcom  4381  difcom  4447  eqsn  4788  uniintsn  4948  disjxun  5104  reusv2lem4  5368  exss  5436  eqvinot  5462  opab0  5534  opelinxp  5737  eqbrriv  5773  dm0rn0  5914  dm0rn0OLD  5915  elidinxp  6049  qfto  6128  xpdifcnvepel  6173  rninxp  6184  coeq0  6271  fununi  6640  dffv2  7006  fndmin  7070  fnprb  7240  fntpb  7241  dfoprab2  7504  frpoins3xp3g  8188  dfer2  8749  eceqoveq  8874  euen1  9085  xpsnen  9111  xpassen  9121  marypha2lem3  9459  rankuni  9909  card1  10079  alephislim  10192  dfacacn  10250  kmlem4  10262  ac6num  10587  zorn2lem4  10607  mappsrpr  11223  sqeqori  14388  trclublem  15180  fprodle  16195  vdwmc2  17189  txflf  24358  metustid  24906  caucfil  25637  ovolgelb  25834  dfcgra2  29371  axcontlem5  29579  frgr3v  30909  nmoubi  31407  hvsubaddi  31701  hlimeui  31875  omlsilem  32037  pjoml3i  32221  hodsi  32410  nmopub  32543  nmfnleub  32560  nmopcoadj0i  32738  pjin3i  32829  or3dir  33133  ralcom4f  33139  rexcom4f  33140  uniinn0  33222  extdgfialglem1  34407  ordtconnlem1  34639  bnj62  35434  bnj610  35461  bnj1143  35503  bnj1533  35565  bnj543  35606  bnj545  35608  bnj594  35625  cusgracyclt3v  36091  mirimanofffr  36642  xpab  36682  lemsuccf  36894  brfullfun  36903  in-ax8  37204  filnetlem4  37360  mh-unprimbi  37523  mh-infprim2bi  37526  bj-alnnf  37830  icorempo  38479  poimirlem13  38756  poimirlem14  38757  poimirlem21  38764  poimirlem22  38765  poimir  38776  sbccom2lem  39259  alrmomorn  39493  raldmqseu  39500  qseq  39868  dfeldisj5  39948  qmapeldisjsim  39995  mpet2  40089  isltrn2N  41380  moxfr  43907  ifporcor  44666  ifpancor  44668  ifpbicor  44679  ifpnorcor  44684  ifpnancor  44685  ifpororb  44709  minregex  44738  relexp0eq  44904  hashnzfzclim  45509  pm11.6  45579  sbc3or  45717  cbvexsv  45732  dfich2  48755  ichbi12i  48757  sprvalpwn0  48780  copisnmnd  49481  veronesevrowd  51291