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  648  anandi  677  anandir  678  orordi  929  orordir  930  ianor  984  trunantru  1583  falnanfal  1586  had0  1606  nic-axALT  1676  equsexvw  2007  sbiedvw  2101  sbievw2  2104  cbvsbv  2106  sbal  2175  sbco4OLD  2181  sb6a  2266  sbiedw  2322  sbied  2508  sbidm  2515  mo  2566  2mosOLD  2651  2eu6  2658  cbvab  2809  nabbib  3036  rexcom4a  3268  abv  3454  ceqsex  3491  ceqsexv  3492  spc2ed  3557  clel2g  3615  2reuswap  3706  2reuswap2  3707  2reu5  3718  2rmoswap  3721  nfcdeq  3737  sbcid  3759  sbcco2  3769  sbc7  3774  sbcie2g  3783  eqsbc1  3789  sbcralt  3824  cbvralcsf  3893  cbvrabcsf  3896  abss  4016  ssab  4017  raldifb  4103  difrab  4272  euelss  4286  sbccsb  4390  vdif0  4423  difrab0eq  4424  ssunsn2  4785  sspr  4793  sstp  4794  uniintsn  4942  brab1  5148  unopab  5180  axrep5  5234  axrep6OLD  5236  intexab  5293  reusv2lem4  5348  reusv2  5350  el  5394  wefrc  5626  eliunxp  5794  ralxp  5798  rexxp  5799  opelco  5828  reldm0  5885  resieq  5957  iss  6002  imai  6041  intasym  6080  asymref  6081  codir  6085  poirr2  6089  xpdifid  6134  rninxp  6145  dfpo2  6262  frpoins2fg  6310  ordelord  6347  ordtri3  6361  funopg  6534  fin  6722  f1cnvcnv  6747  funimass4  6906  fnressn  7113  resoprab  7486  mpo2eqb  7500  elrnmpores  7506  ov6g  7532  imaeqexov  7606  imaeqalov  7607  offval  7641  uniuni  7717  dfwe2  7729  orduniorsuc  7782  tfinds2  7816  dfopab2  8006  dfoprab3s  8007  fmpox  8021  fparlem1  8064  fparlem2  8065  ralxp3f  8089  frpoins3xpg  8092  brtpos0  8185  dftpos3  8196  tpostpos  8198  dfrecs3  8314  tz7.48lem  8382  omeu  8522  ercnv  8667  ixp0  8881  xpcomco  9007  xpassen  9011  php  9143  findcard3  9195  ixpfi2  9262  dfsup2  9359  sup0riota  9381  card2on  9471  infeq5i  9557  cnfcom3lem  9624  ssttrcl  9636  ttrcltr  9637  ttrclss  9641  setinds2f  9671  frins2f  9677  r1elss  9730  rankxplim  9803  scott0s  9812  aceq1  10039  dfac5lem1  10045  dfac5lem2  10046  kmlem3  10075  kmlem8  10080  kmlem16  10088  djuinf  10111  cflemOLD  10168  cf0  10173  alephval2  10495  fpwwe2lem7  10560  fpwwe2lem11  10564  rankcf  10700  r1tskina  10705  wfgru  10739  genpass  10932  psslinpr  10954  ltpsrpr  11032  addeq0  11572  infm3  12113  nnwos  12840  ioo0  13298  ico0  13319  ioc0  13320  icc0  13321  elfz2nn0  13546  elfzmlbp  13567  sqeqori  14149  hashgt12el  14357  hashgt12el2  14358  cshwidxmod  14738  clim0  15441  divalglem6  16337  ncoprmlnprm  16667  pceu  16786  prmreclem2  16857  cshwshash  17044  xpscf  17498  acsfn2  17598  invsym2  17699  cat1  18033  pospo  18278  issubmndb  18742  f1omvdco3  19390  psgnunilem5  19435  efgrelexlemb  19691  gexex  19794  srgrmhm  20169  isdomn3  20660  isdomn4r  20664  lssne0  20914  islindf4  21805  opsrtoslem1  22022  opsrtoslem2  22023  mdetunilem8  22575  cpmatmcllem  22674  pmatcollpw2lem  22733  ntreq0  23033  ordtrest2lem  23159  ist0-3  23301  ist1-2  23303  ist1-3  23305  cmpfi  23364  2ndcctbss  23411  ptbasfi  23537  ptcnplem  23577  hausdiag  23601  hauseqlcld  23602  cnmptcom  23634  txflf  23962  tgphaus  24073  metrest  24480  iccpnfcnv  24910  bcth3  25299  dyadmax  25567  vitalilem2  25578  vitalilem3  25579  mbfimaopnlem  25624  itg2leub  25703  dvres2  25881  ellogdm  26616  reasinsin  26874  leibpilem2  26919  ftalem3  27053  dchreq  27237  bdayimaon  27673  noetainflem4  27720  cuteq1  27825  addsprop  27984  leadds1  27997  negsprop  28043  mulsprop  28138  mulsuniflem  28157  addsdilem1  28159  addsdilem2  28160  mulsasslem1  28171  mulsasslem2  28172  precsexlem10  28224  precsexlem11  28225  onnolt  28274  bdayn0p1  28377  legso  28683  outpasch  28839  axcontlem2  29050  incistruhgr  29164  nbgrel  29425  usgr2pth0  29850  rusgrnumwwlkslem  30057  frgr3v  30362  4cycl2vnunb  30377  frgrncvvdeqlem2  30387  lnon0  30885  spansncvi  31739  pjssmii  31768  nmlnopgt0i  32084  largei  32354  cvexchlem  32455  xfree  32531  nmo  32575  reuxfrdf  32576  fpwrelmapffslem  32821  eliccioo  33022  1arithidom  33629  ufdprmidl  33633  qtophaus  34013  ordtrest2NEWlem  34099  ordtconnlem1  34101  xrge0iifcnv  34110  xrge0iifiso  34112  xrge0iifhom  34114  cntnevol  34405  eulerpartlemgh  34555  ballotlem7  34713  signswch  34738  bnj446  34893  bnj563  34919  bnj110  35033  bnj153  35055  bnj864  35097  bnj865  35098  bnj849  35100  bnj929  35111  bnj1110  35157  fineqvac  35291  axregs  35314  cusgr3cyclex  35349  derang0  35382  iccllysconn  35463  cvmsss2  35487  satf0op  35590  elmrsubrn  35733  rexxfr3dALT  35852  quad3  35883  axacprim  35920  dftr6  35964  elintfv  35978  opelco3  35988  elima4  35989  elpotr  35992  wzel  36035  elfuns  36126  dfiota3  36134  brimg  36148  imagesset  36166  lineunray  36360  ellines  36365  hfninf  36399  in-ax8  36437  ss-ax8  36438  bj-elabtru  37113  bj-snglc  37208  bj-mpomptALT  37363  bj-elid7  37415  bj-imdirco  37434  nlpineqsn  37652  curf  37838  tan2h  37852  poimirlem26  37886  poimirlem27  37887  poimirlem30  37890  poimirlem32  37892  poimir  37893  ovoliunnfl  37902  voliunnfl  37904  ftc1anc  37941  inixp  37968  heibor1lem  38049  csbcom2fi  38368  tsna1  38384  anan  38475  brid  38552  ref5  38559  idinxpssinxp4  38566  iss2  38584  raldmqseu  38605  xrninxp  38655  cossssid3  38799  dmqs1cosscnvepreseq  38987  disjxrnres5  39087  dmqsblocks  39207  islshpat  39382  lkr0f  39459  lshpsmreu  39474  cvrnbtwn4  39644  ishlat2  39718  islvol5  39944  tendoeq2  41139  dibelval3  41512  mapdpglem3  42040  hdmapglem7a  42292  4rexfrabdioph  43144  dford4  43375  fgraphopab  43549  onsupmaxb  43585  tfsconcatlem  43682  ifpim123g  43845  ifpbibib  43855  rp-isfinite6  43863  elrncard  43882  undmrnresiss  43949  cnvssco  43951  iunrelexpuztr  44064  dffrege115  44323  brco2f1o  44377  ntrneiiso  44436  ismnuprim  44639  undisjrab  44651  radcnvrat  44659  opelopab4  44896  2sb5nd  44905  un2122  45134  uunT12p4  45147  2sb5ndVD  45254  2sb5ndALT  45276  ndisj2  45400  ssabf  45448  abssf  45460  fourierdlem42  46496  smflimlem4  47121  aiotaexaiotaiota  47443  ndmaovcom  47554  dmafv2rnb  47578  afv2ndeffv0  47609  modm1p1ne  47719  0nelsetpreimafv  47739  usgrexmpl2nb0  48380  usgrexmpl2nb1  48381  gpg5nbgrvtx03starlem1  48417  gpg5nbgrvtx03starlem2  48418  gpg5nbgrvtx03starlem3  48419  gpg5nbgrvtx13starlem1  48420  gpg5nbgrvtx13starlem2  48421  gpg5nbgrvtx13starlem3  48422  pgnbgreunbgrlem2lem2  48464  gpg5edgnedg  48479  eliunxp2  48683  pgrpgt2nabl  48715  islindeps  48802  lindslinindsimp1  48806  lindslinindsimp2  48812