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  1486  an42ds  1492  xorass  1517  cbvaldvaw  2040  sbievw2  2104  sbco4lemOLD  2180  cbvexv1  2347  cbvex  2404  sbco2d  2517  sbcom  2519  sb7f  2530  eq2tri  2799  clelsb1fw  2903  clelsb1f  2904  cbvraldva  3218  rexcom  3267  cbvrexfw  3279  sbralie  3316  sbralieOLD  3318  ceqsralt  3465  gencbvex  3488  gencbval  3490  ceqsrexbv  3599  ceqsralbv  3600  euind  3671  reuind  3700  sbccomlem  3808  sbccomlemOLD  3809  sbccom  3810  csbcom  4361  difcom  4429  eqsn  4773  uniintsn  4928  disjxun  5084  reusv2lem4  5338  exss  5410  opab0  5502  opelinxp  5704  eqbrriv  5740  dm0rn0  5873  dm0rn0OLD  5874  elidinxp  6003  qfto  6078  rninxp  6137  coeq0  6214  fununi  6567  dffv2  6929  fndmin  6991  fnprb  7156  fntpb  7157  dfoprab2  7418  frpoins3xp3g  8084  dfer2  8637  eceqoveq  8762  euen1  8967  xpsnen  8992  xpassen  9002  marypha2lem3  9343  rankuni  9778  card1  9883  alephislim  9996  dfacacn  10055  kmlem4  10067  ac6num  10392  zorn2lem4  10412  mappsrpr  11022  sqeqori  14167  trclublem  14948  fprodle  15952  vdwmc2  16941  txflf  23981  metustid  24529  caucfil  25260  ovolgelb  25457  dfcgra2  28912  axcontlem5  29051  frgr3v  30360  nmoubi  30858  hvsubaddi  31152  hlimeui  31326  omlsilem  31488  pjoml3i  31672  hodsi  31861  nmopub  31994  nmfnleub  32011  nmopcoadj0i  32189  pjin3i  32280  or3dir  32544  ralcom4f  32551  rexcom4f  32552  uniinn0  32635  extdgfialglem1  33852  ordtconnlem1  34084  bnj62  34879  bnj610  34906  bnj1143  34948  bnj1533  35010  bnj543  35051  bnj545  35053  bnj594  35070  cusgracyclt3v  35354  xpab  35924  lemsuccf  36137  brfullfun  36146  in-ax8  36422  filnetlem4  36579  mh-unprimbi  36742  mh-infprim2bi  36745  bj-alnnf  37050  icorempo  37681  poimirlem13  37968  poimirlem14  37969  poimirlem21  37976  poimirlem22  37977  poimir  37988  sbccom2lem  38459  alrmomorn  38693  raldmqseu  38700  qseq  39068  dfeldisj5  39148  qmapeldisjsim  39195  mpet2  39289  isltrn2N  40580  moxfr  43138  ifporcor  43907  ifpancor  43909  ifpbicor  43920  ifpnorcor  43925  ifpnancor  43926  ifpororb  43950  minregex  43979  relexp0eq  44146  hashnzfzclim  44767  pm11.6  44837  sbc3or  44977  cbvexsv  44992  dfich2  47930  ichbi12i  47932  sprvalpwn0  47955  copisnmnd  48657