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  3442  ceqsex  3478  ceqsexv  3479  spc2ed  3544  clel2g  3602  2reuswap  3693  2reuswap2  3694  2reu5  3705  2rmoswap  3708  nfcdeq  3724  sbcid  3746  sbcco2  3756  sbc7  3761  sbcie2g  3770  eqsbc1  3776  sbcralt  3811  cbvralcsf  3880  cbvrabcsf  3883  abss  4003  ssab  4004  raldifb  4090  difrab  4259  euelss  4273  sbccsb  4377  vdif0  4410  difrab0eq  4411  ssunsn2  4771  sspr  4779  sstp  4780  uniintsn  4928  brab1  5134  unopab  5166  axrep5  5221  axrep6OLD  5223  intexab  5288  reusv2lem4  5344  reusv2  5346  elOLD  5392  wefrc  5625  eliunxp  5793  ralxp  5797  rexxp  5798  opelco  5827  reldm0  5884  resieq  5956  iss  6001  imai  6040  intasym  6079  asymref  6080  codir  6084  poirr2  6088  xpdifid  6133  rninxp  6144  dfpo2  6261  frpoins2fg  6309  ordelord  6346  ordtri3  6360  funopg  6533  fin  6721  f1cnvcnv  6746  funimass4  6905  fnressn  7112  resoprab  7485  mpo2eqb  7499  elrnmpores  7505  ov6g  7531  imaeqexov  7605  imaeqalov  7606  offval  7640  uniuni  7716  dfwe2  7728  orduniorsuc  7781  tfinds2  7815  dfopab2  8005  dfoprab3s  8006  fmpox  8020  fparlem1  8062  fparlem2  8063  ralxp3f  8087  frpoins3xpg  8090  brtpos0  8183  dftpos3  8194  tpostpos  8196  dfrecs3  8312  tz7.48lem  8380  omeu  8520  ercnv  8665  ixp0  8879  xpcomco  9005  xpassen  9009  php  9141  findcard3  9193  ixpfi2  9260  dfsup2  9357  sup0riota  9379  card2on  9469  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  11573  infm3  12115  nnwos  12865  ioo0  13323  ico0  13344  ioc0  13345  icc0  13346  elfz2nn0  13572  elfzmlbp  13593  sqeqori  14176  hashgt12el  14384  hashgt12el2  14385  cshwidxmod  14765  clim0  15468  divalglem6  16367  ncoprmlnprm  16698  pceu  16817  prmreclem2  16888  cshwshash  17075  xpscf  17529  acsfn2  17629  invsym2  17730  cat1  18064  pospo  18309  issubmndb  18773  f1omvdco3  19424  psgnunilem5  19469  efgrelexlemb  19725  gexex  19828  srgrmhm  20203  isdomn3  20692  isdomn4r  20696  lssne0  20946  islindf4  21818  opsrtoslem1  22033  opsrtoslem2  22034  mdetunilem8  22584  cpmatmcllem  22683  pmatcollpw2lem  22742  ntreq0  23042  ordtrest2lem  23168  ist0-3  23310  ist1-2  23312  ist1-3  23314  cmpfi  23373  2ndcctbss  23420  ptbasfi  23546  ptcnplem  23586  hausdiag  23610  hauseqlcld  23611  cnmptcom  23643  txflf  23971  tgphaus  24082  metrest  24489  iccpnfcnv  24911  bcth3  25298  dyadmax  25565  vitalilem2  25576  vitalilem3  25577  mbfimaopnlem  25622  itg2leub  25701  dvres2  25879  ellogdm  26603  reasinsin  26860  leibpilem2  26905  ftalem3  27038  dchreq  27221  bdayimaon  27657  noetainflem4  27704  cuteq1  27809  addsprop  27968  leadds1  27981  negsprop  28027  mulsprop  28122  mulsuniflem  28141  addsdilem1  28143  addsdilem2  28144  mulsasslem1  28155  mulsasslem2  28156  precsexlem10  28208  precsexlem11  28209  onnolt  28258  bdayn0p1  28361  legso  28667  outpasch  28823  axcontlem2  29034  incistruhgr  29148  nbgrel  29409  usgr2pth0  29833  rusgrnumwwlkslem  30040  frgr3v  30345  4cycl2vnunb  30360  frgrncvvdeqlem2  30370  lnon0  30869  spansncvi  31723  pjssmii  31752  nmlnopgt0i  32068  largei  32338  cvexchlem  32439  xfree  32515  nmo  32559  reuxfrdf  32560  fpwrelmapffslem  32805  eliccioo  32990  1arithidom  33597  ufdprmidl  33601  qtophaus  33980  ordtrest2NEWlem  34066  ordtconnlem1  34068  xrge0iifcnv  34077  xrge0iifiso  34079  xrge0iifhom  34081  cntnevol  34372  eulerpartlemgh  34522  ballotlem7  34680  signswch  34705  bnj446  34860  bnj563  34886  bnj110  35000  bnj153  35022  bnj864  35064  bnj865  35065  bnj849  35067  bnj929  35078  bnj1110  35124  fineqvac  35260  axregs  35283  cusgr3cyclex  35318  derang0  35351  iccllysconn  35432  cvmsss2  35456  satf0op  35559  elmrsubrn  35702  rexxfr3dALT  35821  quad3  35852  axacprim  35889  dftr6  35933  elintfv  35947  opelco3  35957  elima4  35958  elpotr  35961  wzel  36004  elfuns  36095  dfiota3  36103  brimg  36117  imagesset  36135  lineunray  36329  ellines  36334  hfninf  36368  in-ax8  36406  ss-ax8  36407  bj-df-sb  36944  bj-elabtru  37181  bj-snglc  37276  bj-mpomptALT  37431  bj-elid7  37485  bj-imdirco  37504  nlpineqsn  37724  curf  37919  tan2h  37933  poimirlem26  37967  poimirlem27  37968  poimirlem30  37971  poimirlem32  37973  poimir  37974  ovoliunnfl  37983  voliunnfl  37985  ftc1anc  38022  inixp  38049  heibor1lem  38130  csbcom2fi  38449  tsna1  38465  anan  38556  brid  38633  ref5  38640  idinxpssinxp4  38647  iss2  38665  raldmqseu  38686  xrninxp  38736  cossssid3  38880  dmqs1cosscnvepreseq  39068  disjxrnres5  39168  dmqsblocks  39288  islshpat  39463  lkr0f  39540  lshpsmreu  39555  cvrnbtwn4  39725  ishlat2  39799  islvol5  40025  tendoeq2  41220  dibelval3  41593  mapdpglem3  42121  hdmapglem7a  42373  4rexfrabdioph  43226  dford4  43457  fgraphopab  43631  onsupmaxb  43667  tfsconcatlem  43764  ifpim123g  43927  ifpbibib  43937  rp-isfinite6  43945  elrncard  43964  undmrnresiss  44031  cnvssco  44033  iunrelexpuztr  44146  dffrege115  44405  brco2f1o  44459  ntrneiiso  44518  ismnuprim  44721  undisjrab  44733  radcnvrat  44741  opelopab4  44978  2sb5nd  44987  un2122  45216  uunT12p4  45229  2sb5ndVD  45336  2sb5ndALT  45358  ndisj2  45482  ssabf  45530  abssf  45542  fourierdlem42  46577  smflimlem4  47202  aiotaexaiotaiota  47536  ndmaovcom  47647  dmafv2rnb  47671  afv2ndeffv0  47702  modm1p1ne  47818  0nelsetpreimafv  47844  usgrexmpl2nb0  48501  usgrexmpl2nb1  48502  gpg5nbgrvtx03starlem1  48538  gpg5nbgrvtx03starlem2  48539  gpg5nbgrvtx03starlem3  48540  gpg5nbgrvtx13starlem1  48541  gpg5nbgrvtx13starlem2  48542  gpg5nbgrvtx13starlem3  48543  pgnbgreunbgrlem2lem2  48585  gpg5edgnedg  48600  eliunxp2  48804  pgrpgt2nabl  48836  islindeps  48923  lindslinindsimp1  48927  lindslinindsimp2  48933