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  2135  sbco4lemOLD  2210  cbvexv1  2373  cbvex  2430  sbco2d  2543  sbcom  2545  sb7f  2556  eq2tri  2824  clelsb1fw  2928  clelsb1f  2929  cbvraldva  3244  rexcom  3293  cbvrexfw  3305  sbralie  3340  sbralieOLD  3342  ceqsralt  3487  gencbvex  3509  gencbval  3511  ceqsrexbv  3613  ceqsralbv  3614  euind  3685  reuind  3714  sbccomlem  3820  sbccom  3821  csbcom  4381  difcom  4447  eqsn  4793  uniintsn  4948  disjxun  5105  reusv2lem4  5370  exss  5442  opab0  5537  opelinxp  5739  eqbrriv  5775  dm0rn0  5912  dm0rn0OLD  5913  elidinxp  6044  qfto  6119  xpdifcnvepel  6165  rninxp  6176  coeq0  6256  fununi  6612  dffv2  6977  fndmin  7041  fnprb  7211  fntpb  7212  dfoprab2  7475  frpoins3xp3g  8143  dfer2  8701  eceqoveq  8826  euen1  9037  xpsnen  9063  xpassen  9073  marypha2lem3  9411  rankuni  9849  card1  9977  alephislim  10090  dfacacn  10148  kmlem4  10160  ac6num  10485  zorn2lem4  10505  mappsrpr  11121  sqeqori  14282  trclublem  15072  fprodle  16089  vdwmc2  17077  txflf  24238  metustid  24786  caucfil  25517  ovolgelb  25714  dfcgra2  29225  axcontlem5  29433  frgr3v  30763  nmoubi  31261  hvsubaddi  31555  hlimeui  31729  omlsilem  31891  pjoml3i  32075  hodsi  32264  nmopub  32397  nmfnleub  32414  nmopcoadj0i  32592  pjin3i  32683  or3dir  32945  ralcom4f  32951  rexcom4f  32952  uniinn0  33034  extdgfialglem1  34210  ordtconnlem1  34442  bnj62  35238  bnj610  35265  bnj1143  35307  bnj1533  35369  bnj543  35410  bnj545  35412  bnj594  35429  cusgracyclt3v  35743  xpab  36313  lemsuccf  36526  brfullfun  36535  in-ax8  36852  filnetlem4  37008  mh-unprimbi  37171  mh-infprim2bi  37174  bj-alnnf  37478  icorempo  38113  poimirlem13  38390  poimirlem14  38391  poimirlem21  38398  poimirlem22  38399  poimir  38410  sbccom2lem  38880  alrmomorn  39114  raldmqseu  39121  qseq  39489  dfeldisj5  39569  qmapeldisjsim  39616  mpet2  39710  isltrn2N  41001  moxfr  43545  ifporcor  44310  ifpancor  44312  ifpbicor  44323  ifpnorcor  44328  ifpnancor  44329  ifpororb  44353  minregex  44382  relexp0eq  44549  hashnzfzclim  45154  pm11.6  45224  sbc3or  45363  cbvexsv  45378  dfich2  48366  ichbi12i  48368  sprvalpwn0  48391  copisnmnd  49092  veronesevrowd  50820