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  1482  xorass  1511  cbvaldvaw  2034  sbievw2  2095  sbco4lemOLD  2171  sbco4lemOLDOLD  2276  cbvexv1  2342  cbvex  2401  sbco2d  2514  sbcom  2516  sb7f  2527  eq2tri  2801  clelsb2OLD  2867  clelsb1fw  2906  clelsb1f  2907  cbvraldva  3236  rexcom  3287  cbvrexfw  3302  cbvraldva2  3345  cbvrexdva2OLD  3347  sbralie  3355  ceqsralt  3513  gencbvex  3540  gencbval  3542  ceqsrexbv  3655  ceqsralbv  3656  euind  3732  reuind  3761  sbccomlem  3877  sbccomlemOLD  3878  sbccom  3879  csbcom  4425  difcom  4494  eqsn  4833  uniintsn  4989  disjxun  5145  reusv2lem4  5406  exss  5473  opab0  5563  opelinxp  5767  eqbrriv  5803  dm0rn0  5937  elidinxp  6063  qfto  6143  rninxp  6200  coeq0  6276  fununi  6642  dffv2  7003  fndmin  7064  fnprb  7227  fntpb  7228  dfoprab2  7490  frpoins3xp3g  8164  dfer2  8744  eceqoveq  8860  euen1  9065  xpsnen  9093  xpassen  9104  marypha2lem3  9474  rankuni  9900  card1  10005  alephislim  10120  dfacacn  10179  kmlem4  10191  ac6num  10516  zorn2lem4  10536  mappsrpr  11145  sqeqori  14249  trclublem  15030  fprodle  16028  vdwmc2  17012  txflf  24029  metustid  24582  caucfil  25330  ovolgelb  25528  dfcgra2  28852  axcontlem5  28997  frgr3v  30303  nmoubi  30800  hvsubaddi  31094  hlimeui  31268  omlsilem  31430  pjoml3i  31614  hodsi  31803  nmopub  31936  nmfnleub  31953  nmopcoadj0i  32131  pjin3i  32222  an42ds  32478  or3dir  32488  ralcom4f  32495  rexcom4f  32496  uniinn0  32570  ordtconnlem1  33884  bnj62  34712  bnj610  34739  bnj1143  34782  bnj1533  34844  bnj543  34885  bnj545  34887  bnj594  34904  cusgracyclt3v  35140  xpab  35705  brsuccf  35922  brfullfun  35929  in-ax8  36206  filnetlem4  36363  icorempo  37333  poimirlem13  37619  poimirlem14  37620  poimirlem21  37627  poimirlem22  37628  poimir  37639  sbccom2lem  38110  alrmomorn  38339  dfeldisj5  38702  mpet2  38821  isltrn2N  40102  moxfr  42679  ifporcor  43451  ifpancor  43453  ifpbicor  43464  ifpnorcor  43469  ifpnancor  43470  ifpororb  43494  minregex  43523  relexp0eq  43690  hashnzfzclim  44317  pm11.6  44387  sbc3or  44529  cbvexsv  44544  dfich2  47382  ichbi12i  47384  sprvalpwn0  47407  copisnmnd  48012