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  954  pm5.17  1012  pm4.83  1025  3or6  1447  nanim  1495  nannot  1496  empty  1905  19.12vvv  1988  19.12vv  2353  cvjust  2734  necon1abii  2995  nrexralim  3143  r19.23v  3189  nelb  3240  cbvralsvw  3323  spc3gv  3617  ralxpxfr2d  3659  sbc8g  3812  csbied  3959  dfss2  3994  ss2rab  4094  difdif  4158  ddif  4164  unass  4195  unss  4213  undi  4304  vn0  4368  ab0orv  4406  disj  4473  ssindif0  4487  prneimg  4879  iinrab2  5093  unopab  5248  axrep5  5309  eqvinop  5507  pwssun  5590  dmun  5935  reldm0  5952  dmres  6041  imadmrn  6099  ssrnres  6209  dmsnn0  6238  coundi  6278  coundir  6279  resco  6281  cnvpo  6318  xpco  6320  dfpo2  6327  fun11  6652  fununi  6653  isarep1OLD  6668  fdmrn  6779  dffv2  7017  fsn  7169  eufnfv  7266  eloprabga  7558  eloprabgaOLD  7559  funoprabg  7571  ralrnmpo  7589  imaeqexov  7688  sucexeloniOLD  7846  suceloniOLD  7848  tfinds2  7901  funcnvuni  7972  oprabrexex2  8019  ralxp3f  8178  soseq  8200  dfer2  8764  euen1b  9092  xpsnen  9121  1sdomOLD  9312  wemapsolem  9619  zfregcl  9663  epfrs  9800  rankbnd  9937  rankbnd2  9938  rankxplim2  9949  rankxplim3  9950  isinfcard  10161  dfac5lem2  10193  dfac5lem5  10196  kmlem14  10233  kmlem15  10234  kmlem16  10235  axdc2lem  10517  axcclem  10526  ac9  10552  ac9s  10562  nnunb  12549  xrrebnd  13230  elfznelfzo  13822  hashfun  14486  hashtpg  14534  rexuz3  15397  imasaddfnlem  17588  isnsgrp  18761  eqg0subg  19236  dprd2d2  20088  isnirred  20446  subsubrng2  20590  subsubrg2  20627  isdomn2OLD  20734  mdetunilem8  22646  maducoeval2  22667  tgval2  22984  0top  23011  ssntr  23087  uncmp  23432  opnfbas  23871  fbunfip  23898  alexsubALTlem2  24077  alexsubALTlem3  24078  alexsubALT  24080  metrest  24558  cfilucfil3  25373  ellimc3  25934  plyun0  26256  sinhalfpilem  26523  2lgslem4  27468  addsdilem1  28195  addsdilem2  28196  mulsasslem1  28207  mulsasslem2  28208  dfcgra2  28856  colinearalg  28943  axcontlem5  29001  nb3grprlem2  29416  wlkeq  29670  isspthonpth  29785  clwlkclwwlklem2a4  30029  clwwlkn1  30073  clwwlkn2  30076  clwwlknon2x  30135  fusgreg2wsp  30368  h2hlm  31012  shlesb1i  31418  pjneli  31755  cnlnssadj  32112  pjin2i  32225  cvnbtwn2  32319  cvnbtwn4  32321  mdsl1i  32353  mdsl2i  32354  hatomistici  32394  cdj3lem3b  32472  iuninc  32583  disjex  32614  disjexc  32615  fpwrelmapffslem  32746  fpwrelmapffs  32748  mgcval  32960  isarchi2  33165  ismntop  33972  coinfliprv  34447  ballotlem2  34453  ballotlemi1  34467  plymulx  34525  oddprm2  34632  bnj168  34706  bnj153  34856  bnj605  34883  bnj607  34892  bnj986  34931  bnj1090  34955  bnj1128  34966  fineqvrep  35071  fmlasucdisj  35367  dfso2  35717  19.12b  35765  dfom5b  35876  elfuns  35879  dfint3  35916  hfext  36147  trer  36282  bj-alcomexcom  36646  wl-3xornot1  37446  wl-df3maxtru1  37458  cnambfre  37628  itg2addnclem2  37632  itg2addnc  37634  heiborlem1  37771  inxpxrn  38351  lssat  38972  islshpat  38973  lcvnbtwn2  38983  pclfinclN  39907  lhpex2leN  39970  diclspsn  41151  dihmeetlem4preN  41263  dihmeetlem13N  41276  lcdlss  41576  mapd1o  41605  eq0rabdioph  42732  rmspecnonsq  42863  rmxdioph  42973  wopprc  42987  islssfg2  43028  ifpan23  43422  ifpid1g  43456  minregex  43496  dfrtrcl5  43591  dfhe3  43737  ntrneikb  44056  scottabf  44209  2sbc6g  44384  2sbc5g  44385  iotasbc2  44389  2sb5nd  44531  2sb5ndVD  44881  2sb5ndALT  44903  limsupre2lem  45645  2rexsb  47016  2rexrsb  47017  usgrexmpl2nb2  47848  usgrexmpl2nb5  47851  usgrexmpl2trifr  47852  islindeps  48182  io1ii  48600