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  2044  sbievw2  2106  sbco4lem  2282  cbval2vOLD  2363  cbvex  2416  cbvexvOLD  2420  cbval2OLD  2432  sbco2d  2553  sbcom  2555  sb7f  2567  sb7fALT  2615  eq2tri  2886  clelsb3vOLD  2944  clelsb3fw  2984  clelsb3f  2985  clelsb3fOLD  2986  cbvraldva2  3459  cbvrexdva2  3460  cbvrexdva2OLD  3461  ralcom4OLD  3528  rexcom4OLD  3529  ceqsralt  3531  gencbvex  3552  gencbval  3554  ceqsrexbv  3653  euind  3718  reuind  3747  sbccomlem  3856  sbccom  3857  csbcom  4372  difcom  4437  eqsn  4765  uniintsn  4916  disjxun  5067  reusv2lem4  5305  exss  5358  opab0  5444  opelinxp  5634  eqbrriv  5667  dm0rn0  5798  elidinxp  5914  qfto  5984  rninxp  6039  coeq0  6111  fununi  6432  dffv2  6759  fndmin  6818  fnprb  6974  fntpb  6975  dfoprab2  7215  dfer2  8293  eceqoveq  8405  euen1  8582  xpsnen  8604  xpassen  8614  marypha2lem3  8904  rankuni  9295  card1  9400  alephislim  9512  dfacacn  9570  kmlem4  9582  ac6num  9904  zorn2lem4  9924  mappsrpr  10533  sqeqori  13579  trclublem  14358  fprodle  15353  vdwmc2  16318  txflf  22617  metustid  23167  caucfil  23889  ovolgelb  24084  dfcgra2  26619  axcontlem5  26757  frgr3v  28057  nmoubi  28552  hvsubaddi  28846  hlimeui  29020  omlsilem  29182  pjoml3i  29366  hodsi  29555  nmopub  29688  nmfnleub  29705  nmopcoadj0i  29883  pjin3i  29974  or3dir  30229  ralcom4f  30236  rexcom4f  30237  uniinn0  30305  ordtconnlem1  31171  bnj62  31994  bnj610  32022  bnj1143  32066  bnj1533  32128  bnj543  32169  bnj545  32171  bnj594  32188  cusgracyclt3v  32407  ceqsralv2  32960  brsuccf  33406  brfullfun  33413  filnetlem4  33733  icorempo  34636  poimirlem13  34909  poimirlem14  34910  poimirlem21  34917  poimirlem22  34918  poimir  34929  sbccom2lem  35406  alrmomorn  35616  dfeldisj5  35958  isltrn2N  37260  moxfr  39295  ifporcor  39833  ifpancor  39835  ifpbicor  39847  ifpnorcor  39852  ifpnancor  39853  ifpororb  39877  relexp0eq  40052  hashnzfzclim  40660  pm11.6  40730  sbc3or  40872  cbvexsv  40887  dfich2  43620  ichbi12i  43625  sprvalpwn0  43652  copisnmnd  44083