Theorem 3bitr3i 289

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

Syntax hints:   ↔ wb 195

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 196

This theorem is referenced by:  an12  834  xorass  1460  cbval2  2267  cbvaldva  2269  sbco2d  2404  sbcom  2406  equsb3  2420  equsb3ALT  2421  elsb3  2422  elsb4  2423  sb7f  2441  sbco4lem  2453  eq2tri  2671  eqsb3  2715  clelsb3  2716  r19.35  3065  ralcom4  3197  rexcom4  3198  ceqsralt  3202  gencbvex  3223  gencbval  3225  ceqsrexbv  3307  euind  3360  reuind  3378  sbccomlem  3475  sbccom  3476  csbcom  3946  difcom  4005  eqsn  4299  uniintsn  4444  disjxun  4576  reusv2lem4  4793  exss  4852  elxp2OLD  5047  eqbrriv  5127  dm0rn0  5250  dfres2  5359  qfto  5423  rninxp  5478  coeq0  5547  fununi  5864  dffv2  6166  fndmin  6217  fnprb  6355  fntpb  6356  dfoprab2  6577  dfer2  7608  eceqoveq  7718  euen1  7890  xpsnen  7907  xpassen  7917  marypha2lem3  8204  rankuni  8587  card1  8655  alephislim  8767  dfacacn  8824  kmlem4  8836  ac6num  9162  zorn2lem4  9182  fpwwe2lem8  9316  fpwwe2lem12  9320  mappsrpr  9786  sqeqori  12796  trclublem  13531  fprodle  14515  vdwmc2  15470  txflf  21568  metustid  22117  caucfil  22834  ovolgelb  23000  dfcgra2  25467  axcontlem5  25594  nmoubi  26805  hvsubaddi  27101  hlimeui  27275  omlsilem  27439  pjoml3i  27623  hodsi  27812  nmopub  27945  nmfnleub  27962  nmopcoadj0i  28140  pjin3i  28231  or3dir  28486  ralcom4f  28494  rexcom4f  28495  clelsb3f  28498  uniinn0  28543  ordtconlem1  29092  bnj62  29834  bnj610  29865  bnj1143  29909  bnj1533  29970  bnj543  30011  bnj545  30013  bnj594  30030  ceqsralv2  30656  br1steq  30711  br2ndeq  30712  brsuccf  31012  brfullfun  31019  filnetlem4  31340  bj-ssbcom3lem  31633  bj-cbval2v  31718  bj-clelsb3  31836  icorempt2  32169  poimirlem13  32386  poimirlem14  32387  poimirlem21  32394  poimirlem22  32395  poimir  32406  sbccom2lem  32893  isltrn2N  34218  moxfr  36067  ifporcor  36619  ifpancor  36621  ifpbicor  36633  ifpnorcor  36638  ifpnancor  36639  ifpororb  36663  relexp0eq  36806  hashnzfzclim  37337  pm11.6  37408  sbc3or  37553  cbvexsv  37577  frgr3v  41437  copisnmnd  41591