Theorem bitr3i 277

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 224	. 2 ⊢ (𝜑 ↔ 𝜓)
3		bitr3i.2	. 2 ⊢ (𝜓 ↔ 𝜒)
4	2, 3	bitri 275	1 ⊢ (𝜑 ↔ 𝜒)

Syntax hints:   ↔ wb 206

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 207

This theorem is referenced by:  3bitrri  298  3bitr3i  301  3bitr3ri  302  xchnxbi  332  an13  647  anandi  676  anandir  677  orordi  928  orordir  929  ianor  983  trunantru  1581  falnanfal  1584  had0  1604  nic-axALT  1674  equsexvw  2005  sbiedvw  2096  sbievw2  2099  cbvsbv  2101  sbal  2170  sbco4OLD  2176  sb6a  2259  sbiedw  2315  sbied  2502  sbidm  2509  mo  2559  2mosOLD  2644  2eu6  2651  cbvab  2802  nabbib  3029  rexcom4a  3269  abv  3462  ceqsex  3499  ceqsexv  3501  spc2ed  3570  clel2g  3628  2reuswap  3720  2reuswap2  3721  2reu5  3732  2rmoswap  3735  nfcdeq  3751  sbcid  3773  sbcco2  3783  sbc7  3788  sbcie2g  3797  eqsbc1  3803  sbcralt  3838  cbvralcsf  3907  cbvrabcsf  3910  abss  4029  ssab  4030  raldifb  4115  difrab  4284  euelss  4298  vn0  4311  sbccsb  4402  vdif0  4435  difrab0eq  4436  ssunsn2  4794  sspr  4802  sstp  4803  uniintsn  4952  brab1  5158  unopab  5190  axrep5  5245  axrep6OLD  5247  intexab  5304  reusv2lem4  5359  reusv2  5361  el  5400  wefrc  5635  eliunxp  5804  ralxp  5808  rexxp  5809  opelco  5838  reldm0  5894  resieq  5964  iss  6009  imai  6048  cnvsymOLDOLD  6090  intasym  6091  asymref  6092  codir  6096  poirr2  6100  xpdifid  6144  rninxp  6155  dfpo2  6272  frpoins2fg  6320  ordelord  6357  ordtri3  6371  dffun3OLD  6529  funopg  6553  fin  6743  f1cnvcnv  6768  funimass4  6928  fnressn  7133  resoprab  7510  mpo2eqb  7524  elrnmpores  7530  ov6g  7556  imaeqexov  7630  imaeqalov  7631  offval  7665  uniuni  7741  dfwe2  7753  orduniorsuc  7808  tfinds2  7843  dfopab2  8034  dfoprab3s  8035  fmpox  8049  fparlem1  8094  fparlem2  8095  ralxp3f  8119  frpoins3xpg  8122  brtpos0  8215  dftpos3  8226  tpostpos  8228  dfrecs3  8344  tz7.48lem  8412  omeu  8552  ercnv  8695  ixp0  8907  xpcomco  9036  xpassen  9040  php  9177  findcard3  9236  findcard3OLD  9237  ixpfi2  9308  dfsup2  9402  sup0riota  9424  card2on  9514  infeq5i  9596  cnfcom3lem  9663  ssttrcl  9675  ttrcltr  9676  ttrclss  9680  frins2f  9713  r1elss  9766  rankxplim  9839  scott0s  9848  aceq1  10077  dfac5lem1  10083  dfac5lem2  10084  kmlem3  10113  kmlem8  10118  kmlem16  10126  djuinf  10149  cflemOLD  10206  cf0  10211  alephval2  10532  fpwwe2lem7  10597  fpwwe2lem11  10601  rankcf  10737  r1tskina  10742  wfgru  10776  genpass  10969  psslinpr  10991  ltpsrpr  11069  addeq0  11608  infm3  12149  nnwos  12881  ioo0  13338  ico0  13359  ioc0  13360  icc0  13361  elfz2nn0  13586  elfzmlbp  13607  sqeqori  14186  hashgt12el  14394  hashgt12el2  14395  cshwidxmod  14775  clim0  15479  divalglem6  16375  ncoprmlnprm  16705  pceu  16824  prmreclem2  16895  cshwshash  17082  xpscf  17535  acsfn2  17631  invsym2  17732  cat1  18066  pospo  18311  issubmndb  18739  f1omvdco3  19386  psgnunilem5  19431  efgrelexlemb  19687  gexex  19790  srgrmhm  20138  isdomn3  20631  isdomn4r  20635  lssne0  20864  islindf4  21754  opsrtoslem1  21969  opsrtoslem2  21970  mdetunilem8  22513  cpmatmcllem  22612  pmatcollpw2lem  22671  ntreq0  22971  ordtrest2lem  23097  ist0-3  23239  ist1-2  23241  ist1-3  23243  cmpfi  23302  2ndcctbss  23349  ptbasfi  23475  ptcnplem  23515  hausdiag  23539  hauseqlcld  23540  cnmptcom  23572  txflf  23900  tgphaus  24011  metrest  24419  iccpnfcnv  24849  bcth3  25238  dyadmax  25506  vitalilem2  25517  vitalilem3  25518  mbfimaopnlem  25563  itg2leub  25642  dvres2  25820  ellogdm  26555  reasinsin  26813  leibpilem2  26858  ftalem3  26992  dchreq  27176  bdayimaon  27612  noetainflem4  27659  cuteq1  27753  addsprop  27890  sleadd1  27903  negsprop  27948  mulsprop  28040  mulsuniflem  28059  addsdilem1  28061  addsdilem2  28062  mulsasslem1  28073  mulsasslem2  28074  precsexlem10  28125  precsexlem11  28126  onnolt  28174  bdayn0p1  28265  legso  28533  outpasch  28689  axcontlem2  28899  incistruhgr  29013  nbgrel  29274  usgr2pth0  29702  rusgrnumwwlkslem  29906  frgr3v  30211  4cycl2vnunb  30226  frgrncvvdeqlem2  30236  lnon0  30734  spansncvi  31588  pjssmii  31617  nmlnopgt0i  31933  largei  32203  cvexchlem  32304  xfree  32380  nmo  32426  reuxfrdf  32427  fpwrelmapffslem  32662  eliccioo  32858  1arithidom  33515  ufdprmidl  33519  qtophaus  33833  ordtrest2NEWlem  33919  ordtconnlem1  33921  xrge0iifcnv  33930  xrge0iifiso  33932  xrge0iifhom  33934  cntnevol  34225  eulerpartlemgh  34376  ballotlem7  34534  signswch  34559  bnj446  34714  bnj563  34740  bnj110  34855  bnj153  34877  bnj864  34919  bnj865  34920  bnj849  34922  bnj929  34933  bnj1110  34979  fineqvac  35094  cusgr3cyclex  35130  derang0  35163  iccllysconn  35244  cvmsss2  35268  satf0op  35371  elmrsubrn  35514  rexxfr3dALT  35633  quad3  35664  axacprim  35701  dftr6  35745  elintfv  35759  opelco3  35769  elima4  35770  setinds2f  35774  elpotr  35776  wzel  35819  elfuns  35910  dfiota3  35918  brimg  35932  imagesset  35948  lineunray  36142  ellines  36147  hfninf  36181  in-ax8  36219  ss-ax8  36220  bj-elabtru  36869  bj-snglc  36964  bj-mpomptALT  37114  bj-elid7  37166  bj-imdirco  37185  nlpineqsn  37403  curf  37599  tan2h  37613  poimirlem26  37647  poimirlem27  37648  poimirlem30  37651  poimirlem32  37653  poimir  37654  ovoliunnfl  37663  voliunnfl  37665  ftc1anc  37702  inixp  37729  heibor1lem  37810  csbcom2fi  38129  tsna1  38145  anan  38224  brid  38301  ref5  38308  idinxpssinxp4  38315  iss2  38333  xrninxp  38385  cossssid3  38467  dmqs1cosscnvepreseq  38661  disjxrnres5  38746  dmqsblocks  38852  islshpat  39017  lkr0f  39094  lshpsmreu  39109  cvrnbtwn4  39279  ishlat2  39353  islvol5  39580  tendoeq2  40775  dibelval3  41148  mapdpglem3  41676  hdmapglem7a  41928  4rexfrabdioph  42793  dford4  43025  fgraphopab  43199  onsupmaxb  43235  tfsconcatlem  43332  ifpim123g  43496  ifpbibib  43506  rp-isfinite6  43514  elrncard  43533  undmrnresiss  43600  cnvssco  43602  iunrelexpuztr  43715  dffrege115  43974  brco2f1o  44028  ntrneiiso  44087  ismnuprim  44290  undisjrab  44302  radcnvrat  44310  opelopab4  44548  2sb5nd  44557  un2122  44786  uunT12p4  44799  2sb5ndVD  44906  2sb5ndALT  44928  ndisj2  45052  ssabf  45101  abssf  45113  fourierdlem42  46154  smflimlem4  46779  aiotaexaiotaiota  47099  ndmaovcom  47210  dmafv2rnb  47234  afv2ndeffv0  47265  modm1p1ne  47375  0nelsetpreimafv  47395  usgrexmpl2nb0  48026  usgrexmpl2nb1  48027  gpg5nbgrvtx03starlem1  48063  gpg5nbgrvtx03starlem2  48064  gpg5nbgrvtx03starlem3  48065  gpg5nbgrvtx13starlem1  48066  gpg5nbgrvtx13starlem2  48067  gpg5nbgrvtx13starlem3  48068  pgnbgreunbgrlem2lem2  48109  eliunxp2  48326  pgrpgt2nabl  48358  islindeps  48446  lindslinindsimp1  48450  lindslinindsimp2  48456