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 ⊢ (𝜒 ↔ 𝜃)

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  an33rean  1507  an42ds  1513  xorass  1538  cbvaldvaw  2061  sbievw2  2135  sbco4lemOLD  2210  cbvexv1  2376  cbvex  2433  sbco2d  2546  sbcom  2548  sb7f  2559  eq2tri  2827  clelsb1fw  2931  clelsb1f  2932  cbvraldva  3245  rexcom  3294  cbvrexfw  3306  sbralie  3343  sbralieOLD  3345  ceqsralt  3491  gencbvex  3513  gencbval  3515  ceqsrexbv  3618  ceqsralbv  3619  euind  3690  reuind  3719  sbccomlem  3825  sbccomlemOLD  3826  sbccom  3827  csbcom  4377  difcom  4445  eqsn  4790  uniintsn  4945  disjxun  5102  reusv2lem4  5362  exss  5434  opab0  5529  opelinxp  5731  eqbrriv  5767  dm0rn0  5904  dm0rn0OLD  5905  elidinxp  6036  qfto  6111  xpdifcnvepel  6157  rninxp  6168  coeq0  6246  fununi  6600  dffv2  6966  fndmin  7030  fnprb  7196  fntpb  7197  dfoprab2  7458  frpoins3xp3g  8125  dfer2  8683  eceqoveq  8808  euen1  9012  xpsnen  9037  xpassen  9047  marypha2lem3  9385  rankuni  9823  card1  9942  alephislim  10055  dfacacn  10113  kmlem4  10125  ac6num  10451  zorn2lem4  10471  mappsrpr  11081  sqeqori  14238  trclublem  15020  fprodle  16038  vdwmc2  17027  txflf  24120  metustid  24668  caucfil  25399  ovolgelb  25596  dfcgra2  29078  axcontlem5  29223  frgr3v  30531  nmoubi  31029  hvsubaddi  31323  hlimeui  31497  omlsilem  31659  pjoml3i  31843  hodsi  32032  nmopub  32165  nmfnleub  32182  nmopcoadj0i  32360  pjin3i  32451  or3dir  32713  ralcom4f  32720  rexcom4f  32721  uniinn0  32803  extdgfialglem1  33994  ordtconnlem1  34226  bnj62  35021  bnj610  35048  bnj1143  35090  bnj1533  35152  bnj543  35193  bnj545  35195  bnj594  35212  cusgracyclt3v  35514  xpab  36084  lemsuccf  36297  brfullfun  36306  in-ax8  36592  filnetlem4  36749  mh-unprimbi  36912  mh-infprim2bi  36915  bj-alnnf  37219  icorempo  37852  poimirlem13  38139  poimirlem14  38140  poimirlem21  38147  poimirlem22  38148  poimir  38159  sbccom2lem  38630  alrmomorn  38864  raldmqseu  38871  qseq  39239  dfeldisj5  39319  qmapeldisjsim  39366  mpet2  39460  isltrn2N  40751  moxfr  43280  ifporcor  44045  ifpancor  44047  ifpbicor  44058  ifpnorcor  44063  ifpnancor  44064  ifpororb  44088  minregex  44117  relexp0eq  44284  hashnzfzclim  44891  pm11.6  44961  sbc3or  45100  cbvexsv  45115  dfich2  48063  ichbi12i  48065  sprvalpwn0  48088  copisnmnd  48790