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

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  an33rean  1514  an42ds  1520  xorass  1545  cbvaldvaw  2068  sbievw2  2133  sbco4lemOLD  2208  cbvexv1  2374  cbvex  2431  sbco2d  2544  sbcom  2546  sb7f  2557  eq2tri  2825  clelsb1fw  2929  clelsb1f  2930  cbvraldva  3245  rexcom  3294  cbvrexfw  3306  sbralie  3342  sbralieOLD  3344  ceqsralt  3489  gencbvex  3511  gencbval  3513  ceqsrexbv  3616  ceqsralbv  3617  euind  3688  reuind  3717  sbccomlem  3823  sbccomlemOLD  3824  sbccom  3825  csbcom  4386  difcom  4450  eqsn  4796  uniintsn  4951  disjxun  5108  reusv2lem4  5374  exss  5446  opab0  5541  opelinxp  5743  eqbrriv  5779  dm0rn0  5916  dm0rn0OLD  5917  elidinxp  6048  qfto  6123  xpdifcnvepel  6168  rninxp  6179  coeq0  6259  fununi  6613  dffv2  6978  fndmin  7042  fnprb  7208  fntpb  7209  dfoprab2  7470  frpoins3xp3g  8138  dfer2  8696  eceqoveq  8821  euen1  9025  xpsnen  9050  xpassen  9060  marypha2lem3  9398  rankuni  9836  card1  9955  alephislim  10068  dfacacn  10126  kmlem4  10138  ac6num  10464  zorn2lem4  10484  mappsrpr  11094  sqeqori  14252  trclublem  15034  fprodle  16052  vdwmc2  17040  txflf  24144  metustid  24692  caucfil  25423  ovolgelb  25620  dfcgra2  29122  axcontlem5  29299  frgr3v  30607  nmoubi  31105  hvsubaddi  31399  hlimeui  31573  omlsilem  31735  pjoml3i  31919  hodsi  32108  nmopub  32241  nmfnleub  32258  nmopcoadj0i  32436  pjin3i  32527  or3dir  32789  ralcom4f  32795  rexcom4f  32796  uniinn0  32878  extdgfialglem1  34063  ordtconnlem1  34295  bnj62  35090  bnj610  35117  bnj1143  35159  bnj1533  35221  bnj543  35262  bnj545  35264  bnj594  35281  cusgracyclt3v  35629  xpab  36199  lemsuccf  36412  brfullfun  36421  in-ax8  36717  filnetlem4  36873  mh-unprimbi  37036  mh-infprim2bi  37039  bj-alnnf  37343  icorempo  37978  poimirlem13  38265  poimirlem14  38266  poimirlem21  38273  poimirlem22  38274  poimir  38285  sbccom2lem  38754  alrmomorn  38988  raldmqseu  38995  qseq  39363  dfeldisj5  39443  qmapeldisjsim  39490  mpet2  39584  isltrn2N  40875  moxfr  43406  ifporcor  44171  ifpancor  44173  ifpbicor  44184  ifpnorcor  44189  ifpnancor  44190  ifpororb  44214  minregex  44243  relexp0eq  44410  hashnzfzclim  45015  pm11.6  45085  sbc3or  45224  cbvexsv  45239  dfich2  48190  ichbi12i  48192  sprvalpwn0  48215  copisnmnd  48917