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  956  pm5.17  1014  pm4.83  1027  3or6  1450  nanim  1500  nannot  1501  empty  1908  19.12vvv  1996  19.12vv  2352  cvjust  2731  necon1abii  2981  nrexralim  3122  r19.23v  3165  nelb  3214  cbvralsvw  3289  spc3gv  3560  ralxpxfr2d  3602  sbc8g  3750  csbied  3887  dfss2  3921  ss2rab  4023  difdif  4089  ddif  4095  unass  4126  unss  4144  undi  4239  disj  4404  ssindif0  4418  prneimg  4812  iinrab2  5027  unopab  5180  axrep5  5234  eqvinop  5443  pwssun  5524  dmun  5867  reldm0  5885  dmres  5979  imadmrn  6037  ssrnres  6144  dmsnn0  6173  coundi  6213  coundir  6214  resco  6216  cnvpo  6253  xpco  6255  dfpo2  6262  fun11  6574  fununi  6575  fdmrn  6701  dffv2  6937  fsn  7090  eufnfv  7185  eloprabga  7477  funoprabg  7489  ralrnmpo  7507  imaeqexov  7606  tfinds2  7816  funcnvuni  7884  oprabrexex2  7932  ralxp3f  8089  soseq  8111  dfer2  8646  euen1b  8977  xpsnen  9001  wemapsolem  9467  zfregcl  9511  zfregclOLD  9512  epfrs  9652  rankbnd  9792  rankbnd2  9793  rankxplim2  9804  rankxplim3  9805  isinfcard  10014  dfac5lem2  10046  dfac5lem5  10049  kmlem14  10086  kmlem15  10087  kmlem16  10088  axdc2lem  10370  axcclem  10379  ac9  10405  ac9s  10415  nnunb  12409  xrrebnd  13095  elfznelfzo  13701  hashfun  14372  hashtpg  14420  rexuz3  15284  imasaddfnlem  17461  isnsgrp  18660  eqg0subg  19137  dprd2d2  19987  isnirred  20368  subsubrng2  20509  subsubrg2  20544  isdomn2OLD  20657  mdetunilem8  22575  maducoeval2  22596  tgval2  22912  0top  22939  ssntr  23014  uncmp  23359  opnfbas  23798  fbunfip  23825  alexsubALTlem2  24004  alexsubALTlem3  24005  alexsubALT  24007  metrest  24480  cfilucfil3  25288  ellimc3  25848  plyun0  26170  sinhalfpilem  26440  2lgslem4  27385  addsdilem1  28159  addsdilem2  28160  mulsasslem1  28171  mulsasslem2  28172  dfcgra2  28914  colinearalg  28995  axcontlem5  29053  nb3grprlem2  29466  wlkeq  29719  isspthonpth  29834  clwlkclwwlklem2a4  30084  clwwlkn1  30128  clwwlkn2  30131  clwwlknon2x  30190  fusgreg2wsp  30423  h2hlm  31067  shlesb1i  31473  pjneli  31810  cnlnssadj  32167  pjin2i  32280  cvnbtwn2  32374  cvnbtwn4  32376  mdsl1i  32408  mdsl2i  32409  hatomistici  32449  cdj3lem3b  32527  iuninc  32646  disjex  32678  disjexc  32679  fpwrelmapffslem  32821  fpwrelmapffs  32823  mgcval  33079  isarchi2  33278  elrgspnlem2  33336  ismntop  34203  coinfliprv  34660  ballotlem2  34666  ballotlemi1  34680  plymulx  34725  oddprm2  34832  bnj168  34906  bnj153  35055  bnj605  35082  bnj607  35091  bnj986  35130  bnj1090  35154  bnj1128  35165  fineqvrep  35289  axregszf  35304  axregs  35314  fmlasucdisj  35612  dfso2  35968  19.12b  36012  dfom5b  36123  elfuns  36126  dfint3  36165  hfext  36396  trer  36529  bj-alcomexcom  36918  wl-3xornot1  37724  wl-df3maxtru1  37736  cnambfre  37908  itg2addnclem2  37912  itg2addnc  37914  heiborlem1  38051  inxpxrn  38658  eldisjdmqsim  39057  lssat  39381  islshpat  39382  lcvnbtwn2  39392  pclfinclN  40315  lhpex2leN  40378  diclspsn  41559  dihmeetlem4preN  41671  dihmeetlem13N  41684  lcdlss  41984  mapd1o  42013  eq0rabdioph  43122  rmspecnonsq  43253  rmxdioph  43362  wopprc  43376  islssfg2  43417  ifpan23  43805  ifpid1g  43839  minregex  43879  dfrtrcl5  43974  dfhe3  44120  ntrneikb  44439  scottabf  44585  2sbc6g  44760  2sbc5g  44761  iotasbc2  44765  2sb5nd  44905  2sb5ndVD  45254  2sb5ndALT  45276  ssclaxsep  45327  permac8prim  45359  limsupre2lem  46071  2rexsb  47450  2rexrsb  47451  usgrexmpl2nb2  48382  usgrexmpl2nb5  48385  usgrexmpl2trifr  48386  islindeps  48802  io1ii  49269