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 ⊢ (𝜒 ↔ 𝜑)

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3bitrri  301  3bitr2ri  303  3bitr4ri  307  nan  842  pm4.15  845  pm5.7  968  pm5.17  1029  pm4.83  1042  3or6  1476  nanim  1528  nannot  1529  empty  1936  19.12vvv  2024  19.12vv  2379  cvjust  2757  necon1abii  3006  nrexralim  3149  r19.23v  3192  nelb  3241  cbvralsvw  3316  spc3gv  3563  ralxpxfr2d  3605  sbc8g  3752  csbied  3889  dfss2  3923  ss2rab  4023  difdif  4089  ddif  4095  unass  4125  unss  4143  undi  4238  disj  4410  ssindif0  4424  prneimg  4819  iinrab2  5034  unopab  5191  axrep5  5246  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  7856  funcnvuni  7925  oprabrexex2  7971  ralxp3f  8129  soseq  8151  dfer2  8691  euen1b  9021  xpsnen  9045  wemapsolem  9508  zfregcl  9552  zfregclOLD  9553  epfrs  9696  rankbnd  9836  rankbnd2  9837  rankxplim2  9848  rankxplim3  9849  scottabf  9864  isinfcard  10081  dfac5lem2  10113  dfac5lem5  10116  kmlem14  10152  kmlem15  10153  kmlem16  10154  axdc2lem  10436  axcclem  10445  ac9  10471  ac9s  10481  nnunb  12504  xrrebnd  13198  elfznelfzo  13807  hashfun  14479  hashtpg  14527  rexuz3  15405  imasaddfnlem  17586  isnsgrp  18785  eqg0subg  19271  dprd2d2  20120  isnirred  20507  subsubrng2  20672  subsubrg2  20707  mdetunilem8  22785  maducoeval2  22806  tgval2  23122  0top  23149  ssntr  23224  uncmp  23569  opnfbas  24008  fbunfip  24035  alexsubALTlem2  24214  alexsubALTlem3  24215  alexsubALT  24217  metrest  24690  cfilucfil3  25488  ellimc3  26047  plyun0  26363  plymulidp  26452  sinhalfpilem  26637  2lgslem4  27579  addsdilem1  28353  addsdilem2  28354  mulsasslem1  28365  mulsasslem2  28366  dfcgra2  29150  colinearalg  29269  axcontlem5  29327  nb3grprlem2  29740  wlkeq  29992  isspthonpth  30107  clwlkclwwlklem2a4  30357  clwwlkn1  30401  clwwlkn2  30404  clwwlknon2x  30463  fusgreg2wsp  30696  h2hlm  31341  shlesb1i  31747  pjneli  32084  cnlnssadj  32441  pjin2i  32554  cvnbtwn2  32648  cvnbtwn4  32650  mdsl1i  32682  mdsl2i  32683  hatomistici  32723  cdj3lem3b  32801  iuninc  32914  disjex  32946  disjexc  32947  fpwrelmapffslem  33086  fpwrelmapffs  33088  mgcval  33316  isarchi2  33514  elrgspnlem2  33572  ismntop  34425  coinfliprv  34882  ballotlem2  34888  ballotlemi1  34902  oddprm2  35051  bnj168  35128  bnj153  35277  bnj605  35304  bnj607  35313  bnj986  35352  bnj1090  35376  bnj1128  35387  fineqvrep  35535  axregszf  35550  axregs  35560  fmlasucdisj  35899  dfso2  36255  19.12b  36299  dfom5b  36410  elfuns  36413  dfint3  36452  hfext  36683  nmulprop  36690  trer  36855  bj-alcomexcom  37331  wl-3xornot1  38154  wl-df3maxtru1  38166  cnambfre  38347  itg2addnclem2  38351  itg2addnc  38353  heiborlem1  38490  inxpxrn  39095  eldisjdmqsim  39494  lssat  39818  islshpat  39819  lcvnbtwn2  39829  pclfinclN  40752  lhpex2leN  40815  diclspsn  41996  dihmeetlem4preN  42108  dihmeetlem13N  42121  lcdlss  42421  mapd1o  42450  eq0rabdioph  43535  rmspecnonsq  43662  rmxdioph  43771  wopprc  43785  islssfg2  43826  ifpan23  44214  ifpid1g  44248  minregex  44288  dfrtrcl5  44383  dfhe3  44529  ntrneikb  44848  2sbc6g  45153  2sbc5g  45154  iotasbc2  45158  2sb5nd  45297  2sb5ndVD  45646  2sb5ndALT  45668  ssclaxsep  45719  permac8prim  45751  limsupre2lem  46466  2rexsb  47866  2rexrsb  47867  usgrexmpl2nb2  48826  usgrexmpl2nb5  48829  usgrexmpl2trifr  48830  islindeps  49261  io1ii  49727