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 205

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 206

This theorem is referenced by:  an33rean  1484  xorass  1515  cbvaldvaw  2042  sbievw2  2100  sbco4lem  2273  sbco4lemOLD  2274  cbvexv1  2339  cbvex  2399  sbco2d  2512  sbcom  2514  sb7f  2525  eq2tri  2800  clelsb2OLD  2863  clelsb1fw  2908  clelsb1f  2909  cbvraldva  3237  rexcom  3288  cbvrexfw  3303  cbvraldva2  3345  cbvrexdva2OLD  3347  sbralie  3355  ceqsralt  3507  gencbvex  3536  gencbval  3538  ceqsrexbv  3645  ceqsralbv  3646  euind  3721  reuind  3750  sbccomlem  3865  sbccom  3866  csbcom  4418  difcom  4489  eqsn  4833  uniintsn  4992  disjxun  5147  reusv2lem4  5400  exss  5464  opab0  5555  opelinxp  5756  eqbrriv  5792  dm0rn0  5925  elidinxp  6044  qfto  6123  rninxp  6179  coeq0  6255  fununi  6624  dffv2  6987  fndmin  7047  fnprb  7210  fntpb  7211  dfoprab2  7467  frpoins3xp3g  8127  dfer2  8704  eceqoveq  8816  euen1  9026  xpsnen  9055  xpassen  9066  marypha2lem3  9432  rankuni  9858  card1  9963  alephislim  10078  dfacacn  10136  kmlem4  10148  ac6num  10474  zorn2lem4  10494  mappsrpr  11103  sqeqori  14178  trclublem  14942  fprodle  15940  vdwmc2  16912  txflf  23510  metustid  24063  caucfil  24800  ovolgelb  24997  dfcgra2  28081  axcontlem5  28226  frgr3v  29528  nmoubi  30025  hvsubaddi  30319  hlimeui  30493  omlsilem  30655  pjoml3i  30839  hodsi  31028  nmopub  31161  nmfnleub  31178  nmopcoadj0i  31356  pjin3i  31447  or3dir  31702  ralcom4f  31709  rexcom4f  31710  uniinn0  31782  ordtconnlem1  32904  bnj62  33731  bnj610  33758  bnj1143  33801  bnj1533  33863  bnj543  33904  bnj545  33906  bnj594  33923  cusgracyclt3v  34147  xpab  34695  brsuccf  34913  brfullfun  34920  filnetlem4  35266  icorempo  36232  poimirlem13  36501  poimirlem14  36502  poimirlem21  36509  poimirlem22  36510  poimir  36521  sbccom2lem  36992  alrmomorn  37227  dfeldisj5  37591  mpet2  37710  isltrn2N  38991  moxfr  41430  ifporcor  42213  ifpancor  42215  ifpbicor  42226  ifpnorcor  42231  ifpnancor  42232  ifpororb  42256  minregex  42285  relexp0eq  42452  hashnzfzclim  43081  pm11.6  43151  sbc3or  43293  cbvexsv  43308  dfich2  46126  ichbi12i  46128  sprvalpwn0  46151  copisnmnd  46579