Theorem 3bitr3i 290

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

Syntax hints:   ↔ wb 196

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 197

This theorem is referenced by:  an12  855  xorass  1508  cbval2  2315  cbvaldva  2317  sbco2d  2444  sbcom  2446  equsb3  2460  equsb3ALT  2461  elsb3  2462  elsb4  2463  sb7f  2481  sbco4lem  2493  eq2tri  2712  eqsb3  2757  clelsb3  2758  clelsb3f  2797  r19.35  3113  ralcom4  3255  rexcom4  3256  ceqsralt  3260  gencbvex  3281  gencbval  3283  ceqsrexbv  3368  euind  3426  reuind  3444  sbccomlem  3541  sbccom  3542  csbcom  4027  difcom  4086  eqsn  4393  uniintsn  4546  disjxun  4683  reusv2lem4  4902  exss  4961  opab0  5036  elxp2OLD  5167  eqbrriv  5249  dm0rn0  5374  dfres2  5488  qfto  5552  rninxp  5608  coeq0  5682  fununi  6002  dffv2  6310  fndmin  6364  fnprb  6513  fntpb  6514  dfoprab2  6743  dfer2  7788  eceqoveq  7895  euen1  8067  xpsnen  8085  xpassen  8095  marypha2lem3  8384  rankuni  8764  card1  8832  alephislim  8944  dfacacn  9001  kmlem4  9013  ac6num  9339  zorn2lem4  9359  fpwwe2lem8  9497  fpwwe2lem12  9501  mappsrpr  9967  sqeqori  13016  trclublem  13780  fprodle  14771  vdwmc2  15730  txflf  21857  metustid  22406  caucfil  23127  ovolgelb  23294  dfcgra2  25766  axcontlem5  25893  frgr3v  27255  nmoubi  27755  hvsubaddi  28051  hlimeui  28225  omlsilem  28389  pjoml3i  28573  hodsi  28762  nmopub  28895  nmfnleub  28912  nmopcoadj0i  29090  pjin3i  29181  or3dir  29436  ralcom4f  29444  rexcom4f  29445  uniinn0  29492  ordtconnlem1  30098  bnj62  30914  bnj610  30943  bnj1143  30987  bnj1533  31048  bnj543  31089  bnj545  31091  bnj594  31108  ceqsralv2  31733  brsuccf  32173  brfullfun  32180  filnetlem4  32501  bj-ssbcom3lem  32775  bj-cbval2v  32862  bj-clelsb3  32973  icorempt2  33329  poimirlem13  33552  poimirlem14  33553  poimirlem21  33560  poimirlem22  33561  poimir  33572  sbccom2lem  34059  eldmqsres  34192  opelinxp  34251  alrmomorn  34263  xrninxp2  34291  isltrn2N  35724  moxfr  37572  ifporcor  38123  ifpancor  38125  ifpbicor  38137  ifpnorcor  38142  ifpnancor  38143  ifpororb  38167  relexp0eq  38310  hashnzfzclim  38838  pm11.6  38909  sbc3or  39055  cbvexsv  39079  sprvalpwn0  42058  copisnmnd  42134