Theorem bitr2i 276

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 275	. 2 ⊢ (𝜑 ↔ 𝜒)
4	3	bicomi 224	1 ⊢ (𝜒 ↔ 𝜑)

Syntax hints:   ↔ wb 206

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 207

This theorem is referenced by:  3bitrri  298  3bitr2ri  300  3bitr4ri  304  nan  830  pm4.15  833  pm5.7  955  pm5.17  1013  pm4.83  1026  3or6  1446  nanim  1495  nannot  1496  empty  1904  19.12vvv  1986  19.12vv  2348  cvjust  2729  necon1abii  2987  nrexralim  3135  r19.23v  3181  nelb  3232  cbvralsvw  3315  spc3gv  3604  ralxpxfr2d  3646  sbc8g  3799  csbied  3946  dfss2  3981  ss2rab  4081  difdif  4145  ddif  4151  unass  4182  unss  4200  undi  4291  vn0  4351  ab0orv  4389  disj  4456  ssindif0  4470  prneimg  4859  iinrab2  5075  unopab  5230  axrep5  5293  eqvinop  5498  pwssun  5580  dmun  5924  reldm0  5941  dmres  6032  imadmrn  6090  ssrnres  6200  dmsnn0  6229  coundi  6269  coundir  6270  resco  6272  cnvpo  6309  xpco  6311  dfpo2  6318  fun11  6642  fununi  6643  isarep1OLD  6658  fdmrn  6768  dffv2  7004  fsn  7155  eufnfv  7249  eloprabga  7541  eloprabgaOLD  7542  funoprabg  7554  ralrnmpo  7572  imaeqexov  7671  sucexeloniOLD  7830  suceloniOLD  7832  tfinds2  7885  funcnvuni  7955  oprabrexex2  8002  ralxp3f  8161  soseq  8183  dfer2  8745  euen1b  9067  xpsnen  9094  1sdomOLD  9283  wemapsolem  9588  zfregcl  9632  epfrs  9769  rankbnd  9906  rankbnd2  9907  rankxplim2  9918  rankxplim3  9919  isinfcard  10130  dfac5lem2  10162  dfac5lem5  10165  kmlem14  10202  kmlem15  10203  kmlem16  10204  axdc2lem  10486  axcclem  10495  ac9  10521  ac9s  10531  nnunb  12520  xrrebnd  13207  elfznelfzo  13808  hashfun  14473  hashtpg  14521  rexuz3  15384  imasaddfnlem  17575  isnsgrp  18749  eqg0subg  19227  dprd2d2  20079  isnirred  20437  subsubrng2  20581  subsubrg2  20616  isdomn2OLD  20729  mdetunilem8  22641  maducoeval2  22662  tgval2  22979  0top  23006  ssntr  23082  uncmp  23427  opnfbas  23866  fbunfip  23893  alexsubALTlem2  24072  alexsubALTlem3  24073  alexsubALT  24075  metrest  24553  cfilucfil3  25368  ellimc3  25929  plyun0  26251  sinhalfpilem  26520  2lgslem4  27465  addsdilem1  28192  addsdilem2  28193  mulsasslem1  28204  mulsasslem2  28205  dfcgra2  28853  colinearalg  28940  axcontlem5  28998  nb3grprlem2  29413  wlkeq  29667  isspthonpth  29782  clwlkclwwlklem2a4  30026  clwwlkn1  30070  clwwlkn2  30073  clwwlknon2x  30132  fusgreg2wsp  30365  h2hlm  31009  shlesb1i  31415  pjneli  31752  cnlnssadj  32109  pjin2i  32222  cvnbtwn2  32316  cvnbtwn4  32318  mdsl1i  32350  mdsl2i  32351  hatomistici  32391  cdj3lem3b  32469  iuninc  32581  disjex  32612  disjexc  32613  fpwrelmapffslem  32750  fpwrelmapffs  32752  mgcval  32962  isarchi2  33175  elrgspnlem2  33233  ismntop  33989  coinfliprv  34464  ballotlem2  34470  ballotlemi1  34484  plymulx  34542  oddprm2  34649  bnj168  34723  bnj153  34873  bnj605  34900  bnj607  34909  bnj986  34948  bnj1090  34972  bnj1128  34983  fineqvrep  35088  fmlasucdisj  35384  dfso2  35735  19.12b  35783  dfom5b  35894  elfuns  35897  dfint3  35934  hfext  36165  trer  36299  bj-alcomexcom  36663  wl-3xornot1  37463  wl-df3maxtru1  37475  cnambfre  37655  itg2addnclem2  37659  itg2addnc  37661  heiborlem1  37798  inxpxrn  38377  lssat  38998  islshpat  38999  lcvnbtwn2  39009  pclfinclN  39933  lhpex2leN  39996  diclspsn  41177  dihmeetlem4preN  41289  dihmeetlem13N  41302  lcdlss  41602  mapd1o  41631  eq0rabdioph  42764  rmspecnonsq  42895  rmxdioph  43005  wopprc  43019  islssfg2  43060  ifpan23  43450  ifpid1g  43484  minregex  43524  dfrtrcl5  43619  dfhe3  43765  ntrneikb  44084  scottabf  44236  2sbc6g  44411  2sbc5g  44412  iotasbc2  44416  2sb5nd  44558  2sb5ndVD  44908  2sb5ndALT  44930  ssclaxsep  44947  limsupre2lem  45680  2rexsb  47051  2rexrsb  47052  usgrexmpl2nb2  47928  usgrexmpl2nb5  47931  usgrexmpl2trifr  47932  islindeps  48299  io1ii  48717