Theorem 3bitr3i 303

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

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  an33rean  1479  xorass  1506  cbvaldvaw  2045  sbievw2  2107  sbco4lem  2283  cbval2vOLD  2364  cbvex  2417  cbvexvOLD  2421  cbval2OLD  2433  sbco2d  2554  sbcom  2556  sb7f  2568  sb7fALT  2616  eq2tri  2883  clelsb3vOLD  2941  clelsb3fw  2981  clelsb3f  2982  clelsb3fOLD  2983  cbvraldva2  3456  cbvrexdva2  3457  cbvrexdva2OLD  3458  ralcom4OLD  3525  rexcom4OLD  3526  ceqsralt  3528  gencbvex  3549  gencbval  3551  ceqsrexbv  3650  euind  3715  reuind  3744  sbccomlem  3853  sbccom  3854  csbcom  4369  difcom  4434  eqsn  4762  uniintsn  4913  disjxun  5064  reusv2lem4  5302  exss  5355  opab0  5441  opelinxp  5631  eqbrriv  5664  dm0rn0  5795  elidinxp  5911  qfto  5981  rninxp  6036  coeq0  6108  fununi  6429  dffv2  6756  fndmin  6815  fnprb  6971  fntpb  6972  dfoprab2  7212  dfer2  8290  eceqoveq  8402  euen1  8579  xpsnen  8601  xpassen  8611  marypha2lem3  8901  rankuni  9292  card1  9397  alephislim  9509  dfacacn  9567  kmlem4  9579  ac6num  9901  zorn2lem4  9921  mappsrpr  10530  sqeqori  13577  trclublem  14355  fprodle  15350  vdwmc2  16315  txflf  22614  metustid  23164  caucfil  23886  ovolgelb  24081  dfcgra2  26616  axcontlem5  26754  frgr3v  28054  nmoubi  28549  hvsubaddi  28843  hlimeui  29017  omlsilem  29179  pjoml3i  29363  hodsi  29552  nmopub  29685  nmfnleub  29702  nmopcoadj0i  29880  pjin3i  29971  or3dir  30226  ralcom4f  30233  rexcom4f  30234  uniinn0  30302  ordtconnlem1  31167  bnj62  31990  bnj610  32018  bnj1143  32062  bnj1533  32124  bnj543  32165  bnj545  32167  bnj594  32184  cusgracyclt3v  32403  ceqsralv2  32956  brsuccf  33402  brfullfun  33409  filnetlem4  33729  icorempo  34635  poimirlem13  34920  poimirlem14  34921  poimirlem21  34928  poimirlem22  34929  poimir  34940  sbccom2lem  35417  alrmomorn  35627  dfeldisj5  35969  isltrn2N  37271  moxfr  39309  ifporcor  39847  ifpancor  39849  ifpbicor  39861  ifpnorcor  39866  ifpnancor  39867  ifpororb  39891  relexp0eq  40066  hashnzfzclim  40674  pm11.6  40744  sbc3or  40886  cbvexsv  40901  dfich2  43633  ichbi12i  43638  sprvalpwn0  43665  copisnmnd  44096