Theorem bitr2i 277

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

Syntax hints:   ↔ wb 207

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 208

This theorem is referenced by:  3bitrri  299  3bitr2ri  301  3bitr4ri  305  nan  835  pm4.15  838  pm5.7  961  pm5.17  1019  pm4.83  1032  3or6  1455  nanim  1505  nannot  1506  empty  1913  19.12vvv  2001  19.12vv  2355  cvjust  2734  necon1abii  2983  nrexralim  3124  r19.23v  3167  nelb  3216  cbvralsvw  3291  spc3gv  3549  ralxpxfr2d  3591  sbc8g  3738  csbied  3874  dfss2  3908  ss2rab  4007  difdif  4072  ddif  4078  unass  4108  unss  4126  undi  4220  disj  4385  ssindif0  4399  prneimg  4792  iinrab2  5006  unopab  5159  axrep5  5214  eqvinop  5434  pwssun  5517  dmun  5859  reldm0  5877  dmres  5971  imadmrn  6029  ssrnres  6136  dmsnn0  6165  coundi  6205  coundir  6206  resco  6208  cnvpo  6245  xpco  6247  dfpo2  6254  fun11  6566  fununi  6567  fdmrn  6693  dffv2  6929  fsn  7084  eufnfv  7180  eloprabga  7472  funoprabg  7484  ralrnmpo  7502  imaeqexov  7601  tfinds2  7811  funcnvuni  7879  oprabrexex2  7927  ralxp3f  8084  soseq  8106  dfer2  8641  euen1b  8972  xpsnen  8996  wemapsolem  9462  zfregcl  9506  zfregclOLD  9507  epfrs  9650  rankbnd  9790  rankbnd2  9791  rankxplim2  9802  rankxplim3  9803  isinfcard  10012  dfac5lem2  10044  dfac5lem5  10047  kmlem14  10084  kmlem15  10085  kmlem16  10086  axdc2lem  10368  axcclem  10377  ac9  10403  ac9s  10413  nnunb  12431  xrrebnd  13118  elfznelfzo  13726  hashfun  14397  hashtpg  14445  rexuz3  15309  imasaddfnlem  17490  isnsgrp  18689  eqg0subg  19169  dprd2d2  20019  isnirred  20398  subsubrng2  20543  subsubrg2  20578  isdomn2OLD  20691  mdetunilem8  22609  maducoeval2  22630  tgval2  22946  0top  22973  ssntr  23048  uncmp  23393  opnfbas  23832  fbunfip  23859  alexsubALTlem2  24038  alexsubALTlem3  24039  alexsubALT  24041  metrest  24514  cfilucfil3  25312  ellimc3  25871  plyun0  26187  sinhalfpilem  26452  2lgslem4  27394  addsdilem1  28168  addsdilem2  28169  mulsasslem1  28180  mulsasslem2  28181  dfcgra2  28923  colinearalg  29004  axcontlem5  29062  nb3grprlem2  29475  wlkeq  29727  isspthonpth  29842  clwlkclwwlklem2a4  30092  clwwlkn1  30136  clwwlkn2  30139  clwwlknon2x  30198  fusgreg2wsp  30431  h2hlm  31076  shlesb1i  31482  pjneli  31819  cnlnssadj  32176  pjin2i  32289  cvnbtwn2  32383  cvnbtwn4  32385  mdsl1i  32417  mdsl2i  32418  hatomistici  32458  cdj3lem3b  32536  iuninc  32656  disjex  32688  disjexc  32689  fpwrelmapffslem  32831  fpwrelmapffs  32833  mgcval  33073  isarchi2  33273  elrgspnlem2  33331  ismntop  34217  coinfliprv  34674  ballotlem2  34680  ballotlemi1  34694  plymulx  34739  oddprm2  34846  bnj168  34920  bnj153  35069  bnj605  35096  bnj607  35105  bnj986  35144  bnj1090  35168  bnj1128  35179  fineqvrep  35305  axregszf  35320  axregs  35330  fmlasucdisj  35628  dfso2  35984  19.12b  36028  dfom5b  36139  elfuns  36142  dfint3  36181  hfext  36412  trer  36545  bj-alcomexcom  37022  wl-3xornot1  37843  wl-df3maxtru1  37855  cnambfre  38036  itg2addnclem2  38040  itg2addnc  38042  heiborlem1  38179  inxpxrn  38786  eldisjdmqsim  39185  lssat  39509  islshpat  39510  lcvnbtwn2  39520  pclfinclN  40443  lhpex2leN  40506  diclspsn  41687  dihmeetlem4preN  41799  dihmeetlem13N  41812  lcdlss  42112  mapd1o  42141  eq0rabdioph  43226  rmspecnonsq  43353  rmxdioph  43462  wopprc  43476  islssfg2  43517  ifpan23  43905  ifpid1g  43939  minregex  43979  dfrtrcl5  44074  dfhe3  44220  ntrneikb  44539  scottabf  44685  2sbc6g  44860  2sbc5g  44861  iotasbc2  44865  2sb5nd  45005  2sb5ndVD  45354  2sb5ndALT  45376  ssclaxsep  45427  permac8prim  45459  limsupre2lem  46168  2rexsb  47565  2rexrsb  47566  usgrexmpl2nb2  48525  usgrexmpl2nb5  48528  usgrexmpl2trifr  48529  islindeps  48945  io1ii  49412