Theorem bitr2i 278

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

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  3bitrri  300  3bitr2ri  302  3bitr4ri  306  nan  827  pm4.15  830  pm5.7  950  pm5.17  1008  pm4.83  1021  3or6  1443  nanim  1487  nannot  1488  empty  1903  19.12vvv  1991  19.12vv  2364  cvjust  2816  abbi  2888  abbiOLD  2955  necon1abii  3064  nabbi  3121  ralnex2OLD  3261  ralnex3OLD  3263  nrexralim  3266  r19.23v  3279  spc3gv  3604  ralxpxfr2d  3638  sbc8g  3779  ss2rab  4046  difdif  4106  ddif  4112  unass  4141  unss  4159  undi  4250  disj  4398  ssindif0  4412  prneimg  4784  pwsnALT  4830  iinrab2  4991  unopab  5144  axrep5  5195  eqvinop  5377  pwssun  5455  dmun  5778  reldm0  5797  dmres  5874  imadmrn  5938  ssrnres  6034  dmsnn0  6063  coundi  6099  coundir  6100  resco  6102  cnvpo  6137  xpco  6139  fun11  6427  fununi  6428  isarep1  6441  fdmrn  6537  dffv2  6755  fsn  6896  eufnfv  6990  eloprabga  7260  funoprabg  7272  ralrnmpo  7288  suceloni  7527  tfinds2  7577  funcnvuni  7635  oprabrexex2  7678  fsplitOLD  7812  dfer2  8289  euen1b  8579  xpsnen  8600  1sdom  8720  wemapsolem  9013  zfregcl  9057  epfrs  9172  rankbnd  9296  rankbnd2  9297  rankxplim2  9308  rankxplim3  9309  isinfcard  9517  dfac5lem2  9549  dfac5lem5  9552  kmlem14  9588  kmlem15  9589  kmlem16  9590  axdc2lem  9869  axcclem  9878  ac9  9904  ac9s  9914  nnunb  11892  xrrebnd  12560  elfznelfzo  13141  hashfun  13797  hashtpg  13842  rexuz3  14707  imasaddfnlem  16800  isnsgrp  17904  dprd2d2  19165  isnirred  19449  subsubrg2  19561  isdomn2  20071  mdetunilem8  21227  maducoeval2  21248  tgval2  21563  0top  21590  ssntr  21665  uncmp  22010  opnfbas  22449  fbunfip  22476  alexsubALTlem2  22655  alexsubALTlem3  22656  alexsubALT  22658  metrest  23133  cfilucfil3  23922  ellimc3  24476  plyun0  24786  sinhalfpilem  25048  2lgslem4  25981  dfcgra2  26615  colinearalg  26695  axcontlem5  26753  nb3grprlem2  27162  wlkeq  27414  isspthonpth  27529  clwlkclwwlklem2a4  27774  clwwlkn1  27818  clwwlkn2  27821  clwwlknon2x  27881  fusgreg2wsp  28114  h2hlm  28756  shlesb1i  29162  pjneli  29499  cnlnssadj  29856  pjin2i  29969  cvnbtwn2  30063  cvnbtwn4  30065  mdsl1i  30097  mdsl2i  30098  hatomistici  30138  cdj3lem3b  30216  nelbOLD  30231  iuninc  30311  disjex  30341  disjexc  30342  fpwrelmapffslem  30467  fpwrelmapffs  30469  isarchi2  30814  ismntop  31267  coinfliprv  31740  ballotlem2  31746  ballotlemi1  31760  plymulx  31818  oddprm2  31926  bnj168  32000  bnj153  32152  bnj605  32179  bnj607  32188  bnj986  32227  bnj1090  32251  bnj1128  32262  fmlasucdisj  32646  dfso2  32990  dfpo2  32991  19.12b  33046  soseq  33096  dfom5b  33373  elfuns  33376  dfint3  33413  hfext  33644  trer  33664  cnambfre  34939  itg2addnclem2  34943  itg2addnc  34945  heiborlem1  35088  inxpxrn  35642  lssat  36151  islshpat  36152  lcvnbtwn2  36162  pclfinclN  37085  lhpex2leN  37148  diclspsn  38329  dihmeetlem4preN  38441  dihmeetlem13N  38454  lcdlss  38754  mapd1o  38783  eq0rabdioph  39371  rmspecnonsq  39502  rmxdioph  39611  wopprc  39625  islssfg2  39669  ifpan23  39823  ifpid1g  39858  dfrtrcl5  39987  dfhe3  40119  ntrneikb  40442  scottabf  40574  2sbc6g  40745  2sbc5g  40746  iotasbc2  40750  2sb5nd  40892  2sb5ndVD  41242  2sb5ndALT  41264  limsupre2lem  42003  2rexsb  43298  2rexrsb  43299  islindeps  44507