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  1477  nanim  1528  nannot  1529  empty  1941  19.12vvv  2029  19.12vv  2380  cvjust  2757  necon1abii  3007  nrexralim  3150  r19.23v  3193  nelb  3242  cbvralsvw  3317  spc3gv  3562  ralxpxfr2d  3603  sbc8g  3750  csbied  3887  ss2rab  3997  difdif  4074  ddif  4080  dfss2  4097  unass  4173  unss  4191  undi  4233  disj  4406  ssindif0  4420  prneimg  4812  iinrab2  5031  unopab  5188  axrep5  5242  eqvinop  5460  eqvinot  5461  pwssun  5547  dmun  5899  reldm0  5917  dmres  6015  imadmrnOLD  6080  ssrnres  6182  dmsnn0  6221  coundi  6261  coundir  6262  resco  6264  cnvpo  6308  xpco  6310  dfpo2  6317  fun11  6636  fununi  6637  fdmrn  6763  dffv2  7003  fsn  7160  eufnfv  7258  eloprabga  7552  funoprabg  7564  ralrnmpo  7583  imaeqexov  7683  tfinds2  7899  funcnvuni  7968  oprabrexex2  8014  ralxp3f  8181  soseq  8203  dfer2  8746  euen1b  9083  xpsnen  9108  wemapsolem  9571  zfregcl  9615  zfregclOLD  9616  epfrs  9759  rankbnd  9912  rankbnd2  9913  rankxplim2  9924  rankxplim3  9925  scottabf  9966  isinfcard  10198  dfac5lem2  10230  dfac5lem5  10233  kmlem14  10269  kmlem15  10270  kmlem16  10271  axdc2lem  10553  axcclem  10562  ac9  10588  ac9s  10598  nnunb  12629  xrrebnd  13325  elfznelfzo  13935  hashfun  14609  hashtpg  14657  rexuz3  15545  imasaddfnlem  17729  isnsgrp  18941  eqg0subg  19440  dprd2d2  20290  isnirred  20680  subsubrng2  20846  subsubrg2  20881  mdetunilem8  22964  maducoeval2  22985  tgval2  23304  0top  23331  ssntr  23406  uncmp  23751  opnfbas  24191  fbunfip  24218  alexsubALTlem2  24397  alexsubALTlem3  24398  alexsubALT  24400  metrest  24873  cfilucfil3  25671  ellimc3  26229  plyun0  26545  plymulidp  26633  sinhalfpilem  26822  2lgslem4  27763  addsdilem1  28567  addsdilem2  28568  mulsasslem1  28579  mulsasslem2  28580  dfcgra2  29368  colinearalg  29518  axcontlem5  29576  nb3grprlem2  29992  wlkeq  30244  isspthonpth  30365  clwlkclwwlklem2a4  30618  clwwlkn1  30662  clwwlkn2  30665  clwwlknon2x  30724  fusgreg2wsp  30967  h2hlm  31612  shlesb1i  32018  pjneli  32355  cnlnssadj  32712  pjin2i  32825  cvnbtwn2  32919  cvnbtwn4  32921  mdsl1i  32953  mdsl2i  32954  hatomistici  32994  cdj3lem3b  33072  iuninc  33227  disjex  33258  disjexc  33259  fpwrelmapffslem  33394  fpwrelmapffs  33396  mgcval  33618  isarchi2  33816  elrgspnlem2  33874  ismntop  34728  coinfliprv  35185  ballotlem2  35191  ballotlemi1  35205  oddprm2  35354  bnj168  35431  bnj153  35580  bnj605  35607  bnj607  35616  bnj986  35655  bnj1090  35679  bnj1128  35690  fineqvrep  35882  axregszf  35897  axregs  35907  fmlasucdisj  36331  dfso2  36698  19.12b  36741  dfom5b  36852  elfuns  36855  dfint3  36894  hfext  37112  nmulprop  37117  trer  37282  bj-alcomexcom  37758  bj-dfres2  38141  wl-3xornot1  38595  wl-df3maxtru1  38607  cnambfre  38778  itg2addnclem2  38782  itg2addnc  38784  heiborlem1  38937  inxpxrn  39542  eldisjdmqsim  39941  lssat  40265  islshpat  40266  lcvnbtwn2  40276  pclfinclN  41199  lhpex2leN  41262  diclspsn  42443  dihmeetlem4preN  42555  dihmeetlem13N  42568  lcdlss  42868  mapd1o  42897  eq0rabdioph  43980  rmspecnonsq  44107  rmxdioph  44216  wopprc  44230  islssfg2  44266  ifpan23  44653  ifpid1g  44687  minregex  44727  dfrtrcl5  44821  dfhe3  44967  ntrneikb  45286  2sbc6g  45591  2sbc5g  45592  iotasbc2  45595  2sb5nd  45734  2sb5ndVD  46083  2sb5ndALT  46105  ssclaxsep  46167  permac8prim  46199  limsupre2lem  46939  2rexsb  48377  2rexrsb  48378  usgrexmpl2nb2  49336  usgrexmpl2nb5  49339  usgrexmpl2trifr  49340  islindeps  49770  io1ii  50240