Theorem bitr2i 278

Description: An inference from transitive law for logical equivalence. (Contributed by NM, 12-Mar-1993.)

Hypotheses

Ref	Expression
bitr2i.1	⊢ (𝜑 ↔ 𝜓)
bitr2i.2	⊢ (𝜓 ↔ 𝜒)

Assertion

Ref	Expression
bitr2i	⊢ (𝜒 ↔ 𝜑)

Proof of Theorem bitr2i

Step	Hyp	Ref	Expression
1		bitr2i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2		bitr2i.2	. . 3 ⊢ (𝜓 ↔ 𝜒)
3	1, 2	bitri 277	. 2 ⊢ (𝜑 ↔ 𝜒)
4	3	bicomi 226	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:  3bitrri  300  3bitr2ri  302  3bitr4ri  306  nan  827  pm4.15  830  pm5.7  950  pm5.17  1008  pm4.83  1021  3or6  1443  nanim  1488  nannot  1489  empty  1907  19.12vvv  1995  19.12vv  2368  cvjust  2818  abbi  2890  abbiOLD  2957  necon1abii  3066  nabbi  3123  ralnex2OLD  3263  ralnex3OLD  3265  nrexralim  3268  r19.23v  3281  spc3gv  3607  ralxpxfr2d  3641  sbc8g  3782  ss2rab  4049  difdif  4109  ddif  4115  unass  4144  unss  4162  undi  4253  disj  4401  ssindif0  4415  prneimg  4787  pwsnOLD  4833  iinrab2  4994  unopab  5147  axrep5  5198  eqvinop  5380  pwssun  5458  dmun  5781  reldm0  5800  dmres  5877  imadmrn  5941  ssrnres  6037  dmsnn0  6066  coundi  6102  coundir  6103  resco  6105  cnvpo  6140  xpco  6142  fun11  6430  fununi  6431  isarep1  6444  fdmrn  6540  dffv2  6758  fsn  6899  eufnfv  6993  eloprabga  7263  funoprabg  7275  ralrnmpo  7291  suceloni  7530  tfinds2  7580  funcnvuni  7638  oprabrexex2  7681  fsplitOLD  7815  dfer2  8292  euen1b  8582  xpsnen  8603  1sdom  8723  wemapsolem  9016  zfregcl  9060  epfrs  9175  rankbnd  9299  rankbnd2  9300  rankxplim2  9311  rankxplim3  9312  isinfcard  9520  dfac5lem2  9552  dfac5lem5  9555  kmlem14  9591  kmlem15  9592  kmlem16  9593  axdc2lem  9872  axcclem  9881  ac9  9907  ac9s  9917  nnunb  11896  xrrebnd  12564  elfznelfzo  13145  hashfun  13801  hashtpg  13846  rexuz3  14710  imasaddfnlem  16803  isnsgrp  17907  dprd2d2  19168  isnirred  19452  subsubrg2  19564  isdomn2  20074  mdetunilem8  21230  maducoeval2  21251  tgval2  21566  0top  21593  ssntr  21668  uncmp  22013  opnfbas  22452  fbunfip  22479  alexsubALTlem2  22658  alexsubALTlem3  22659  alexsubALT  22661  metrest  23136  cfilucfil3  23925  ellimc3  24479  plyun0  24789  sinhalfpilem  25051  2lgslem4  25984  dfcgra2  26618  colinearalg  26698  axcontlem5  26756  nb3grprlem2  27165  wlkeq  27417  isspthonpth  27532  clwlkclwwlklem2a4  27777  clwwlkn1  27821  clwwlkn2  27824  clwwlknon2x  27884  fusgreg2wsp  28117  h2hlm  28759  shlesb1i  29165  pjneli  29502  cnlnssadj  29859  pjin2i  29972  cvnbtwn2  30066  cvnbtwn4  30068  mdsl1i  30100  mdsl2i  30101  hatomistici  30141  cdj3lem3b  30219  nelbOLD  30234  iuninc  30314  disjex  30344  disjexc  30345  fpwrelmapffslem  30470  fpwrelmapffs  30472  isarchi2  30816  ismntop  31269  coinfliprv  31742  ballotlem2  31748  ballotlemi1  31762  plymulx  31820  oddprm2  31928  bnj168  32002  bnj153  32154  bnj605  32181  bnj607  32190  bnj986  32229  bnj1090  32253  bnj1128  32264  fmlasucdisj  32648  dfso2  32992  dfpo2  32993  19.12b  33048  soseq  33098  dfom5b  33375  elfuns  33378  dfint3  33415  hfext  33646  trer  33666  cnambfre  34942  itg2addnclem2  34946  itg2addnc  34948  heiborlem1  35091  inxpxrn  35645  lssat  36154  islshpat  36155  lcvnbtwn2  36165  pclfinclN  37088  lhpex2leN  37151  diclspsn  38332  dihmeetlem4preN  38444  dihmeetlem13N  38457  lcdlss  38757  mapd1o  38786  eq0rabdioph  39380  rmspecnonsq  39511  rmxdioph  39620  wopprc  39634  islssfg2  39678  ifpan23  39832  ifpid1g  39867  dfrtrcl5  39996  dfhe3  40128  ntrneikb  40451  scottabf  40583  2sbc6g  40754  2sbc5g  40755  iotasbc2  40759  2sb5nd  40901  2sb5ndVD  41251  2sb5ndALT  41273  limsupre2lem  42012  2rexsb  43306  2rexrsb  43307  islindeps  44515