Theorem bitr3i 278

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

Syntax hints:   ↔ wb 207

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 208

This theorem is referenced by:  3bitrri  299  3bitr3i  302  3bitr3ri  303  xchnxbi  333  an13  653  anandi  682  anandir  683  orordi  934  orordir  935  ianor  989  trunantru  1588  falnanfal  1591  had0  1611  nic-axALT  1681  equsexvw  2012  sbiedvw  2106  sbievw2  2109  cbvsbv  2111  sbal  2180  sbco4OLD  2185  sb6a  2270  sbiedw  2325  sbied  2511  sbidm  2518  mo  2569  2mosOLD  2654  2eu6  2661  cbvab  2812  nabbib  3038  rexcom4a  3270  abv  3444  ceqsex  3480  ceqsexv  3481  spc2ed  3546  clel2g  3604  2reuswap  3694  2reuswap2  3695  2reu5  3706  2rmoswap  3709  nfcdeq  3725  sbcid  3747  sbcco2  3757  sbc7  3762  sbcie2g  3770  eqsbc1  3776  sbcralt  3811  cbvralcsf  3880  cbvrabcsf  3883  abss  4000  ssab  4001  raldifb  4086  difrab  4253  euelss  4267  sbccsb  4371  vdif0  4404  difrab0eq  4405  ssunsn2  4765  sspr  4773  sstp  4774  uniintsn  4922  brab1  5127  unopab  5159  axrep5  5214  axrep6OLD  5216  intexab  5281  reusv2lem4  5337  reusv2  5339  elOLD  5385  wefrc  5619  eliunxp  5786  ralxp  5790  rexxp  5791  opelco  5820  reldm0  5877  resieq  5949  iss  5994  imai  6033  intasym  6072  asymref  6073  codir  6077  poirr2  6081  xpdifid  6126  rninxp  6137  dfpo2  6254  frpoins2fg  6302  ordelord  6339  ordtri3  6353  funopg  6526  fin  6714  f1cnvcnv  6739  funimass4  6898  fnressn  7108  resoprab  7481  mpo2eqb  7495  elrnmpores  7501  ov6g  7527  imaeqexov  7601  imaeqalov  7602  offval  7636  uniuni  7712  dfwe2  7724  orduniorsuc  7777  tfinds2  7811  dfopab2  8001  dfoprab3s  8002  fmpox  8016  fparlem1  8058  fparlem2  8059  ralxp3f  8084  frpoins3xpg  8087  brtpos0  8180  dftpos3  8191  tpostpos  8193  dfrecs3  8309  tz7.48lem  8377  omeu  8517  ercnv  8662  ixp0  8876  xpcomco  9002  xpassen  9006  php  9138  findcard3  9190  ixpfi2  9257  dfsup2  9354  sup0riota  9376  card2on  9466  infeq5i  9555  cnfcom3lem  9622  ssttrcl  9634  ttrcltr  9635  ttrclss  9639  setinds2f  9669  frins2f  9675  r1elss  9728  rankxplim  9801  scott0s  9810  aceq1  10037  dfac5lem1  10043  dfac5lem2  10044  kmlem3  10073  kmlem8  10078  kmlem16  10086  djuinf  10109  cflemOLD  10166  cf0  10171  alephval2  10493  fpwwe2lem7  10558  fpwwe2lem11  10562  rankcf  10698  r1tskina  10703  wfgru  10737  genpass  10930  psslinpr  10952  ltpsrpr  11030  addeq0  11571  infm3  12113  nnwos  12863  ioo0  13321  ico0  13342  ioc0  13343  icc0  13344  elfz2nn0  13570  elfzmlbp  13591  sqeqori  14174  hashgt12el  14382  hashgt12el2  14383  cshwidxmod  14763  clim0  15466  divalglem6  16365  ncoprmlnprm  16696  pceu  16815  prmreclem2  16886  cshwshash  17073  xpscf  17527  acsfn2  17627  invsym2  17728  cat1  18062  pospo  18307  issubmndb  18771  f1omvdco3  19422  psgnunilem5  19467  efgrelexlemb  19723  gexex  19826  srgrmhm  20201  isdomn3  20694  isdomn4r  20698  lssne0  20948  islindf4  21820  opsrtoslem1  22038  opsrtoslem2  22039  mdetunilem8  22609  cpmatmcllem  22708  pmatcollpw2lem  22767  ntreq0  23067  ordtrest2lem  23193  ist0-3  23335  ist1-2  23337  ist1-3  23339  cmpfi  23398  2ndcctbss  23445  ptbasfi  23571  ptcnplem  23611  hausdiag  23635  hauseqlcld  23636  cnmptcom  23668  txflf  23996  tgphaus  24107  metrest  24514  iccpnfcnv  24936  bcth3  25323  dyadmax  25590  vitalilem2  25601  vitalilem3  25602  mbfimaopnlem  25647  itg2leub  25726  dvres2  25904  ellogdm  26628  reasinsin  26885  leibpilem2  26930  ftalem3  27063  dchreq  27246  bdayimaon  27682  noetainflem4  27729  cuteq1  27834  addsprop  27993  leadds1  28006  negsprop  28052  mulsprop  28147  mulsuniflem  28166  addsdilem1  28168  addsdilem2  28169  mulsasslem1  28180  mulsasslem2  28181  precsexlem10  28233  precsexlem11  28234  onnolt  28283  bdayn0p1  28386  legso  28692  outpasch  28848  axcontlem2  29059  incistruhgr  29173  nbgrel  29434  usgr2pth0  29858  rusgrnumwwlkslem  30065  frgr3v  30370  4cycl2vnunb  30385  frgrncvvdeqlem2  30395  lnon0  30894  spansncvi  31748  pjssmii  31777  nmlnopgt0i  32093  largei  32363  cvexchlem  32464  xfree  32540  nmo  32584  reuxfrdf  32585  fpwrelmapffslem  32831  eliccioo  33016  1arithidom  33627  ufdprmidl  33631  qtophaus  34027  ordtrest2NEWlem  34113  ordtconnlem1  34115  xrge0iifcnv  34124  xrge0iifiso  34126  xrge0iifhom  34128  cntnevol  34419  eulerpartlemgh  34569  ballotlem7  34727  signswch  34752  bnj446  34907  bnj563  34933  bnj110  35047  bnj153  35069  bnj864  35111  bnj865  35112  bnj849  35114  bnj929  35125  bnj1110  35171  fineqvac  35307  axregs  35330  cusgr3cyclex  35365  derang0  35398  iccllysconn  35479  cvmsss2  35503  satf0op  35606  elmrsubrn  35749  rexxfr3dALT  35868  quad3  35899  axacprim  35936  dftr6  35980  elintfv  35994  opelco3  36004  elima4  36005  elpotr  36008  wzel  36051  elfuns  36142  dfiota3  36150  brimg  36164  imagesset  36182  lineunray  36376  ellines  36381  hfninf  36415  in-ax8  36453  ss-ax8  36454  bj-df-sb  36991  bj-elabtru  37228  bj-snglc  37323  bj-mpomptALT  37478  bj-elid7  37532  bj-imdirco  37551  nlpineqsn  37771  curf  37966  tan2h  37980  poimirlem26  38014  poimirlem27  38015  poimirlem30  38018  poimirlem32  38020  poimir  38021  ovoliunnfl  38030  voliunnfl  38032  ftc1anc  38069  inixp  38096  heibor1lem  38177  csbcom2fi  38496  tsna1  38512  anan  38603  brid  38680  ref5  38687  idinxpssinxp4  38694  iss2  38712  raldmqseu  38733  xrninxp  38783  cossssid3  38927  dmqs1cosscnvepreseq  39115  disjxrnres5  39215  dmqsblocks  39335  islshpat  39510  lkr0f  39587  lshpsmreu  39602  cvrnbtwn4  39772  ishlat2  39846  islvol5  40072  tendoeq2  41267  dibelval3  41640  mapdpglem3  42168  hdmapglem7a  42420  4rexfrabdioph  43244  dford4  43475  fgraphopab  43649  onsupmaxb  43685  tfsconcatlem  43782  ifpim123g  43945  ifpbibib  43955  rp-isfinite6  43963  elrncard  43982  undmrnresiss  44049  cnvssco  44051  iunrelexpuztr  44164  dffrege115  44423  brco2f1o  44477  ntrneiiso  44536  ismnuprim  44739  undisjrab  44751  radcnvrat  44759  opelopab4  44996  2sb5nd  45005  un2122  45234  uunT12p4  45247  2sb5ndVD  45354  2sb5ndALT  45376  ndisj2  45500  ssabf  45548  abssf  45560  fourierdlem42  46593  smflimlem4  47218  aiotaexaiotaiota  47558  ndmaovcom  47669  dmafv2rnb  47693  afv2ndeffv0  47724  modm1p1ne  47840  0nelsetpreimafv  47866  usgrexmpl2nb0  48523  usgrexmpl2nb1  48524  gpg5nbgrvtx03starlem1  48560  gpg5nbgrvtx03starlem2  48561  gpg5nbgrvtx03starlem3  48562  gpg5nbgrvtx13starlem1  48563  gpg5nbgrvtx13starlem2  48564  gpg5nbgrvtx13starlem3  48565  pgnbgreunbgrlem2lem2  48607  gpg5edgnedg  48622  eliunxp2  48826  pgrpgt2nabl  48858  islindeps  48945  lindslinindsimp1  48949  lindslinindsimp2  48955