Theorem bitr2i 275

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

Syntax hints:   ↔ wb 205

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 206

This theorem is referenced by:  3bitrri  298  3bitr2ri  300  3bitr4ri  304  nan  827  pm4.15  830  pm5.7  951  pm5.17  1009  pm4.83  1022  3or6  1446  nanim  1493  nannot  1494  empty  1910  19.12vvv  1993  19.12vv  2346  cvjust  2733  abbi  2811  abbiOLD  2881  necon1abii  2993  nabbi  3048  nrexralim  3194  nelb  3196  r19.23v  3209  spc3gv  3544  ralxpxfr2d  3577  sbc8g  3725  csbied  3871  ss2rab  4005  difdif  4066  ddif  4072  unass  4101  unss  4119  undi  4209  vn0  4273  ab0orv  4313  disj  4382  disjOLD  4383  ssindif0  4398  prneimg  4786  pwsnOLD  4833  iinrab2  5000  unopab  5157  axrep5  5216  eqvinop  5402  pwssun  5486  dmun  5822  reldm0  5840  dmres  5916  imadmrn  5982  ssrnres  6086  dmsnn0  6115  coundi  6155  coundir  6156  resco  6158  cnvpo  6194  xpco  6196  dfpo2  6203  fun11  6515  fununi  6516  isarep1OLD  6531  fdmrn  6641  dffv2  6872  fsn  7016  eufnfv  7114  eloprabga  7391  eloprabgaOLD  7392  funoprabg  7404  ralrnmpo  7421  sucexeloni  7667  suceloniOLD  7669  tfinds2  7719  funcnvuni  7787  oprabrexex2  7830  fsplitOLD  7967  dfer2  8508  euen1b  8826  xpsnen  8851  1sdom  9034  wemapsolem  9318  zfregcl  9362  epfrs  9498  rankbnd  9635  rankbnd2  9636  rankxplim2  9647  rankxplim3  9648  isinfcard  9857  dfac5lem2  9889  dfac5lem5  9892  kmlem14  9928  kmlem15  9929  kmlem16  9930  axdc2lem  10213  axcclem  10222  ac9  10248  ac9s  10258  nnunb  12238  xrrebnd  12911  elfznelfzo  13501  hashfun  14161  hashtpg  14208  rexuz3  15069  imasaddfnlem  17248  isnsgrp  18388  dprd2d2  19656  isnirred  19951  subsubrg2  20060  isdomn2  20579  mdetunilem8  21777  maducoeval2  21798  tgval2  22115  0top  22142  ssntr  22218  uncmp  22563  opnfbas  23002  fbunfip  23029  alexsubALTlem2  23208  alexsubALTlem3  23209  alexsubALT  23211  metrest  23689  cfilucfil3  24493  ellimc3  25052  plyun0  25367  sinhalfpilem  25629  2lgslem4  26563  dfcgra2  27200  colinearalg  27287  axcontlem5  27345  nb3grprlem2  27757  wlkeq  28010  isspthonpth  28126  clwlkclwwlklem2a4  28370  clwwlkn1  28414  clwwlkn2  28417  clwwlknon2x  28476  fusgreg2wsp  28709  h2hlm  29351  shlesb1i  29757  pjneli  30094  cnlnssadj  30451  pjin2i  30564  cvnbtwn2  30658  cvnbtwn4  30660  mdsl1i  30692  mdsl2i  30693  hatomistici  30733  cdj3lem3b  30811  nelbOLDOLD  30826  iuninc  30909  disjex  30940  disjexc  30941  fpwrelmapffslem  31076  fpwrelmapffs  31078  mgcval  31274  isarchi2  31448  ismntop  31985  coinfliprv  32458  ballotlem2  32464  ballotlemi1  32478  plymulx  32536  oddprm2  32644  bnj168  32718  bnj153  32869  bnj605  32896  bnj607  32905  bnj986  32944  bnj1090  32968  bnj1128  32979  fineqvrep  33073  fmlasucdisj  33370  dfso2  33731  19.12b  33786  xpord3ind  33809  soseq  33812  dfom5b  34223  elfuns  34226  dfint3  34263  hfext  34494  trer  34514  wl-3xornot1  35660  wl-df3maxtru1  35672  cnambfre  35834  itg2addnclem2  35838  itg2addnc  35840  heiborlem1  35978  inxpxrn  36528  lssat  37037  islshpat  37038  lcvnbtwn2  37048  pclfinclN  37971  lhpex2leN  38034  diclspsn  39215  dihmeetlem4preN  39327  dihmeetlem13N  39340  lcdlss  39640  mapd1o  39669  eq0rabdioph  40605  rmspecnonsq  40736  rmxdioph  40845  wopprc  40859  islssfg2  40903  ifpan23  41074  ifpid1g  41108  minregex  41148  dfrtrcl5  41244  dfhe3  41390  ntrneikb  41711  scottabf  41865  2sbc6g  42040  2sbc5g  42041  iotasbc2  42045  2sb5nd  42187  2sb5ndVD  42537  2sb5ndALT  42559  limsupre2lem  43272  2rexsb  44604  2rexrsb  44605  islindeps  45805  io1ii  46225