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  3113  r19.23v  3156  nelb  3205  cbvralsvw  3280  spc3gv  3556  ralxpxfr2d  3598  sbc8g  3746  csbied  3883  dfss2  3917  ss2rab  4018  difdif  4082  ddif  4088  unass  4119  unss  4137  undi  4232  vn0  4292  ab0orv  4330  disj  4397  ssindif0  4411  prneimg  4803  iinrab2  5015  unopab  5168  axrep5  5222  eqvinop  5424  pwssun  5505  dmun  5847  reldm0  5864  dmres  5957  imadmrn  6015  ssrnres  6121  dmsnn0  6150  coundi  6190  coundir  6191  resco  6193  cnvpo  6229  xpco  6231  dfpo2  6238  fun11  6550  fununi  6551  fdmrn  6677  dffv2  6911  fsn  7062  eufnfv  7157  eloprabga  7449  funoprabg  7461  ralrnmpo  7479  imaeqexov  7578  tfinds2  7788  funcnvuni  7856  oprabrexex2  7904  ralxp3f  8061  soseq  8083  dfer2  8617  euen1b  8944  xpsnen  8968  wemapsolem  9430  zfregcl  9474  zfregclOLD  9475  epfrs  9615  rankbnd  9752  rankbnd2  9753  rankxplim2  9764  rankxplim3  9765  isinfcard  9974  dfac5lem2  10006  dfac5lem5  10009  kmlem14  10046  kmlem15  10047  kmlem16  10048  axdc2lem  10330  axcclem  10339  ac9  10365  ac9s  10375  nnunb  12368  xrrebnd  13058  elfznelfzo  13663  hashfun  14332  hashtpg  14380  rexuz3  15243  imasaddfnlem  17419  isnsgrp  18584  eqg0subg  19062  dprd2d2  19912  isnirred  20292  subsubrng2  20433  subsubrg2  20468  isdomn2OLD  20581  mdetunilem8  22488  maducoeval2  22509  tgval2  22825  0top  22852  ssntr  22927  uncmp  23272  opnfbas  23711  fbunfip  23738  alexsubALTlem2  23917  alexsubALTlem3  23918  alexsubALT  23920  metrest  24393  cfilucfil3  25201  ellimc3  25761  plyun0  26083  sinhalfpilem  26353  2lgslem4  27298  addsdilem1  28044  addsdilem2  28045  mulsasslem1  28056  mulsasslem2  28057  dfcgra2  28762  colinearalg  28842  axcontlem5  28900  nb3grprlem2  29313  wlkeq  29566  isspthonpth  29681  clwlkclwwlklem2a4  29928  clwwlkn1  29972  clwwlkn2  29975  clwwlknon2x  30034  fusgreg2wsp  30267  h2hlm  30911  shlesb1i  31317  pjneli  31654  cnlnssadj  32011  pjin2i  32124  cvnbtwn2  32218  cvnbtwn4  32220  mdsl1i  32252  mdsl2i  32253  hatomistici  32293  cdj3lem3b  32371  iuninc  32492  disjex  32524  disjexc  32525  fpwrelmapffslem  32667  fpwrelmapffs  32669  mgcval  32924  isarchi2  33122  elrgspnlem2  33178  ismntop  34007  coinfliprv  34464  ballotlem2  34470  ballotlemi1  34484  plymulx  34529  oddprm2  34636  bnj168  34710  bnj153  34860  bnj605  34887  bnj607  34896  bnj986  34935  bnj1090  34959  bnj1128  34970  axregszf  35077  fineqvrep  35083  axregs  35091  fmlasucdisj  35389  dfso2  35745  19.12b  35792  dfom5b  35903  elfuns  35906  dfint3  35943  hfext  36174  trer  36307  bj-alcomexcom  36671  wl-3xornot1  37471  wl-df3maxtru1  37483  cnambfre  37665  itg2addnclem2  37669  itg2addnc  37671  heiborlem1  37808  inxpxrn  38384  lssat  39012  islshpat  39013  lcvnbtwn2  39023  pclfinclN  39946  lhpex2leN  40009  diclspsn  41190  dihmeetlem4preN  41302  dihmeetlem13N  41315  lcdlss  41615  mapd1o  41644  eq0rabdioph  42766  rmspecnonsq  42897  rmxdioph  43006  wopprc  43020  islssfg2  43061  ifpan23  43450  ifpid1g  43484  minregex  43524  dfrtrcl5  43619  dfhe3  43765  ntrneikb  44084  scottabf  44230  2sbc6g  44405  2sbc5g  44406  iotasbc2  44410  2sb5nd  44550  2sb5ndVD  44899  2sb5ndALT  44921  ssclaxsep  44972  permac8prim  45004  limsupre2lem  45719  2rexsb  47099  2rexrsb  47100  usgrexmpl2nb2  48031  usgrexmpl2nb5  48034  usgrexmpl2trifr  48035  islindeps  48452  io1ii  48919