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  3643  ceqsralbv  3644  euind  3719  reuind  3748  sbccomlem  3863  sbccom  3864  csbcom  4416  difcom  4487  eqsn  4831  uniintsn  4990  disjxun  5145  reusv2lem4  5398  exss  5462  opab0  5553  opelinxp  5753  eqbrriv  5789  dm0rn0  5922  elidinxp  6041  qfto  6119  rninxp  6175  coeq0  6251  fununi  6620  dffv2  6983  fndmin  7043  fnprb  7206  fntpb  7207  dfoprab2  7463  frpoins3xp3g  8123  dfer2  8700  eceqoveq  8812  euen1  9022  xpsnen  9051  xpassen  9062  marypha2lem3  9428  rankuni  9854  card1  9959  alephislim  10074  dfacacn  10132  kmlem4  10144  ac6num  10470  zorn2lem4  10490  mappsrpr  11099  sqeqori  14174  trclublem  14938  fprodle  15936  vdwmc2  16908  txflf  23501  metustid  24054  caucfil  24791  ovolgelb  24988  dfcgra2  28070  axcontlem5  28215  frgr3v  29517  nmoubi  30012  hvsubaddi  30306  hlimeui  30480  omlsilem  30642  pjoml3i  30826  hodsi  31015  nmopub  31148  nmfnleub  31165  nmopcoadj0i  31343  pjin3i  31434  or3dir  31689  ralcom4f  31696  rexcom4f  31697  uniinn0  31769  ordtconnlem1  32892  bnj62  33719  bnj610  33746  bnj1143  33789  bnj1533  33851  bnj543  33892  bnj545  33894  bnj594  33911  cusgracyclt3v  34135  xpab  34683  brsuccf  34901  brfullfun  34908  filnetlem4  35254  icorempo  36220  poimirlem13  36489  poimirlem14  36490  poimirlem21  36497  poimirlem22  36498  poimir  36509  sbccom2lem  36980  alrmomorn  37215  dfeldisj5  37579  mpet2  37698  isltrn2N  38979  moxfr  41415  ifporcor  42198  ifpancor  42200  ifpbicor  42211  ifpnorcor  42216  ifpnancor  42217  ifpororb  42241  minregex  42270  relexp0eq  42437  hashnzfzclim  43066  pm11.6  43136  sbc3or  43278  cbvexsv  43293  dfich2  46112  ichbi12i  46114  sprvalpwn0  46137  copisnmnd  46565