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  2398  sbco2d  2511  sbcom  2513  sb7f  2524  eq2tri  2792  clelsb1fw  2896  clelsb1f  2897  cbvraldva  3218  rexcom  3267  cbvrexfw  3281  cbvraldva2  3323  cbvrexdva2OLD  3325  sbralie  3328  sbralieOLD  3330  ceqsralt  3485  gencbvex  3510  gencbval  3512  ceqsrexbv  3625  ceqsralbv  3626  euind  3698  reuind  3727  sbccomlem  3835  sbccomlemOLD  3836  sbccom  3837  csbcom  4386  difcom  4455  eqsn  4796  uniintsn  4952  disjxun  5108  reusv2lem4  5359  exss  5426  opab0  5517  opelinxp  5721  eqbrriv  5757  dm0rn0  5891  elidinxp  6018  qfto  6097  rninxp  6155  coeq0  6231  fununi  6594  dffv2  6959  fndmin  7020  fnprb  7185  fntpb  7186  dfoprab2  7450  frpoins3xp3g  8123  dfer2  8675  eceqoveq  8798  euen1  9001  xpsnen  9029  xpassen  9040  marypha2lem3  9395  rankuni  9823  card1  9928  alephislim  10043  dfacacn  10102  kmlem4  10114  ac6num  10439  zorn2lem4  10459  mappsrpr  11068  sqeqori  14186  trclublem  14968  fprodle  15969  vdwmc2  16957  txflf  23900  metustid  24449  caucfil  25190  ovolgelb  25388  dfcgra2  28764  axcontlem5  28902  frgr3v  30211  nmoubi  30708  hvsubaddi  31002  hlimeui  31176  omlsilem  31338  pjoml3i  31522  hodsi  31711  nmopub  31844  nmfnleub  31861  nmopcoadj0i  32039  pjin3i  32130  an42ds  32386  or3dir  32396  ralcom4f  32403  rexcom4f  32404  uniinn0  32486  ordtconnlem1  33921  bnj62  34717  bnj610  34744  bnj1143  34787  bnj1533  34849  bnj543  34890  bnj545  34892  bnj594  34909  cusgracyclt3v  35150  xpab  35720  brsuccf  35936  brfullfun  35943  in-ax8  36219  filnetlem4  36376  icorempo  37346  poimirlem13  37634  poimirlem14  37635  poimirlem21  37642  poimirlem22  37643  poimir  37654  sbccom2lem  38125  alrmomorn  38347  qseq  38647  dfeldisj5  38720  mpet2  38839  isltrn2N  40121  moxfr  42687  ifporcor  43458  ifpancor  43460  ifpbicor  43471  ifpnorcor  43476  ifpnancor  43477  ifpororb  43501  minregex  43530  relexp0eq  43697  hashnzfzclim  44318  pm11.6  44388  sbc3or  44529  cbvexsv  44544  dfich2  47463  ichbi12i  47465  sprvalpwn0  47488  copisnmnd  48161