Theorem bitr2i 279

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

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  3bitrri  301  3bitr2ri  303  3bitr4ri  307  nan  842  pm4.15  845  pm5.7  968  pm5.17  1027  pm4.83  1040  3or6  1474  nanim  1526  nannot  1527  empty  1934  19.12vvv  2022  19.12vv  2377  cvjust  2755  necon1abii  3004  nrexralim  3147  r19.23v  3190  nelb  3239  cbvralsvw  3314  spc3gv  3562  ralxpxfr2d  3604  sbc8g  3751  csbied  3888  dfss2  3922  ss2rab  4022  difdif  4088  ddif  4094  unass  4124  unss  4142  undi  4237  disj  4409  ssindif0  4423  prneimg  4818  iinrab2  5033  unopab  5190  axrep5  5245  eqvinop  5469  pwssun  5553  dmun  5900  reldm0  5918  dmres  6011  imadmrn  6072  ssrnres  6176  dmsnn0  6208  coundi  6248  coundir  6249  resco  6251  cnvpo  6288  xpco  6290  dfpo2  6297  fun11  6610  fununi  6611  fdmrn  6737  dffv2  6976  fsn  7131  eufnfv  7227  eloprabga  7519  funoprabg  7531  ralrnmpo  7549  imaeqexov  7648  tfinds2  7859  funcnvuni  7928  oprabrexex2  7974  ralxp3f  8132  soseq  8154  dfer2  8694  euen1b  9024  xpsnen  9048  wemapsolem  9511  zfregcl  9555  zfregclOLD  9556  epfrs  9699  rankbnd  9839  rankbnd2  9840  rankxplim2  9851  rankxplim3  9852  scottabf  9865  isinfcard  10075  dfac5lem2  10107  dfac5lem5  10110  kmlem14  10146  kmlem15  10147  kmlem16  10148  axdc2lem  10431  axcclem  10440  ac9  10466  ac9s  10476  nnunb  12499  xrrebnd  13193  elfznelfzo  13802  hashfun  14474  hashtpg  14522  rexuz3  15400  imasaddfnlem  17581  isnsgrp  18780  eqg0subg  19266  dprd2d2  20115  isnirred  20501  subsubrng2  20648  subsubrg2  20683  mdetunilem8  22755  maducoeval2  22776  tgval2  23092  0top  23119  ssntr  23194  uncmp  23539  opnfbas  23978  fbunfip  24005  alexsubALTlem2  24184  alexsubALTlem3  24185  alexsubALT  24187  metrest  24660  cfilucfil3  25458  ellimc3  26017  plyun0  26333  plymulidp  26422  sinhalfpilem  26604  2lgslem4  27546  addsdilem1  28320  addsdilem2  28321  mulsasslem1  28332  mulsasslem2  28333  dfcgra2  29114  colinearalg  29226  axcontlem5  29284  nb3grprlem2  29697  wlkeq  29949  isspthonpth  30064  clwlkclwwlklem2a4  30314  clwwlkn1  30358  clwwlkn2  30361  clwwlknon2x  30420  fusgreg2wsp  30653  h2hlm  31298  shlesb1i  31704  pjneli  32041  cnlnssadj  32398  pjin2i  32511  cvnbtwn2  32605  cvnbtwn4  32607  mdsl1i  32639  mdsl2i  32640  hatomistici  32680  cdj3lem3b  32758  iuninc  32871  disjex  32903  disjexc  32904  fpwrelmapffslem  33043  fpwrelmapffs  33045  mgcval  33273  isarchi2  33471  elrgspnlem2  33529  ismntop  34382  coinfliprv  34839  ballotlem2  34845  ballotlemi1  34859  oddprm2  35008  bnj168  35085  bnj153  35234  bnj605  35261  bnj607  35270  bnj986  35309  bnj1090  35333  bnj1128  35344  fineqvrep  35493  axregszf  35508  axregs  35518  fmlasucdisj  35857  dfso2  36213  19.12b  36257  dfom5b  36368  elfuns  36371  dfint3  36410  hfext  36641  nmulprop  36648  trer  36793  bj-alcomexcom  37269  wl-3xornot1  38092  wl-df3maxtru1  38104  cnambfre  38285  itg2addnclem2  38289  itg2addnc  38291  heiborlem1  38428  inxpxrn  39035  eldisjdmqsim  39434  lssat  39758  islshpat  39759  lcvnbtwn2  39769  pclfinclN  40692  lhpex2leN  40755  diclspsn  41936  dihmeetlem4preN  42048  dihmeetlem13N  42061  lcdlss  42361  mapd1o  42390  eq0rabdioph  43477  rmspecnonsq  43604  rmxdioph  43713  wopprc  43727  islssfg2  43768  ifpan23  44156  ifpid1g  44190  minregex  44230  dfrtrcl5  44325  dfhe3  44471  ntrneikb  44790  2sbc6g  45095  2sbc5g  45096  iotasbc2  45100  2sb5nd  45239  2sb5ndVD  45588  2sb5ndALT  45610  ssclaxsep  45661  permac8prim  45693  limsupre2lem  46408  2rexsb  47805  2rexrsb  47806  usgrexmpl2nb2  48765  usgrexmpl2nb5  48768  usgrexmpl2trifr  48769  islindeps  49200  io1ii  49666