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  967  pm5.17  1028  pm4.83  1041  3or6  1475  nanim  1527  nannot  1528  empty  1935  19.12vvv  2023  19.12vv  2378  cvjust  2756  necon1abii  3005  nrexralim  3148  r19.23v  3191  nelb  3240  cbvralsvw  3315  spc3gv  3562  ralxpxfr2d  3604  sbc8g  3751  csbied  3888  dfss2  3922  ss2rab  4022  difdif  4088  ddif  4094  unass  4124  unss  4142  undi  4237  disj  4409  ssindif0  4423  prneimg  4818  iinrab2  5033  unopab  5190  axrep5  5245  eqvinop  5468  pwssun  5552  dmun  5899  reldm0  5917  dmres  6010  imadmrn  6071  ssrnres  6175  dmsnn0  6207  coundi  6247  coundir  6248  resco  6250  cnvpo  6288  xpco  6290  dfpo2  6297  fun11  6610  fununi  6611  fdmrn  6737  dffv2  6976  fsn  7131  eufnfv  7227  eloprabga  7521  funoprabg  7533  ralrnmpo  7551  imaeqexov  7650  tfinds2  7858  funcnvuni  7927  oprabrexex2  7973  ralxp3f  8131  soseq  8153  dfer2  8693  euen1b  9023  xpsnen  9047  wemapsolem  9510  zfregcl  9554  zfregclOLD  9555  epfrs  9698  rankbnd  9838  rankbnd2  9839  rankxplim2  9850  rankxplim3  9851  scottabf  9866  isinfcard  10083  dfac5lem2  10115  dfac5lem5  10118  kmlem14  10154  kmlem15  10155  kmlem16  10156  axdc2lem  10438  axcclem  10447  ac9  10473  ac9s  10483  nnunb  12506  xrrebnd  13200  elfznelfzo  13809  hashfun  14481  hashtpg  14529  rexuz3  15407  imasaddfnlem  17588  isnsgrp  18787  eqg0subg  19273  dprd2d2  20122  isnirred  20509  subsubrng2  20674  subsubrg2  20709  mdetunilem8  22787  maducoeval2  22808  tgval2  23124  0top  23151  ssntr  23226  uncmp  23571  opnfbas  24010  fbunfip  24037  alexsubALTlem2  24216  alexsubALTlem3  24217  alexsubALT  24219  metrest  24692  cfilucfil3  25490  ellimc3  26049  plyun0  26365  plymulidp  26454  sinhalfpilem  26639  2lgslem4  27581  addsdilem1  28355  addsdilem2  28356  mulsasslem1  28367  mulsasslem2  28368  dfcgra2  29152  colinearalg  29271  axcontlem5  29329  nb3grprlem2  29742  wlkeq  29994  isspthonpth  30109  clwlkclwwlklem2a4  30359  clwwlkn1  30403  clwwlkn2  30406  clwwlknon2x  30465  fusgreg2wsp  30698  h2hlm  31343  shlesb1i  31749  pjneli  32086  cnlnssadj  32443  pjin2i  32556  cvnbtwn2  32650  cvnbtwn4  32652  mdsl1i  32684  mdsl2i  32685  hatomistici  32725  cdj3lem3b  32803  iuninc  32916  disjex  32948  disjexc  32949  fpwrelmapffslem  33088  fpwrelmapffs  33090  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