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  1527  nannot  1528  empty  1938  19.12vvv  2026  19.12vv  2376  cvjust  2754  necon1abii  3003  nrexralim  3146  r19.23v  3189  nelb  3238  cbvralsvw  3313  spc3gv  3558  ralxpxfr2d  3599  sbc8g  3746  csbied  3882  ss2rab  3994  difdif  4071  ddif  4077  dfss2  4094  unass  4170  unss  4188  undi  4230  disj  4402  ssindif0  4416  prneimg  4813  iinrab2  5027  unopab  5184  axrep5  5238  eqvinop  5455  eqvinot  5456  pwssun  5542  dmun  5891  reldm0  5909  dmres  6002  imadmrnOLD  6067  ssrnres  6169  dmsnn0  6208  coundi  6248  coundir  6249  resco  6251  cnvpo  6290  xpco  6292  dfpo2  6299  fun11  6614  fununi  6615  fdmrn  6741  dffv2  6980  fsn  7136  eufnfv  7235  eloprabga  7529  funoprabg  7541  ralrnmpo  7559  imaeqexov  7659  tfinds2  7875  funcnvuni  7944  oprabrexex2  7990  ralxp3f  8154  soseq  8176  dfer2  8719  euen1b  9056  xpsnen  9081  wemapsolem  9545  zfregcl  9589  zfregclOLD  9590  epfrs  9733  rankbnd  9886  rankbnd2  9887  rankxplim2  9898  rankxplim3  9899  scottabf  9940  isinfcard  10172  dfac5lem2  10204  dfac5lem5  10207  kmlem14  10243  kmlem15  10244  kmlem16  10245  axdc2lem  10527  axcclem  10536  ac9  10562  ac9s  10572  nnunb  12603  xrrebnd  13299  elfznelfzo  13909  hashfun  14583  hashtpg  14631  rexuz3  15517  imasaddfnlem  17701  isnsgrp  18913  eqg0subg  19412  dprd2d2  20261  isnirred  20651  subsubrng2  20817  subsubrg2  20852  mdetunilem8  22935  maducoeval2  22956  tgval2  23275  0top  23302  ssntr  23377  uncmp  23722  opnfbas  24162  fbunfip  24189  alexsubALTlem2  24368  alexsubALTlem3  24369  alexsubALT  24371  metrest  24844  cfilucfil3  25642  ellimc3  26200  plyun0  26516  plymulidp  26604  sinhalfpilem  26793  2lgslem4  27734  addsdilem1  28538  addsdilem2  28539  mulsasslem1  28550  mulsasslem2  28551  dfcgra2  29339  colinearalg  29489  axcontlem5  29547  nb3grprlem2  29963  wlkeq  30215  isspthonpth  30336  clwlkclwwlklem2a4  30589  clwwlkn1  30633  clwwlkn2  30636  clwwlknon2x  30695  fusgreg2wsp  30938  h2hlm  31583  shlesb1i  31989  pjneli  32326  cnlnssadj  32683  pjin2i  32796  cvnbtwn2  32890  cvnbtwn4  32892  mdsl1i  32924  mdsl2i  32925  hatomistici  32965  cdj3lem3b  33043  iuninc  33198  disjex  33229  disjexc  33230  fpwrelmapffslem  33367  fpwrelmapffs  33369  mgcval  33591  isarchi2  33789  elrgspnlem2  33847  ismntop  34701  coinfliprv  35158  ballotlem2  35164  ballotlemi1  35178  oddprm2  35327  bnj168  35404  bnj153  35553  bnj605  35580  bnj607  35589  bnj986  35628  bnj1090  35652  bnj1128  35663  fineqvrep  35831  axregszf  35846  axregs  35856  fmlasucdisj  36233  dfso2  36595  19.12b  36638  dfom5b  36749  elfuns  36752  dfint3  36791  hfext  37009  nmulprop  37014  trer  37179  bj-alcomexcom  37655  wl-3xornot1  38479  wl-df3maxtru1  38491  cnambfre  38662  itg2addnclem2  38666  itg2addnc  38668  heiborlem1  38821  inxpxrn  39426  eldisjdmqsim  39825  lssat  40149  islshpat  40150  lcvnbtwn2  40160  pclfinclN  41083  lhpex2leN  41146  diclspsn  42327  dihmeetlem4preN  42439  dihmeetlem13N  42452  lcdlss  42752  mapd1o  42781  eq0rabdioph  43863  rmspecnonsq  43990  rmxdioph  44099  wopprc  44113  islssfg2  44149  ifpan23  44537  ifpid1g  44571  minregex  44611  dfrtrcl5  44705  dfhe3  44851  ntrneikb  45170  2sbc6g  45475  2sbc5g  45476  iotasbc2  45480  2sb5nd  45619  2sb5ndVD  45968  2sb5ndALT  45990  ssclaxsep  46048  permac8prim  46080  limsupre2lem  46810  2rexsb  48247  2rexrsb  48248  usgrexmpl2nb2  49207  usgrexmpl2nb5  49210  usgrexmpl2trifr  49211  islindeps  49641  io1ii  50105