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  843  pm4.15  846  pm5.7  968  pm5.17  1029  pm4.83  1042  3or6  1476  nanim  1528  nannot  1529  empty  1939  19.12vvv  2027  19.12vv  2376  cvjust  2754  necon1abii  3003  nrexralim  3146  r19.23v  3189  nelb  3238  cbvralsvw  3313  spc3gv  3558  ralxpxfr2d  3599  sbc8g  3746  csbied  3882  dfss2  3916  ss2rab  4016  difdif  4081  ddif  4087  unass  4117  unss  4135  undi  4230  disj  4402  ssindif0  4416  prneimg  4813  iinrab2  5027  unopab  5184  axrep5  5238  eqvinop  5455  pwssun  5539  dmun  5888  reldm0  5906  dmres  5999  imadmrn  6060  ssrnres  6165  dmsnn0  6197  coundi  6237  coundir  6238  resco  6240  cnvpo  6279  xpco  6281  dfpo2  6288  fun11  6602  fununi  6603  fdmrn  6729  dffv2  6968  fsn  7124  eufnfv  7223  eloprabga  7517  funoprabg  7529  ralrnmpo  7547  imaeqexov  7647  tfinds2  7858  funcnvuni  7927  oprabrexex2  7973  ralxp3f  8132  soseq  8154  dfer2  8696  euen1b  9033  xpsnen  9058  wemapsolem  9522  zfregcl  9566  zfregclOLD  9567  epfrs  9710  rankbnd  9858  rankbnd2  9859  rankxplim2  9870  rankxplim3  9871  scottabf  9911  isinfcard  10143  dfac5lem2  10175  dfac5lem5  10178  kmlem14  10214  kmlem15  10215  kmlem16  10216  axdc2lem  10498  axcclem  10507  ac9  10533  ac9s  10543  nnunb  12572  xrrebnd  13268  elfznelfzo  13877  hashfun  14550  hashtpg  14598  rexuz3  15484  imasaddfnlem  17662  isnsgrp  18874  eqg0subg  19373  dprd2d2  20222  isnirred  20612  subsubrng2  20778  subsubrg2  20813  mdetunilem8  22896  maducoeval2  22917  tgval2  23236  0top  23263  ssntr  23338  uncmp  23683  opnfbas  24123  fbunfip  24150  alexsubALTlem2  24329  alexsubALTlem3  24330  alexsubALT  24332  metrest  24805  cfilucfil3  25603  ellimc3  26161  plyun0  26477  plymulidp  26567  sinhalfpilem  26756  2lgslem4  27697  addsdilem1  28471  addsdilem2  28472  mulsasslem1  28483  mulsasslem2  28484  dfcgra2  29272  colinearalg  29422  axcontlem5  29480  nb3grprlem2  29896  wlkeq  30148  isspthonpth  30269  clwlkclwwlklem2a4  30522  clwwlkn1  30566  clwwlkn2  30569  clwwlknon2x  30628  fusgreg2wsp  30871  h2hlm  31516  shlesb1i  31922  pjneli  32259  cnlnssadj  32616  pjin2i  32729  cvnbtwn2  32823  cvnbtwn4  32825  mdsl1i  32857  mdsl2i  32858  hatomistici  32898  cdj3lem3b  32976  iuninc  33089  disjex  33120  disjexc  33121  fpwrelmapffslem  33258  fpwrelmapffs  33260  mgcval  33482  isarchi2  33680  elrgspnlem2  33738  ismntop  34592  coinfliprv  35050  ballotlem2  35056  ballotlemi1  35070  oddprm2  35219  bnj168  35296  bnj153  35445  bnj605  35472  bnj607  35481  bnj986  35520  bnj1090  35544  bnj1128  35555  fineqvrep  35707  axregszf  35722  axregs  35732  fmlasucdisj  36085  dfso2  36441  19.12b  36485  dfom5b  36596  elfuns  36599  dfint3  36638  hfext  36856  nmulprop  36861  trer  37026  bj-alcomexcom  37502  wl-3xornot1  38323  wl-df3maxtru1  38335  cnambfre  38506  itg2addnclem2  38510  itg2addnc  38512  heiborlem1  38665  inxpxrn  39270  eldisjdmqsim  39669  lssat  39993  islshpat  39994  lcvnbtwn2  40004  pclfinclN  40927  lhpex2leN  40990  diclspsn  42171  dihmeetlem4preN  42283  dihmeetlem13N  42296  lcdlss  42596  mapd1o  42625  eq0rabdioph  43725  rmspecnonsq  43852  rmxdioph  43961  wopprc  43975  islssfg2  44016  ifpan23  44404  ifpid1g  44438  minregex  44478  dfrtrcl5  44573  dfhe3  44719  ntrneikb  45038  2sbc6g  45343  2sbc5g  45344  iotasbc2  45348  2sb5nd  45487  2sb5ndVD  45836  2sb5ndALT  45858  ssclaxsep  45909  permac8prim  45941  limsupre2lem  46656  2rexsb  48093  2rexrsb  48094  usgrexmpl2nb2  49053  usgrexmpl2nb5  49056  usgrexmpl2trifr  49057  islindeps  49487  io1ii  49951