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  2793  abbi  2865  abbiOLD  2930  necon1abii  3035  nabbi  3089  nrexralim  3225  r19.23v  3238  spc3gv  3553  ralxpxfr2d  3587  sbc8g  3728  ss2rab  3998  difdif  4058  ddif  4064  unass  4093  unss  4111  undi  4201  disj  4355  disjOLD  4356  ssindif0  4371  prneimg  4745  pwsnOLD  4793  iinrab2  4955  unopab  5109  axrep5  5160  eqvinop  5343  pwssun  5421  dmun  5743  reldm0  5762  dmres  5840  imadmrn  5906  ssrnres  6002  dmsnn0  6031  coundi  6067  coundir  6068  resco  6070  cnvpo  6106  xpco  6108  fun11  6398  fununi  6399  isarep1  6412  fdmrn  6512  dffv2  6733  fsn  6874  eufnfv  6969  eloprabga  7240  funoprabg  7252  ralrnmpo  7268  suceloni  7508  tfinds2  7558  funcnvuni  7618  oprabrexex2  7661  fsplitOLD  7796  dfer2  8273  euen1b  8563  xpsnen  8584  1sdom  8705  wemapsolem  8998  zfregcl  9042  epfrs  9157  rankbnd  9281  rankbnd2  9282  rankxplim2  9293  rankxplim3  9294  isinfcard  9503  dfac5lem2  9535  dfac5lem5  9538  kmlem14  9574  kmlem15  9575  kmlem16  9576  axdc2lem  9859  axcclem  9868  ac9  9894  ac9s  9904  nnunb  11881  xrrebnd  12549  elfznelfzo  13137  hashfun  13794  hashtpg  13839  rexuz3  14700  imasaddfnlem  16793  isnsgrp  17897  dprd2d2  19159  isnirred  19446  subsubrg2  19555  isdomn2  20065  mdetunilem8  21224  maducoeval2  21245  tgval2  21561  0top  21588  ssntr  21663  uncmp  22008  opnfbas  22447  fbunfip  22474  alexsubALTlem2  22653  alexsubALTlem3  22654  alexsubALT  22656  metrest  23131  cfilucfil3  23924  ellimc3  24482  plyun0  24794  sinhalfpilem  25056  2lgslem4  25990  dfcgra2  26624  colinearalg  26704  axcontlem5  26762  nb3grprlem2  27171  wlkeq  27423  isspthonpth  27538  clwlkclwwlklem2a4  27782  clwwlkn1  27826  clwwlkn2  27829  clwwlknon2x  27888  fusgreg2wsp  28121  h2hlm  28763  shlesb1i  29169  pjneli  29506  cnlnssadj  29863  pjin2i  29976  cvnbtwn2  30070  cvnbtwn4  30072  mdsl1i  30104  mdsl2i  30105  hatomistici  30145  cdj3lem3b  30223  nelbOLD  30239  iuninc  30324  disjex  30355  disjexc  30356  fpwrelmapffslem  30494  fpwrelmapffs  30496  mgcval  30695  isarchi2  30864  ismntop  31377  coinfliprv  31850  ballotlem2  31856  ballotlemi1  31870  plymulx  31928  oddprm2  32036  bnj168  32110  bnj153  32262  bnj605  32289  bnj607  32298  bnj986  32337  bnj1090  32361  bnj1128  32372  fmlasucdisj  32759  dfso2  33103  dfpo2  33104  19.12b  33159  soseq  33209  dfom5b  33486  elfuns  33489  dfint3  33526  hfext  33757  trer  33777  wl-3xornot1  34897  wl-df3maxtru1  34909  cnambfre  35105  itg2addnclem2  35109  itg2addnc  35111  heiborlem1  35249  inxpxrn  35803  lssat  36312  islshpat  36313  lcvnbtwn2  36323  pclfinclN  37246  lhpex2leN  37309  diclspsn  38490  dihmeetlem4preN  38602  dihmeetlem13N  38615  lcdlss  38915  mapd1o  38944  eq0rabdioph  39717  rmspecnonsq  39848  rmxdioph  39957  wopprc  39971  islssfg2  40015  ifpan23  40168  ifpid1g  40202  dfrtrcl5  40329  dfhe3  40476  ntrneikb  40797  scottabf  40948  2sbc6g  41119  2sbc5g  41120  iotasbc2  41124  2sb5nd  41266  2sb5ndVD  41616  2sb5ndALT  41638  limsupre2lem  42366  2rexsb  43656  2rexrsb  43657  islindeps  44862