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 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  1482  xorass  1511  cbvaldvaw  2042  sbievw2  2100  sbco4lem  2274  sbco4lemOLD  2275  cbvexv1  2340  cbval2vOLD  2342  cbvex  2400  sbco2d  2517  sbcom  2519  sb7f  2531  eq2tri  2806  clelsb2OLD  2869  clelsb1fw  2912  clelsb1f  2913  rexcom  3235  cbvrexfw  3371  cbvraldva2  3393  cbvrexdva2  3394  ceqsralt  3464  gencbvex  3489  gencbval  3491  ceqsrexbv  3587  euind  3660  reuind  3689  sbccomlem  3804  sbccom  3805  csbcom  4352  difcom  4420  eqsn  4763  uniintsn  4919  disjxun  5073  reusv2lem4  5325  exss  5379  opab0  5468  opelinxp  5667  eqbrriv  5703  dm0rn0  5837  elidinxp  5954  qfto  6031  rninxp  6087  coeq0  6163  fununi  6516  dffv2  6872  fndmin  6931  fnprb  7093  fntpb  7094  dfoprab2  7342  dfer2  8508  eceqoveq  8620  euen1  8825  xpsnen  8851  xpassen  8862  marypha2lem3  9205  rankuni  9630  card1  9735  alephislim  9848  dfacacn  9906  kmlem4  9918  ac6num  10244  zorn2lem4  10264  mappsrpr  10873  sqeqori  13939  trclublem  14715  fprodle  15715  vdwmc2  16689  txflf  23166  metustid  23719  caucfil  24456  ovolgelb  24653  dfcgra2  27200  axcontlem5  27345  frgr3v  28648  nmoubi  29143  hvsubaddi  29437  hlimeui  29611  omlsilem  29773  pjoml3i  29957  hodsi  30146  nmopub  30279  nmfnleub  30296  nmopcoadj0i  30474  pjin3i  30565  or3dir  30820  ralcom4f  30827  rexcom4f  30828  uniinn0  30899  ordtconnlem1  31883  bnj62  32708  bnj610  32736  bnj1143  32779  bnj1533  32841  bnj543  32882  bnj545  32884  bnj594  32901  cusgracyclt3v  33127  ceqsralv2  33679  xpab  33686  brsuccf  34252  brfullfun  34259  filnetlem4  34579  icorempo  35531  poimirlem13  35799  poimirlem14  35800  poimirlem21  35807  poimirlem22  35808  poimir  35819  sbccom2lem  36291  alrmomorn  36497  dfeldisj5  36839  isltrn2N  38141  moxfr  40521  ifporcor  41076  ifpancor  41078  ifpbicor  41089  ifpnorcor  41094  ifpnancor  41095  ifpororb  41119  minregex  41148  relexp0eq  41316  hashnzfzclim  41947  pm11.6  42017  sbc3or  42159  cbvexsv  42174  dfich2  44921  ichbi12i  44923  sprvalpwn0  44946  copisnmnd  45374