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  1481  xorass  1508  cbvaldvaw  2042  sbievw2  2101  sbco4lem  2276  sbco4lemOLD  2277  cbvexv1  2341  cbval2vOLD  2343  cbvex  2399  sbco2d  2516  sbcom  2518  sb7f  2530  eq2tri  2806  clelsb2  2867  clelsb1fw  2910  clelsb1f  2911  cbvraldva2  3381  cbvrexdva2  3382  ceqsralt  3453  gencbvex  3478  gencbval  3480  ceqsrexbv  3579  euind  3654  reuind  3683  sbccomlem  3799  sbccom  3800  csbcom  4348  difcom  4416  eqsn  4759  uniintsn  4915  disjxun  5068  reusv2lem4  5319  exss  5372  opab0  5460  opelinxp  5657  eqbrriv  5690  dm0rn0  5823  elidinxp  5940  qfto  6015  rninxp  6071  coeq0  6148  fununi  6493  dffv2  6845  fndmin  6904  fnprb  7066  fntpb  7067  dfoprab2  7311  dfer2  8457  eceqoveq  8569  euen1  8770  xpsnen  8796  xpassen  8806  marypha2lem3  9126  rankuni  9552  card1  9657  alephislim  9770  dfacacn  9828  kmlem4  9840  ac6num  10166  zorn2lem4  10186  mappsrpr  10795  sqeqori  13858  trclublem  14634  fprodle  15634  vdwmc2  16608  txflf  23065  metustid  23616  caucfil  24352  ovolgelb  24549  dfcgra2  27095  axcontlem5  27239  frgr3v  28540  nmoubi  29035  hvsubaddi  29329  hlimeui  29503  omlsilem  29665  pjoml3i  29849  hodsi  30038  nmopub  30171  nmfnleub  30188  nmopcoadj0i  30366  pjin3i  30457  or3dir  30712  ralcom4f  30719  rexcom4f  30720  uniinn0  30791  ordtconnlem1  31776  bnj62  32599  bnj610  32627  bnj1143  32670  bnj1533  32732  bnj543  32773  bnj545  32775  bnj594  32792  cusgracyclt3v  33018  ceqsralv2  33572  xpab  33579  brsuccf  34170  brfullfun  34177  filnetlem4  34497  icorempo  35449  poimirlem13  35717  poimirlem14  35718  poimirlem21  35725  poimirlem22  35726  poimir  35737  sbccom2lem  36209  alrmomorn  36417  dfeldisj5  36759  isltrn2N  38061  moxfr  40430  ifporcor  40967  ifpancor  40969  ifpbicor  40980  ifpnorcor  40985  ifpnancor  40986  ifpororb  41010  relexp0eq  41198  hashnzfzclim  41829  pm11.6  41899  sbc3or  42041  cbvexsv  42056  dfich2  44798  ichbi12i  44800  sprvalpwn0  44823  copisnmnd  45251