Theorem bitr3i 280

Description: An inference from transitive law for logical equivalence. (Contributed by NM, 2-Jun-1993.)

Hypotheses

Ref	Expression
bitr3i.1	⊢ (𝜓 ↔ 𝜑)
bitr3i.2	⊢ (𝜓 ↔ 𝜒)

Assertion

Ref	Expression
bitr3i	⊢ (𝜑 ↔ 𝜒)

Proof of Theorem bitr3i

Step	Hyp	Ref	Expression
1		bitr3i.1	. . 3 ⊢ (𝜓 ↔ 𝜑)
2	1	bicomi 227	. 2 ⊢ (𝜑 ↔ 𝜓)
3		bitr3i.2	. 2 ⊢ (𝜓 ↔ 𝜒)
4	2, 3	bitri 278	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  3bitr3i  304  3bitr3ri  305  xchnxbi  335  an13  647  anandi  676  anandir  677  orordi  929  orordir  930  ianor  982  trunantru  1584  falnanfal  1587  had0  1611  nic-axALT  1682  equsexvw  2013  sbiedvw  2100  sbievw2  2103  sbal  2163  sb6a  2255  sb56OLD  2274  sbco4  2279  sbiedw  2314  sbiedwOLD  2315  sbied  2506  sbidm  2513  mo  2564  2mos  2650  2eu6  2657  cbvabv  2811  cbvabwOLD  2813  cbvab  2814  nabbi  3044  rexcom4a  3174  r19.41v  3260  r19.41  3261  2ralor  3281  abv  3419  spc2ed  3516  clel2g  3566  2reuswap  3659  2reuswap2  3660  2reu5  3671  2rmoswap  3674  nfcdeq  3690  sbcid  3711  sbcco2  3721  sbc7  3727  sbcie2g  3736  eqsbc3  3743  sbcralt  3784  cbvralcsf  3856  cbvrabcsf  3859  abss  3974  ssab  3975  raldifb  4059  difrab  4223  euelss  4236  vn0  4253  sbccsb  4348  vdif0  4383  difrab0eq  4384  ssunsn2  4740  sspr  4746  sstp  4747  uniintsn  4898  brab1  5101  unopab  5134  axrep5  5185  axrep6  5186  intexab  5232  reusv2lem4  5294  reusv2  5296  wefrc  5545  eliunxp  5706  ralxp  5710  rexxp  5711  opelco  5740  reldm0  5797  resieq  5862  iss  5903  imai  5942  cnvsym  5979  intasym  5980  asymref  5981  codir  5985  poirr2  5989  xpdifid  6031  rninxp  6042  frpoins2fg  6198  tz6.26  6201  wfis2fg  6207  ordelord  6235  ordtri3  6249  dffun3  6391  funopg  6414  fin  6599  f1cnvcnv  6625  funimass4  6777  fnressn  6973  resoprab  7328  mpo2eqb  7342  elrnmpores  7347  ov6g  7372  offval  7477  uniuni  7547  dfwe2  7559  orduniorsuc  7609  tfinds2  7642  dfopab2  7822  dfoprab3s  7823  fmpox  7837  fparlem1  7880  fparlem2  7881  brtpos0  7975  dftpos3  7986  tpostpos  7988  dfrecs3  8109  tz7.48lem  8177  omeu  8313  ercnv  8412  ixp0  8612  xpcomco  8735  xpassen  8739  php  8830  findcard3  8914  ixpfi2  8974  dfsup2  9060  sup0riota  9081  card2on  9170  infeq5i  9251  cnfcom3lem  9318  frins2f  9369  r1elss  9422  rankxplim  9495  scott0s  9504  aceq1  9731  dfac5lem1  9737  dfac5lem2  9738  kmlem3  9766  kmlem8  9771  kmlem16  9779  djuinf  9802  cflem  9860  cf0  9865  alephval2  10186  fpwwe2lem7  10251  fpwwe2lem11  10255  rankcf  10391  r1tskina  10396  wfgru  10430  genpass  10623  psslinpr  10645  ltpsrpr  10723  addeq0  11255  infm3  11791  nnwos  12511  ioo0  12960  ico0  12981  ioc0  12982  icc0  12983  elfz2nn0  13203  elfzmlbp  13223  sqeqori  13782  hashgt12el  13989  hashgt12el2  13990  cshwidxmod  14368  clim0  15067  divalglem6  15959  ncoprmlnprm  16284  pceu  16399  prmreclem2  16470  cshwshash  16658  xpscf  17070  acsfn2  17166  invsym2  17268  cat1  17603  pospo  17851  issubmndb  18232  f1omvdco3  18841  psgnunilem5  18886  efgrelexlemb  19140  gexex  19238  srgrmhm  19551  lssne0  19987  islindf4  20800  opsrtoslem1  21012  opsrtoslem2  21013  mdetunilem8  21516  cpmatmcllem  21615  pmatcollpw2lem  21674  ntreq0  21974  ordtrest2lem  22100  ist0-3  22242  ist1-2  22244  ist1-3  22246  cmpfi  22305  2ndcctbss  22352  ptbasfi  22478  ptcnplem  22518  hausdiag  22542  hauseqlcld  22543  cnmptcom  22575  txflf  22903  tgphaus  23014  metrest  23422  iccpnfcnv  23841  bcth3  24228  dyadmax  24495  vitalilem2  24506  vitalilem3  24507  mbfimaopnlem  24552  itg2leub  24632  dvres2  24809  ellogdm  25527  reasinsin  25779  leibpilem2  25824  ftalem3  25957  dchreq  26139  legso  26690  outpasch  26846  axcontlem2  27056  incistruhgr  27170  nbgrel  27428  usgr2pth0  27852  rusgrnumwwlkslem  28053  frgr3v  28358  4cycl2vnunb  28373  frgrncvvdeqlem2  28383  lnon0  28879  spansncvi  29733  pjssmii  29762  nmlnopgt0i  30078  largei  30348  cvexchlem  30449  xfree  30525  nmo  30557  reuxfrdf  30558  fpwrelmapffslem  30787  eliccioo  30925  qtophaus  31500  ordtrest2NEWlem  31586  ordtconnlem1  31588  xrge0iifcnv  31597  xrge0iifiso  31599  xrge0iifhom  31601  cntnevol  31908  eulerpartlemgh  32057  ballotlem7  32214  signswch  32252  bnj446  32408  bnj563  32435  bnj110  32551  bnj153  32573  bnj864  32615  bnj865  32616  bnj849  32618  bnj929  32629  bnj1110  32675  fineqvac  32779  cusgr3cyclex  32811  derang0  32844  iccllysconn  32925  cvmsss2  32949  satf0op  33052  elmrsubrn  33195  quad3  33341  axacprim  33361  ralxp3f  33401  dftr6  33436  dfpo2  33441  elintfv  33457  opelco3  33468  elima4  33469  setinds2f  33474  elpotr  33476  ssttrcl  33514  ttrcltr  33515  ttrclss  33519  frpoins3xpg  33524  frpoins3xp3g  33525  xpord3pred  33535  wzel  33555  bdayimaon  33633  noetainflem4  33680  elfuns  33954  dfiota3  33962  brimg  33976  imagesset  33992  lineunray  34186  ellines  34191  hfninf  34225  bj-elabtru  34795  bj-snglc  34896  bj-mpomptALT  35025  bj-elid7  35077  bj-imdirco  35096  bj-isrvec  35199  nlpineqsn  35316  curf  35492  tan2h  35506  poimirlem26  35540  poimirlem27  35541  poimirlem30  35544  poimirlem32  35546  poimir  35547  ovoliunnfl  35556  voliunnfl  35558  ftc1anc  35595  inixp  35623  heibor1lem  35704  csbcom2fi  36023  tsna1  36039  anan  36116  brid  36179  idinxpssinxp4  36192  iss2  36216  xrninxp  36255  cossssid3  36324  dmqs1cosscnvepreseq  36511  islshpat  36768  lkr0f  36845  lshpsmreu  36860  cvrnbtwn4  37030  ishlat2  37104  islvol5  37330  tendoeq2  38525  dibelval3  38898  mapdpglem3  39426  hdmapglem7a  39678  4rexfrabdioph  40323  dford4  40554  isdomn3  40732  fgraphopab  40738  ifpim123g  40792  ifpbibib  40802  rp-isfinite6  40810  elrncard  40827  undmrnresiss  40888  cnvssco  40890  iunrelexpuztr  41004  dffrege115  41263  brco2f1o  41319  ntrneiiso  41378  ismnuprim  41585  undisjrab  41597  radcnvrat  41605  opelopab4  41844  2sb5nd  41853  un2122  42083  uunT12p4  42096  2sb5ndVD  42203  2sb5ndALT  42225  ndisj2  42272  ssabf  42323  abssf  42335  fourierdlem42  43365  smflimlem4  43981  aiotaexaiotaiota  44258  ndmaovcom  44369  dmafv2rnb  44393  afv2ndeffv0  44424  0nelsetpreimafv  44515  eliunxp2  45342  pgrpgt2nabl  45375  islindeps  45467  lindslinindsimp1  45471  lindslinindsimp2  45477