Theorem bitr2i 278

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

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  3bitrri  300  3bitr2ri  302  3bitr4ri  306  nan  838  pm4.15  841  pm5.7  964  pm5.17  1022  pm4.83  1035  3or6  1462  nanim  1512  nannot  1513  empty  1920  19.12vvv  2008  19.12vv  2372  cvjust  2750  necon1abii  2999  nrexralim  3140  r19.23v  3183  nelb  3232  cbvralsvw  3307  spc3gv  3558  ralxpxfr2d  3600  sbc8g  3747  csbied  3883  dfss2  3917  ss2rab  4017  difdif  4083  ddif  4089  unass  4119  unss  4137  undi  4232  disj  4398  ssindif0  4412  prneimg  4806  iinrab2  5021  unopab  5174  axrep5  5229  eqvinop  5449  pwssun  5532  dmun  5879  reldm0  5897  dmres  5991  imadmrn  6049  ssrnres  6153  dmsnn0  6183  coundi  6223  coundir  6224  resco  6226  cnvpo  6263  xpco  6265  dfpo2  6272  fun11  6584  fununi  6585  fdmrn  6712  dffv2  6951  fsn  7106  eufnfv  7202  eloprabga  7494  funoprabg  7506  ralrnmpo  7524  imaeqexov  7623  tfinds2  7833  funcnvuni  7902  oprabrexex2  7948  ralxp3f  8105  soseq  8127  dfer2  8667  euen1b  8998  xpsnen  9022  wemapsolem  9488  zfregcl  9532  zfregclOLD  9533  epfrs  9676  rankbnd  9816  rankbnd2  9817  rankxplim2  9828  rankxplim3  9829  isinfcard  10038  dfac5lem2  10070  dfac5lem5  10073  kmlem14  10110  kmlem15  10111  kmlem16  10112  axdc2lem  10395  axcclem  10404  ac9  10430  ac9s  10440  nnunb  12467  xrrebnd  13161  elfznelfzo  13769  hashfun  14440  hashtpg  14488  rexuz3  15352  imasaddfnlem  17534  isnsgrp  18733  eqg0subg  19213  dprd2d2  20062  isnirred  20441  subsubrng2  20586  subsubrg2  20621  isdomn2OLD  20734  mdetunilem8  22652  maducoeval2  22673  tgval2  22989  0top  23016  ssntr  23091  uncmp  23436  opnfbas  23875  fbunfip  23902  alexsubALTlem2  24081  alexsubALTlem3  24082  alexsubALT  24084  metrest  24557  cfilucfil3  25355  ellimc3  25914  plyun0  26230  sinhalfpilem  26498  2lgslem4  27440  addsdilem1  28214  addsdilem2  28215  mulsasslem1  28226  mulsasslem2  28227  dfcgra2  28969  colinearalg  29050  axcontlem5  29108  nb3grprlem2  29521  wlkeq  29773  isspthonpth  29888  clwlkclwwlklem2a4  30138  clwwlkn1  30182  clwwlkn2  30185  clwwlknon2x  30244  fusgreg2wsp  30477  h2hlm  31122  shlesb1i  31528  pjneli  31865  cnlnssadj  32222  pjin2i  32335  cvnbtwn2  32429  cvnbtwn4  32431  mdsl1i  32463  mdsl2i  32464  hatomistici  32504  cdj3lem3b  32582  iuninc  32702  disjex  32734  disjexc  32735  fpwrelmapffslem  32877  fpwrelmapffs  32879  mgcval  33119  isarchi2  33319  elrgspnlem2  33378  ismntop  34277  coinfliprv  34734  ballotlem2  34740  ballotlemi1  34754  plymulx  34799  oddprm2  34906  bnj168  34983  bnj153  35132  bnj605  35159  bnj607  35168  bnj986  35207  bnj1090  35231  bnj1128  35242  fineqvrep  35365  axregszf  35380  axregs  35390  fmlasucdisj  35697  dfso2  36053  19.12b  36097  dfom5b  36208  elfuns  36211  dfint3  36250  hfext  36481  nmulprop  36488  trer  36624  bj-alcomexcom  37101  wl-3xornot1  37922  wl-df3maxtru1  37934  cnambfre  38115  itg2addnclem2  38119  itg2addnc  38121  heiborlem1  38258  inxpxrn  38865  eldisjdmqsim  39264  lssat  39588  islshpat  39589  lcvnbtwn2  39599  pclfinclN  40522  lhpex2leN  40585  diclspsn  41766  dihmeetlem4preN  41878  dihmeetlem13N  41891  lcdlss  42191  mapd1o  42220  eq0rabdioph  43305  rmspecnonsq  43432  rmxdioph  43541  wopprc  43555  islssfg2  43596  ifpan23  43984  ifpid1g  44018  minregex  44058  dfrtrcl5  44153  dfhe3  44299  ntrneikb  44618  scottabf  44764  2sbc6g  44939  2sbc5g  44940  iotasbc2  44944  2sb5nd  45084  2sb5ndVD  45433  2sb5ndALT  45455  ssclaxsep  45506  permac8prim  45538  limsupre2lem  46246  2rexsb  47643  2rexrsb  47644  usgrexmpl2nb2  48603  usgrexmpl2nb5  48606  usgrexmpl2trifr  48607  islindeps  49023  io1ii  49490