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

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  an33rean  1514  an42ds  1520  xorass  1545  cbvaldvaw  2071  sbievw2  2135  cbvexv1  2372  cbvex  2429  sbco2d  2542  sbcom  2544  sb7f  2555  eq2tri  2823  clelsb1fw  2927  clelsb1f  2928  cbvraldva  3243  rexcom  3292  cbvrexfw  3304  sbralie  3339  sbralieOLD  3341  ceqsralt  3485  gencbvex  3507  gencbval  3509  ceqsrexbv  3610  ceqsralbv  3611  euind  3682  reuind  3711  sbccomlem  3817  sbccom  3818  csbcom  4378  difcom  4444  eqsn  4790  uniintsn  4945  disjxun  5101  reusv2lem4  5363  exss  5431  eqvinot  5457  opab0  5529  opelinxp  5731  eqbrriv  5767  dm0rn0  5906  dm0rn0OLD  5907  elidinxp  6038  qfto  6113  xpdifcnvepel  6159  rninxp  6170  coeq0  6250  fununi  6607  dffv2  6972  fndmin  7036  fnprb  7206  fntpb  7207  dfoprab2  7470  frpoins3xp3g  8142  dfer2  8702  eceqoveq  8827  euen1  9038  xpsnen  9064  xpassen  9074  marypha2lem3  9413  rankuni  9860  card1  10030  alephislim  10143  dfacacn  10201  kmlem4  10213  ac6num  10538  zorn2lem4  10558  mappsrpr  11174  sqeqori  14338  trclublem  15128  fprodle  16143  vdwmc2  17137  txflf  24305  metustid  24853  caucfil  25584  ovolgelb  25781  dfcgra2  29320  axcontlem5  29528  frgr3v  30858  nmoubi  31356  hvsubaddi  31650  hlimeui  31824  omlsilem  31986  pjoml3i  32170  hodsi  32359  nmopub  32492  nmfnleub  32509  nmopcoadj0i  32687  pjin3i  32778  or3dir  33040  ralcom4f  33046  rexcom4f  33047  uniinn0  33129  extdgfialglem1  34306  ordtconnlem1  34538  bnj62  35334  bnj610  35361  bnj1143  35403  bnj1533  35465  bnj543  35506  bnj545  35508  bnj594  35525  r1omhf  35710  cusgracyclt3v  35890  xpab  36460  lemsuccf  36673  brfullfun  36682  in-ax8  36983  filnetlem4  37139  mh-unprimbi  37302  mh-infprim2bi  37305  bj-alnnf  37609  icorempo  38242  poimirlem13  38519  poimirlem14  38520  poimirlem21  38527  poimirlem22  38528  poimir  38539  sbccom2lem  39024  alrmomorn  39258  raldmqseu  39265  qseq  39633  dfeldisj5  39713  qmapeldisjsim  39760  mpet2  39854  isltrn2N  41145  moxfr  43656  ifporcor  44421  ifpancor  44423  ifpbicor  44434  ifpnorcor  44439  ifpnancor  44440  ifpororb  44464  minregex  44493  relexp0eq  44660  hashnzfzclim  45265  pm11.6  45335  sbc3or  45474  cbvexsv  45489  dfich2  48484  ichbi12i  48486  sprvalpwn0  48509  copisnmnd  49210  veronesevrowd  50923