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 206

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 207

This theorem is referenced by:  an33rean  1485  xorass  1515  cbvaldvaw  2038  sbievw2  2099  sbco4lemOLD  2175  cbvexv1  2340  cbvex  2397  sbco2d  2510  sbcom  2512  sb7f  2523  eq2tri  2791  clelsb1fw  2895  clelsb1f  2896  cbvraldva  3217  rexcom  3266  cbvrexfw  3279  cbvraldva2  3321  cbvrexdva2OLD  3323  sbralie  3326  sbralieOLD  3328  ceqsralt  3482  gencbvex  3507  gencbval  3509  ceqsrexbv  3622  ceqsralbv  3623  euind  3695  reuind  3724  sbccomlem  3832  sbccomlemOLD  3833  sbccom  3834  csbcom  4383  difcom  4452  eqsn  4793  uniintsn  4949  disjxun  5105  reusv2lem4  5356  exss  5423  opab0  5514  opelinxp  5718  eqbrriv  5754  dm0rn0  5888  elidinxp  6015  qfto  6094  rninxp  6152  coeq0  6228  fununi  6591  dffv2  6956  fndmin  7017  fnprb  7182  fntpb  7183  dfoprab2  7447  frpoins3xp3g  8120  dfer2  8672  eceqoveq  8795  euen1  8998  xpsnen  9025  xpassen  9035  marypha2lem3  9388  rankuni  9816  card1  9921  alephislim  10036  dfacacn  10095  kmlem4  10107  ac6num  10432  zorn2lem4  10452  mappsrpr  11061  sqeqori  14179  trclublem  14961  fprodle  15962  vdwmc2  16950  txflf  23893  metustid  24442  caucfil  25183  ovolgelb  25381  dfcgra2  28757  axcontlem5  28895  frgr3v  30204  nmoubi  30701  hvsubaddi  30995  hlimeui  31169  omlsilem  31331  pjoml3i  31515  hodsi  31704  nmopub  31837  nmfnleub  31854  nmopcoadj0i  32032  pjin3i  32123  an42ds  32379  or3dir  32389  ralcom4f  32396  rexcom4f  32397  uniinn0  32479  ordtconnlem1  33914  bnj62  34710  bnj610  34737  bnj1143  34780  bnj1533  34842  bnj543  34883  bnj545  34885  bnj594  34902  cusgracyclt3v  35143  xpab  35713  brsuccf  35929  brfullfun  35936  in-ax8  36212  filnetlem4  36369  icorempo  37339  poimirlem13  37627  poimirlem14  37628  poimirlem21  37635  poimirlem22  37636  poimir  37647  sbccom2lem  38118  alrmomorn  38340  qseq  38640  dfeldisj5  38713  mpet2  38832  isltrn2N  40114  moxfr  42680  ifporcor  43451  ifpancor  43453  ifpbicor  43464  ifpnorcor  43469  ifpnancor  43470  ifpororb  43494  minregex  43523  relexp0eq  43690  hashnzfzclim  44311  pm11.6  44381  sbc3or  44522  cbvexsv  44537  dfich2  47459  ichbi12i  47461  sprvalpwn0  47484  copisnmnd  48157