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  1485  an42ds  1491  xorass  1516  cbvaldvaw  2039  sbievw2  2103  sbco4lemOLD  2179  cbvexv1  2346  cbvex  2403  sbco2d  2516  sbcom  2518  sb7f  2529  eq2tri  2798  clelsb1fw  2902  clelsb1f  2903  cbvraldva  3216  rexcom  3265  cbvrexfw  3277  cbvraldva2  3318  sbralie  3322  sbralieOLD  3324  ceqsralt  3475  gencbvex  3499  gencbval  3501  ceqsrexbv  3610  ceqsralbv  3611  euind  3682  reuind  3711  sbccomlem  3819  sbccomlemOLD  3820  sbccom  3821  csbcom  4372  difcom  4441  eqsn  4785  uniintsn  4940  disjxun  5096  reusv2lem4  5346  exss  5411  opab0  5502  opelinxp  5704  eqbrriv  5740  dm0rn0  5873  dm0rn0OLD  5874  elidinxp  6003  qfto  6078  rninxp  6137  coeq0  6214  fununi  6567  dffv2  6929  fndmin  6990  fnprb  7154  fntpb  7155  dfoprab2  7416  frpoins3xp3g  8083  dfer2  8636  eceqoveq  8759  euen1  8964  xpsnen  8989  xpassen  8999  marypha2lem3  9340  rankuni  9775  card1  9880  alephislim  9993  dfacacn  10052  kmlem4  10064  ac6num  10389  zorn2lem4  10409  mappsrpr  11019  sqeqori  14137  trclublem  14918  fprodle  15919  vdwmc2  16907  txflf  23950  metustid  24498  caucfil  25239  ovolgelb  25437  dfcgra2  28902  axcontlem5  29041  frgr3v  30350  nmoubi  30847  hvsubaddi  31141  hlimeui  31315  omlsilem  31477  pjoml3i  31661  hodsi  31850  nmopub  31983  nmfnleub  32000  nmopcoadj0i  32178  pjin3i  32269  or3dir  32534  ralcom4f  32541  rexcom4f  32542  uniinn0  32625  extdgfialglem1  33849  ordtconnlem1  34081  bnj62  34876  bnj610  34903  bnj1143  34946  bnj1533  35008  bnj543  35049  bnj545  35051  bnj594  35068  cusgracyclt3v  35350  xpab  35920  lemsuccf  36133  brfullfun  36142  in-ax8  36418  filnetlem4  36575  bj-df-sb  36853  icorempo  37556  poimirlem13  37834  poimirlem14  37835  poimirlem21  37842  poimirlem22  37843  poimir  37854  sbccom2lem  38325  alrmomorn  38551  qseq  38907  dfeldisj5  38980  mpet2  39099  isltrn2N  40380  moxfr  42934  ifporcor  43703  ifpancor  43705  ifpbicor  43716  ifpnorcor  43721  ifpnancor  43722  ifpororb  43746  minregex  43775  relexp0eq  43942  hashnzfzclim  44563  pm11.6  44633  sbc3or  44773  cbvexsv  44788  dfich2  47704  ichbi12i  47706  sprvalpwn0  47729  copisnmnd  48415