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  1498  nannot  1499  empty  1906  19.12vvv  1994  19.12vv  2345  cvjust  2723  necon1abii  2973  nrexralim  3113  r19.23v  3156  nelb  3205  cbvralsvw  3281  spc3gv  3561  ralxpxfr2d  3603  sbc8g  3752  csbied  3889  dfss2  3923  ss2rab  4024  difdif  4088  ddif  4094  unass  4125  unss  4143  undi  4238  vn0  4298  ab0orv  4336  disj  4403  ssindif0  4417  prneimg  4808  iinrab2  5022  unopab  5175  axrep5  5229  eqvinop  5434  pwssun  5515  dmun  5857  reldm0  5874  dmres  5967  imadmrn  6025  ssrnres  6131  dmsnn0  6160  coundi  6200  coundir  6201  resco  6203  cnvpo  6239  xpco  6241  dfpo2  6248  fun11  6560  fununi  6561  fdmrn  6687  dffv2  6922  fsn  7073  eufnfv  7169  eloprabga  7462  funoprabg  7474  ralrnmpo  7492  imaeqexov  7591  sucexeloniOLD  7750  tfinds2  7804  funcnvuni  7872  oprabrexex2  7920  ralxp3f  8077  soseq  8099  dfer2  8633  euen1b  8960  xpsnen  8985  wemapsolem  9461  zfregcl  9505  zfregclOLD  9506  epfrs  9646  rankbnd  9783  rankbnd2  9784  rankxplim2  9795  rankxplim3  9796  isinfcard  10005  dfac5lem2  10037  dfac5lem5  10040  kmlem14  10077  kmlem15  10078  kmlem16  10079  axdc2lem  10361  axcclem  10370  ac9  10396  ac9s  10406  nnunb  12398  xrrebnd  13088  elfznelfzo  13693  hashfun  14362  hashtpg  14410  rexuz3  15274  imasaddfnlem  17450  isnsgrp  18615  eqg0subg  19093  dprd2d2  19943  isnirred  20323  subsubrng2  20467  subsubrg2  20502  isdomn2OLD  20615  mdetunilem8  22522  maducoeval2  22543  tgval2  22859  0top  22886  ssntr  22961  uncmp  23306  opnfbas  23745  fbunfip  23772  alexsubALTlem2  23951  alexsubALTlem3  23952  alexsubALT  23954  metrest  24428  cfilucfil3  25236  ellimc3  25796  plyun0  26118  sinhalfpilem  26388  2lgslem4  27333  addsdilem1  28077  addsdilem2  28078  mulsasslem1  28089  mulsasslem2  28090  dfcgra2  28793  colinearalg  28873  axcontlem5  28931  nb3grprlem2  29344  wlkeq  29597  isspthonpth  29712  clwlkclwwlklem2a4  29959  clwwlkn1  30003  clwwlkn2  30006  clwwlknon2x  30065  fusgreg2wsp  30298  h2hlm  30942  shlesb1i  31348  pjneli  31685  cnlnssadj  32042  pjin2i  32155  cvnbtwn2  32249  cvnbtwn4  32251  mdsl1i  32283  mdsl2i  32284  hatomistici  32324  cdj3lem3b  32402  iuninc  32522  disjex  32554  disjexc  32555  fpwrelmapffslem  32688  fpwrelmapffs  32690  mgcval  32942  isarchi2  33137  elrgspnlem2  33193  ismntop  33992  coinfliprv  34450  ballotlem2  34456  ballotlemi1  34470  plymulx  34515  oddprm2  34622  bnj168  34696  bnj153  34846  bnj605  34873  bnj607  34882  bnj986  34921  bnj1090  34945  bnj1128  34956  axregszf  35063  fineqvrep  35069  axregs  35073  fmlasucdisj  35371  dfso2  35727  19.12b  35774  dfom5b  35885  elfuns  35888  dfint3  35925  hfext  36156  trer  36289  bj-alcomexcom  36653  wl-3xornot1  37453  wl-df3maxtru1  37465  cnambfre  37647  itg2addnclem2  37651  itg2addnc  37653  heiborlem1  37790  inxpxrn  38366  lssat  38994  islshpat  38995  lcvnbtwn2  39005  pclfinclN  39929  lhpex2leN  39992  diclspsn  41173  dihmeetlem4preN  41285  dihmeetlem13N  41298  lcdlss  41598  mapd1o  41627  eq0rabdioph  42749  rmspecnonsq  42880  rmxdioph  42989  wopprc  43003  islssfg2  43044  ifpan23  43433  ifpid1g  43467  minregex  43507  dfrtrcl5  43602  dfhe3  43748  ntrneikb  44067  scottabf  44213  2sbc6g  44388  2sbc5g  44389  iotasbc2  44393  2sb5nd  44534  2sb5ndVD  44883  2sb5ndALT  44905  ssclaxsep  44956  permac8prim  44988  limsupre2lem  45706  2rexsb  47086  2rexrsb  47087  usgrexmpl2nb2  48008  usgrexmpl2nb5  48011  usgrexmpl2trifr  48012  islindeps  48426  io1ii  48893