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  2378  cvjust  2756  necon1abii  3005  nrexralim  3148  r19.23v  3191  nelb  3240  cbvralsvw  3315  spc3gv  3561  ralxpxfr2d  3603  sbc8g  3750  csbied  3886  dfss2  3920  ss2rab  4020  difdif  4085  ddif  4091  unass  4121  unss  4139  undi  4234  disj  4406  ssindif0  4420  prneimg  4817  iinrab2  5032  unopab  5189  axrep5  5244  eqvinop  5467  pwssun  5551  dmun  5898  reldm0  5916  dmres  6009  imadmrn  6070  ssrnres  6175  dmsnn0  6207  coundi  6247  coundir  6248  resco  6250  cnvpo  6289  xpco  6291  dfpo2  6298  fun11  6611  fununi  6612  fdmrn  6738  dffv2  6977  fsn  7132  eufnfv  7231  eloprabga  7525  funoprabg  7537  ralrnmpo  7555  imaeqexov  7655  tfinds2  7863  funcnvuni  7932  oprabrexex2  7978  ralxp3f  8138  soseq  8160  dfer2  8700  euen1b  9037  xpsnen  9062  wemapsolem  9525  zfregcl  9569  zfregclOLD  9570  epfrs  9713  rankbnd  9853  rankbnd2  9854  rankxplim2  9865  rankxplim3  9866  scottabf  9881  isinfcard  10098  dfac5lem2  10130  dfac5lem5  10133  kmlem14  10169  kmlem15  10170  kmlem16  10171  axdc2lem  10453  axcclem  10462  ac9  10488  ac9s  10498  nnunb  12527  xrrebnd  13222  elfznelfzo  13831  hashfun  14504  hashtpg  14552  rexuz3  15438  imasaddfnlem  17618  isnsgrp  18829  eqg0subg  19328  dprd2d2  20177  isnirred  20565  subsubrng2  20730  subsubrg2  20765  mdetunilem8  22845  maducoeval2  22866  tgval2  23185  0top  23212  ssntr  23287  uncmp  23632  opnfbas  24072  fbunfip  24099  alexsubALTlem2  24278  alexsubALTlem3  24279  alexsubALT  24281  metrest  24754  cfilucfil3  25552  ellimc3  26111  plyun0  26427  plymulidp  26516  sinhalfpilem  26701  2lgslem4  27643  addsdilem1  28417  addsdilem2  28418  mulsasslem1  28429  mulsasslem2  28430  dfcgra2  29218  colinearalg  29368  axcontlem5  29426  nb3grprlem2  29842  wlkeq  30094  isspthonpth  30215  clwlkclwwlklem2a4  30468  clwwlkn1  30512  clwwlkn2  30515  clwwlknon2x  30574  fusgreg2wsp  30817  h2hlm  31462  shlesb1i  31868  pjneli  32205  cnlnssadj  32562  pjin2i  32675  cvnbtwn2  32769  cvnbtwn4  32771  mdsl1i  32803  mdsl2i  32804  hatomistici  32844  cdj3lem3b  32922  iuninc  33035  disjex  33067  disjexc  33068  fpwrelmapffslem  33205  fpwrelmapffs  33207  mgcval  33429  isarchi2  33627  elrgspnlem2  33685  ismntop  34538  coinfliprv  34996  ballotlem2  35002  ballotlemi1  35016  oddprm2  35165  bnj168  35242  bnj153  35391  bnj605  35418  bnj607  35427  bnj986  35466  bnj1090  35490  bnj1128  35501  fineqvrep  35642  axregszf  35657  axregs  35667  fmlasucdisj  35980  dfso2  36336  19.12b  36380  dfom5b  36491  elfuns  36494  dfint3  36533  hfext  36765  nmulprop  36772  trer  36937  bj-alcomexcom  37413  wl-3xornot1  38236  wl-df3maxtru1  38248  cnambfre  38419  itg2addnclem2  38423  itg2addnc  38425  heiborlem1  38563  inxpxrn  39168  eldisjdmqsim  39567  lssat  39891  islshpat  39892  lcvnbtwn2  39902  pclfinclN  40825  lhpex2leN  40888  diclspsn  42069  dihmeetlem4preN  42181  dihmeetlem13N  42194  lcdlss  42494  mapd1o  42523  eq0rabdioph  43623  rmspecnonsq  43750  rmxdioph  43859  wopprc  43873  islssfg2  43914  ifpan23  44302  ifpid1g  44336  minregex  44376  dfrtrcl5  44471  dfhe3  44617  ntrneikb  44936  2sbc6g  45241  2sbc5g  45242  iotasbc2  45246  2sb5nd  45385  2sb5ndVD  45734  2sb5ndALT  45756  ssclaxsep  45807  permac8prim  45839  limsupre2lem  46554  2rexsb  47991  2rexrsb  47992  usgrexmpl2nb2  48951  usgrexmpl2nb5  48954  usgrexmpl2trifr  48955  islindeps  49385  io1ii  49849