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  829  pm4.15  832  pm5.7  955  pm5.17  1013  pm4.83  1026  3or6  1449  nanim  1499  nannot  1500  empty  1907  19.12vvv  1995  19.12vv  2346  cvjust  2724  necon1abii  2974  nrexralim  3114  r19.23v  3157  nelb  3206  cbvralsvw  3281  spc3gv  3557  ralxpxfr2d  3599  sbc8g  3747  csbied  3884  dfss2  3918  ss2rab  4019  difdif  4083  ddif  4089  unass  4120  unss  4138  undi  4233  vn0  4293  ab0orv  4331  disj  4398  ssindif0  4412  prneimg  4804  iinrab2  5016  unopab  5169  axrep5  5223  eqvinop  5425  pwssun  5506  dmun  5848  reldm0  5865  dmres  5958  imadmrn  6016  ssrnres  6122  dmsnn0  6151  coundi  6191  coundir  6192  resco  6194  cnvpo  6230  xpco  6232  dfpo2  6239  fun11  6551  fununi  6552  fdmrn  6678  dffv2  6912  fsn  7063  eufnfv  7158  eloprabga  7450  funoprabg  7462  ralrnmpo  7480  imaeqexov  7579  tfinds2  7789  funcnvuni  7857  oprabrexex2  7905  ralxp3f  8062  soseq  8084  dfer2  8618  euen1b  8945  xpsnen  8969  wemapsolem  9431  zfregcl  9475  zfregclOLD  9476  epfrs  9616  rankbnd  9753  rankbnd2  9754  rankxplim2  9765  rankxplim3  9766  isinfcard  9975  dfac5lem2  10007  dfac5lem5  10010  kmlem14  10047  kmlem15  10048  kmlem16  10049  axdc2lem  10331  axcclem  10340  ac9  10366  ac9s  10376  nnunb  12369  xrrebnd  13059  elfznelfzo  13665  hashfun  14336  hashtpg  14384  rexuz3  15248  imasaddfnlem  17424  isnsgrp  18623  eqg0subg  19101  dprd2d2  19951  isnirred  20331  subsubrng2  20472  subsubrg2  20507  isdomn2OLD  20620  mdetunilem8  22527  maducoeval2  22548  tgval2  22864  0top  22891  ssntr  22966  uncmp  23311  opnfbas  23750  fbunfip  23777  alexsubALTlem2  23956  alexsubALTlem3  23957  alexsubALT  23959  metrest  24432  cfilucfil3  25240  ellimc3  25800  plyun0  26122  sinhalfpilem  26392  2lgslem4  27337  addsdilem1  28083  addsdilem2  28084  mulsasslem1  28095  mulsasslem2  28096  dfcgra2  28801  colinearalg  28881  axcontlem5  28939  nb3grprlem2  29352  wlkeq  29605  isspthonpth  29720  clwlkclwwlklem2a4  29967  clwwlkn1  30011  clwwlkn2  30014  clwwlknon2x  30073  fusgreg2wsp  30306  h2hlm  30950  shlesb1i  31356  pjneli  31693  cnlnssadj  32050  pjin2i  32163  cvnbtwn2  32257  cvnbtwn4  32259  mdsl1i  32291  mdsl2i  32292  hatomistici  32332  cdj3lem3b  32410  iuninc  32530  disjex  32562  disjexc  32563  fpwrelmapffslem  32705  fpwrelmapffs  32707  mgcval  32958  isarchi2  33144  elrgspnlem2  33200  ismntop  34029  coinfliprv  34486  ballotlem2  34492  ballotlemi1  34506  plymulx  34551  oddprm2  34658  bnj168  34732  bnj153  34882  bnj605  34909  bnj607  34918  bnj986  34957  bnj1090  34981  bnj1128  34992  axregszf  35099  fineqvrep  35105  axregs  35113  fmlasucdisj  35411  dfso2  35767  19.12b  35814  dfom5b  35925  elfuns  35928  dfint3  35965  hfext  36196  trer  36329  bj-alcomexcom  36693  wl-3xornot1  37493  wl-df3maxtru1  37505  cnambfre  37687  itg2addnclem2  37691  itg2addnc  37693  heiborlem1  37830  inxpxrn  38406  lssat  39034  islshpat  39035  lcvnbtwn2  39045  pclfinclN  39968  lhpex2leN  40031  diclspsn  41212  dihmeetlem4preN  41324  dihmeetlem13N  41337  lcdlss  41637  mapd1o  41666  eq0rabdioph  42788  rmspecnonsq  42919  rmxdioph  43028  wopprc  43042  islssfg2  43083  ifpan23  43472  ifpid1g  43506  minregex  43546  dfrtrcl5  43641  dfhe3  43787  ntrneikb  44106  scottabf  44252  2sbc6g  44427  2sbc5g  44428  iotasbc2  44432  2sb5nd  44572  2sb5ndVD  44921  2sb5ndALT  44943  ssclaxsep  44994  permac8prim  45026  limsupre2lem  45741  2rexsb  47111  2rexrsb  47112  usgrexmpl2nb2  48043  usgrexmpl2nb5  48046  usgrexmpl2trifr  48047  islindeps  48464  io1ii  48931