Theorem 3bitr3i 303

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 279	. 2 ⊢ (𝜒 ↔ 𝜓)
4		3bitr3i.3	. 2 ⊢ (𝜓 ↔ 𝜃)
5	3, 4	bitri 277	1 ⊢ (𝜒 ↔ 𝜃)

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  an33rean  1503  an42ds  1509  xorass  1534  cbvaldvaw  2057  sbievw2  2131  sbco4lemOLD  2206  cbvexv1  2372  cbvex  2429  sbco2d  2542  sbcom  2544  sb7f  2555  eq2tri  2823  clelsb1fw  2927  clelsb1f  2928  cbvraldva  3241  rexcom  3290  cbvrexfw  3302  sbralie  3339  sbralieOLD  3341  ceqsralt  3487  gencbvex  3509  gencbval  3511  ceqsrexbv  3615  ceqsralbv  3616  euind  3686  reuind  3715  sbccomlem  3822  sbccomlemOLD  3823  sbccom  3824  csbcom  4373  difcom  4441  eqsn  4786  uniintsn  4942  disjxun  5097  reusv2lem4  5357  exss  5429  opab0  5523  opelinxp  5725  eqbrriv  5761  dm0rn0  5898  dm0rn0OLD  5899  elidinxp  6030  qfto  6105  rninxp  6161  coeq0  6239  fununi  6592  dffv2  6958  fndmin  7022  fnprb  7188  fntpb  7189  dfoprab2  7450  frpoins3xp3g  8116  dfer2  8674  eceqoveq  8799  euen1  9004  xpsnen  9029  xpassen  9039  marypha2lem3  9380  rankuni  9818  card1  9923  alephislim  10036  dfacacn  10095  kmlem4  10107  ac6num  10433  zorn2lem4  10453  mappsrpr  11063  sqeqori  14224  trclublem  15005  fprodle  16009  vdwmc2  16998  txflf  24046  metustid  24594  caucfil  25325  ovolgelb  25522  dfcgra2  28976  axcontlem5  29115  frgr3v  30423  nmoubi  30921  hvsubaddi  31215  hlimeui  31389  omlsilem  31551  pjoml3i  31735  hodsi  31924  nmopub  32057  nmfnleub  32074  nmopcoadj0i  32252  pjin3i  32343  or3dir  32607  ralcom4f  32614  rexcom4f  32615  uniinn0  32699  extdgfialglem1  33950  ordtconnlem1  34182  bnj62  34980  bnj610  35007  bnj1143  35049  bnj1533  35111  bnj543  35152  bnj545  35154  bnj594  35171  cusgracyclt3v  35470  xpab  36040  lemsuccf  36253  brfullfun  36262  in-ax8  36548  filnetlem4  36705  mh-unprimbi  36868  mh-infprim2bi  36871  bj-alnnf  37176  icorempo  37809  poimirlem13  38096  poimirlem14  38097  poimirlem21  38104  poimirlem22  38105  poimir  38116  sbccom2lem  38587  alrmomorn  38821  raldmqseu  38828  qseq  39196  dfeldisj5  39276  qmapeldisjsim  39323  mpet2  39417  isltrn2N  40708  moxfr  43237  ifporcor  44002  ifpancor  44004  ifpbicor  44015  ifpnorcor  44020  ifpnancor  44021  ifpororb  44045  minregex  44074  relexp0eq  44241  hashnzfzclim  44862  pm11.6  44932  sbc3or  45072  cbvexsv  45087  dfich2  48028  ichbi12i  48030  sprvalpwn0  48053  copisnmnd  48755