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  2344  cbvex  2401  sbco2d  2514  sbcom  2516  sb7f  2527  eq2tri  2795  clelsb1fw  2899  clelsb1f  2900  cbvraldva  3213  rexcom  3262  cbvrexfw  3274  cbvraldva2  3315  sbralie  3319  sbralieOLD  3321  ceqsralt  3472  gencbvex  3496  gencbval  3498  ceqsrexbv  3607  ceqsralbv  3608  euind  3679  reuind  3708  sbccomlem  3816  sbccomlemOLD  3817  sbccom  3818  csbcom  4369  difcom  4438  eqsn  4782  uniintsn  4937  disjxun  5093  reusv2lem4  5343  exss  5408  opab0  5499  opelinxp  5701  eqbrriv  5737  dm0rn0  5870  dm0rn0OLD  5871  elidinxp  5999  qfto  6074  rninxp  6133  coeq0  6210  fununi  6563  dffv2  6925  fndmin  6986  fnprb  7150  fntpb  7151  dfoprab2  7412  frpoins3xp3g  8079  dfer2  8631  eceqoveq  8754  euen1  8958  xpsnen  8983  xpassen  8993  marypha2lem3  9330  rankuni  9765  card1  9870  alephislim  9983  dfacacn  10042  kmlem4  10054  ac6num  10379  zorn2lem4  10399  mappsrpr  11008  sqeqori  14125  trclublem  14906  fprodle  15907  vdwmc2  16895  txflf  23924  metustid  24472  caucfil  25213  ovolgelb  25411  dfcgra2  28811  axcontlem5  28950  frgr3v  30259  nmoubi  30756  hvsubaddi  31050  hlimeui  31224  omlsilem  31386  pjoml3i  31570  hodsi  31759  nmopub  31892  nmfnleub  31909  nmopcoadj0i  32087  pjin3i  32178  or3dir  32443  ralcom4f  32450  rexcom4f  32451  uniinn0  32534  extdgfialglem1  33728  ordtconnlem1  33960  bnj62  34755  bnj610  34782  bnj1143  34825  bnj1533  34887  bnj543  34928  bnj545  34930  bnj594  34947  cusgracyclt3v  35223  xpab  35793  lemsuccf  36006  brfullfun  36015  in-ax8  36291  filnetlem4  36448  icorempo  37418  poimirlem13  37696  poimirlem14  37697  poimirlem21  37704  poimirlem22  37705  poimir  37716  sbccom2lem  38187  alrmomorn  38413  qseq  38769  dfeldisj5  38842  mpet2  38961  isltrn2N  40242  moxfr  42812  ifporcor  43582  ifpancor  43584  ifpbicor  43595  ifpnorcor  43600  ifpnancor  43601  ifpororb  43625  minregex  43654  relexp0eq  43821  hashnzfzclim  44442  pm11.6  44512  sbc3or  44652  cbvexsv  44667  dfich2  47585  ichbi12i  47587  sprvalpwn0  47610  copisnmnd  48296