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  828  pm4.15  831  pm5.7  951  pm5.17  1009  pm4.83  1022  3or6  1444  nanim  1489  nannot  1490  empty  1907  19.12vvv  1995  19.12vv  2357  cvjust  2752  abbi  2825  abbiOLD  2892  necon1abii  2999  nabbi  3053  nrexralim  3190  r19.23v  3203  spc3gv  3523  ralxpxfr2d  3557  sbc8g  3704  ss2rab  3975  difdif  4036  ddif  4042  unass  4071  unss  4089  undi  4179  vn0  4237  ab0orv  4275  disj  4344  disjOLD  4345  ssindif0  4360  prneimg  4742  pwsnOLD  4791  iinrab2  4957  unopab  5111  axrep5  5162  eqvinop  5346  pwssun  5426  dmun  5750  reldm0  5769  dmres  5845  imadmrn  5911  ssrnres  6007  dmsnn0  6036  coundi  6077  coundir  6078  resco  6080  cnvpo  6116  xpco  6118  fun11  6409  fununi  6410  isarep1  6423  fdmrn  6523  dffv2  6747  fsn  6888  eufnfv  6983  eloprabga  7255  funoprabg  7267  ralrnmpo  7284  suceloni  7527  tfinds2  7577  funcnvuni  7641  oprabrexex2  7683  fsplitOLD  7818  dfer2  8300  euen1b  8599  xpsnen  8622  1sdom  8759  wemapsolem  9047  zfregcl  9091  epfrs  9206  rankbnd  9330  rankbnd2  9331  rankxplim2  9342  rankxplim3  9343  isinfcard  9552  dfac5lem2  9584  dfac5lem5  9587  kmlem14  9623  kmlem15  9624  kmlem16  9625  axdc2lem  9908  axcclem  9917  ac9  9943  ac9s  9953  nnunb  11930  xrrebnd  12602  elfznelfzo  13191  hashfun  13848  hashtpg  13895  rexuz3  14756  imasaddfnlem  16859  isnsgrp  17971  dprd2d2  19234  isnirred  19521  subsubrg2  19630  isdomn2  20140  mdetunilem8  21319  maducoeval2  21340  tgval2  21656  0top  21683  ssntr  21758  uncmp  22103  opnfbas  22542  fbunfip  22569  alexsubALTlem2  22748  alexsubALTlem3  22749  alexsubALT  22751  metrest  23226  cfilucfil3  24020  ellimc3  24578  plyun0  24893  sinhalfpilem  25155  2lgslem4  26089  dfcgra2  26723  colinearalg  26803  axcontlem5  26861  nb3grprlem2  27270  wlkeq  27522  isspthonpth  27637  clwlkclwwlklem2a4  27881  clwwlkn1  27925  clwwlkn2  27928  clwwlknon2x  27987  fusgreg2wsp  28220  h2hlm  28862  shlesb1i  29268  pjneli  29605  cnlnssadj  29962  pjin2i  30075  cvnbtwn2  30169  cvnbtwn4  30171  mdsl1i  30203  mdsl2i  30204  hatomistici  30244  cdj3lem3b  30322  nelbOLD  30338  iuninc  30422  disjex  30453  disjexc  30454  fpwrelmapffslem  30591  fpwrelmapffs  30593  mgcval  30791  isarchi2  30965  ismntop  31495  coinfliprv  31968  ballotlem2  31974  ballotlemi1  31988  plymulx  32046  oddprm2  32154  bnj168  32228  bnj153  32380  bnj605  32407  bnj607  32416  bnj986  32455  bnj1090  32479  bnj1128  32490  fmlasucdisj  32877  dfso2  33237  dfpo2  33238  19.12b  33293  xpord3ind  33355  soseq  33358  dfom5b  33785  elfuns  33788  dfint3  33825  hfext  34056  trer  34076  wl-3xornot1  35199  wl-df3maxtru1  35211  cnambfre  35407  itg2addnclem2  35411  itg2addnc  35413  heiborlem1  35551  inxpxrn  36105  lssat  36614  islshpat  36615  lcvnbtwn2  36625  pclfinclN  37548  lhpex2leN  37611  diclspsn  38792  dihmeetlem4preN  38904  dihmeetlem13N  38917  lcdlss  39217  mapd1o  39246  eq0rabdioph  40112  rmspecnonsq  40243  rmxdioph  40352  wopprc  40366  islssfg2  40410  ifpan23  40563  ifpid1g  40597  dfrtrcl5  40724  dfhe3  40871  ntrneikb  41192  scottabf  41343  2sbc6g  41514  2sbc5g  41515  iotasbc2  41519  2sb5nd  41661  2sb5ndVD  42011  2sb5ndALT  42033  limsupre2lem  42754  2rexsb  44046  2rexrsb  44047  islindeps  45249