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  3117  r19.23v  3161  nelb  3213  cbvralsvw  3290  spc3gv  3570  ralxpxfr2d  3612  sbc8g  3761  csbied  3898  dfss2  3932  ss2rab  4034  difdif  4098  ddif  4104  unass  4135  unss  4153  undi  4248  vn0  4308  ab0orv  4346  disj  4413  ssindif0  4427  prneimg  4818  iinrab2  5034  unopab  5187  axrep5  5242  eqvinop  5447  pwssun  5530  dmun  5874  reldm0  5891  dmres  5983  imadmrn  6041  ssrnres  6151  dmsnn0  6180  coundi  6220  coundir  6221  resco  6223  cnvpo  6260  xpco  6262  dfpo2  6269  fun11  6590  fununi  6591  isarep1OLD  6607  fdmrn  6719  dffv2  6956  fsn  7107  eufnfv  7203  eloprabga  7498  funoprabg  7510  ralrnmpo  7528  imaeqexov  7627  sucexeloniOLD  7786  tfinds2  7840  funcnvuni  7908  oprabrexex2  7957  ralxp3f  8116  soseq  8138  dfer2  8672  euen1b  8999  xpsnen  9025  1sdomOLD  9196  wemapsolem  9503  zfregcl  9547  epfrs  9684  rankbnd  9821  rankbnd2  9822  rankxplim2  9833  rankxplim3  9834  isinfcard  10045  dfac5lem2  10077  dfac5lem5  10080  kmlem14  10117  kmlem15  10118  kmlem16  10119  axdc2lem  10401  axcclem  10410  ac9  10436  ac9s  10446  nnunb  12438  xrrebnd  13128  elfznelfzo  13733  hashfun  14402  hashtpg  14450  rexuz3  15315  imasaddfnlem  17491  isnsgrp  18650  eqg0subg  19128  dprd2d2  19976  isnirred  20329  subsubrng2  20473  subsubrg2  20508  isdomn2OLD  20621  mdetunilem8  22506  maducoeval2  22527  tgval2  22843  0top  22870  ssntr  22945  uncmp  23290  opnfbas  23729  fbunfip  23756  alexsubALTlem2  23935  alexsubALTlem3  23936  alexsubALT  23938  metrest  24412  cfilucfil3  25220  ellimc3  25780  plyun0  26102  sinhalfpilem  26372  2lgslem4  27317  addsdilem1  28054  addsdilem2  28055  mulsasslem1  28066  mulsasslem2  28067  dfcgra2  28757  colinearalg  28837  axcontlem5  28895  nb3grprlem2  29308  wlkeq  29562  isspthonpth  29679  clwlkclwwlklem2a4  29926  clwwlkn1  29970  clwwlkn2  29973  clwwlknon2x  30032  fusgreg2wsp  30265  h2hlm  30909  shlesb1i  31315  pjneli  31652  cnlnssadj  32009  pjin2i  32122  cvnbtwn2  32216  cvnbtwn4  32218  mdsl1i  32250  mdsl2i  32251  hatomistici  32291  cdj3lem3b  32369  iuninc  32489  disjex  32521  disjexc  32522  fpwrelmapffslem  32655  fpwrelmapffs  32657  mgcval  32913  isarchi2  33139  elrgspnlem2  33194  ismntop  34016  coinfliprv  34474  ballotlem2  34480  ballotlemi1  34494  plymulx  34539  oddprm2  34646  bnj168  34720  bnj153  34870  bnj605  34897  bnj607  34906  bnj986  34945  bnj1090  34969  bnj1128  34980  fineqvrep  35085  fmlasucdisj  35386  dfso2  35742  19.12b  35789  dfom5b  35900  elfuns  35903  dfint3  35940  hfext  36171  trer  36304  bj-alcomexcom  36668  wl-3xornot1  37468  wl-df3maxtru1  37480  cnambfre  37662  itg2addnclem2  37666  itg2addnc  37668  heiborlem1  37805  inxpxrn  38381  lssat  39009  islshpat  39010  lcvnbtwn2  39020  pclfinclN  39944  lhpex2leN  40007  diclspsn  41188  dihmeetlem4preN  41300  dihmeetlem13N  41313  lcdlss  41613  mapd1o  41642  eq0rabdioph  42764  rmspecnonsq  42895  rmxdioph  43005  wopprc  43019  islssfg2  43060  ifpan23  43449  ifpid1g  43483  minregex  43523  dfrtrcl5  43618  dfhe3  43764  ntrneikb  44083  scottabf  44229  2sbc6g  44404  2sbc5g  44405  iotasbc2  44409  2sb5nd  44550  2sb5ndVD  44899  2sb5ndALT  44921  ssclaxsep  44972  permac8prim  45004  limsupre2lem  45722  2rexsb  47102  2rexrsb  47103  usgrexmpl2nb2  48024  usgrexmpl2nb5  48027  usgrexmpl2trifr  48028  islindeps  48442  io1ii  48909