Theorem 3bitr3i 300

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

Syntax hints:   ↔ wb 205

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 206

This theorem is referenced by:  an33rean  1483  xorass  1514  cbvaldvaw  2041  sbievw2  2099  sbco4lem  2272  sbco4lemOLD  2273  cbvexv1  2338  cbvex  2398  sbco2d  2511  sbcom  2513  sb7f  2524  eq2tri  2799  clelsb2OLD  2862  clelsb1fw  2907  clelsb1f  2908  cbvraldva  3236  rexcom  3287  cbvrexfw  3302  cbvraldva2  3344  cbvrexdva2OLD  3346  sbralie  3354  ceqsralt  3506  gencbvex  3535  gencbval  3537  ceqsrexbv  3644  ceqsralbv  3645  euind  3720  reuind  3749  sbccomlem  3864  sbccom  3865  csbcom  4417  difcom  4488  eqsn  4832  uniintsn  4991  disjxun  5146  reusv2lem4  5399  exss  5463  opab0  5554  opelinxp  5755  eqbrriv  5791  dm0rn0  5924  elidinxp  6043  qfto  6122  rninxp  6178  coeq0  6254  fununi  6623  dffv2  6986  fndmin  7046  fnprb  7212  fntpb  7213  dfoprab2  7469  frpoins3xp3g  8129  dfer2  8706  eceqoveq  8818  euen1  9028  xpsnen  9057  xpassen  9068  marypha2lem3  9434  rankuni  9860  card1  9965  alephislim  10080  dfacacn  10138  kmlem4  10150  ac6num  10476  zorn2lem4  10496  mappsrpr  11105  sqeqori  14180  trclublem  14944  fprodle  15942  vdwmc2  16914  txflf  23517  metustid  24070  caucfil  24807  ovolgelb  25004  dfcgra2  28119  axcontlem5  28264  frgr3v  29566  nmoubi  30063  hvsubaddi  30357  hlimeui  30531  omlsilem  30693  pjoml3i  30877  hodsi  31066  nmopub  31199  nmfnleub  31216  nmopcoadj0i  31394  pjin3i  31485  or3dir  31740  ralcom4f  31747  rexcom4f  31748  uniinn0  31820  ordtconnlem1  32973  bnj62  33800  bnj610  33827  bnj1143  33870  bnj1533  33932  bnj543  33973  bnj545  33975  bnj594  33992  cusgracyclt3v  34216  xpab  34764  brsuccf  34982  brfullfun  34989  filnetlem4  35352  icorempo  36318  poimirlem13  36587  poimirlem14  36588  poimirlem21  36595  poimirlem22  36596  poimir  36607  sbccom2lem  37078  alrmomorn  37313  dfeldisj5  37677  mpet2  37796  isltrn2N  39077  moxfr  41512  ifporcor  42295  ifpancor  42297  ifpbicor  42308  ifpnorcor  42313  ifpnancor  42314  ifpororb  42338  minregex  42367  relexp0eq  42534  hashnzfzclim  43163  pm11.6  43233  sbc3or  43375  cbvexsv  43390  dfich2  46205  ichbi12i  46207  sprvalpwn0  46230  copisnmnd  46658