Theorem bitr3i 279

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

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  3bitrri  300  3bitr3i  303  3bitr3ri  304  xchnxbi  334  an13  655  anandi  684  anandir  685  orordi  937  orordir  938  ianor  992  trunantru  1595  falnanfal  1598  had0  1618  nic-axALT  1688  equsexvw  2019  sbiedvw  2123  sbievw2  2126  cbvsbv  2128  sbal  2197  sbco4OLD  2202  sb6a  2287  sbiedw  2342  sbied  2528  sbidm  2535  mo  2586  2eu6  2677  cbvab  2828  nabbib  3054  rexcom4a  3286  abv  3460  ceqsex  3495  ceqsexv  3496  spc2ed  3555  clel2g  3613  2reuswap  3703  2reuswap2  3704  2reu5  3715  2rmoswap  3718  nfcdeq  3734  sbcid  3756  sbcco2  3766  sbc7  3771  sbcie2g  3779  eqsbc1  3785  sbcralt  3820  cbvralcsf  3889  cbvrabcsf  3892  abss  4010  ssab  4011  raldifb  4097  difrab  4265  euelss  4279  sbccsb  4384  vdif0  4417  difrab0eq  4418  ssunsn2  4779  sspr  4787  sstp  4788  uniintsn  4937  brab1  5142  unopab  5174  axrep5  5229  axrep6OLD  5231  intexab  5296  reusv2lem4  5352  reusv2  5354  elOLD  5400  wefrc  5634  eliunxp  5802  ralxp  5806  rexxp  5807  opelco  5836  reldm0  5897  resieq  5969  iss  6014  imai  6053  intasym  6092  asymref  6093  codir  6097  poirr2  6101  xpdifid  6143  rninxp  6154  dfpo2  6272  frpoins2fg  6320  ordelord  6357  ordtri3  6371  funopg  6544  fin  6733  f1cnvcnv  6760  funimass4  6920  fnressn  7130  resoprab  7503  mpo2eqb  7517  elrnmpores  7523  ov6g  7549  imaeqexov  7623  imaeqalov  7624  offval  7658  uniuni  7734  dfwe2  7746  orduniorsuc  7799  tfinds2  7833  dfopab2  8022  dfoprab3s  8023  fmpox  8037  fparlem1  8079  fparlem2  8080  ralxp3f  8105  frpoins3xpg  8108  brtpos0  8201  dftpos3  8212  tpostpos  8214  dfrecs3  8331  tz7.48lem  8400  omeu  8542  ercnv  8688  ixp0  8902  xpcomco  9028  xpassen  9032  php  9164  findcard3  9216  ixpfi2  9283  dfsup2  9380  sup0riota  9402  card2on  9492  infeq5i  9581  cnfcom3lem  9648  ssttrcl  9660  ttrcltr  9661  ttrclss  9665  setinds2f  9695  frins2f  9701  r1elss  9754  rankxplim  9827  scott0s  9836  aceq1  10063  dfac5lem1  10069  dfac5lem2  10070  kmlem3  10099  kmlem8  10104  kmlem16  10112  djuinf  10135  cflemOLD  10192  cf0  10197  alephval2  10520  fpwwe2lem7  10585  fpwwe2lem11  10589  rankcf  10725  r1tskina  10730  wfgru  10764  genpass  10957  psslinpr  10979  ltpsrpr  11057  addeq0  11600  infm3  12141  nnwos  12906  ioo0  13364  ico0  13385  ioc0  13386  icc0  13387  elfz2nn0  13613  elfzmlbp  13634  sqeqori  14217  hashgt12el  14425  hashgt12el2  14426  cshwidxmod  14806  clim0  15509  divalglem6  16408  ncoprmlnprm  16739  pceu  16858  prmreclem2  16929  cshwshash  17116  xpscf  17571  acsfn2  17671  invsym2  17772  cat1  18106  pospo  18351  issubmndb  18815  f1omvdco3  19465  psgnunilem5  19510  efgrelexlemb  19766  gexex  19869  srgrmhm  20244  isdomn3  20737  isdomn4r  20741  lssne0  20991  islindf4  21863  opsrtoslem1  22081  opsrtoslem2  22082  mdetunilem8  22652  cpmatmcllem  22751  pmatcollpw2lem  22810  ntreq0  23110  ordtrest2lem  23236  ist0-3  23378  ist1-2  23380  ist1-3  23382  cmpfi  23441  2ndcctbss  23488  ptbasfi  23614  ptcnplem  23654  hausdiag  23678  hauseqlcld  23679  cnmptcom  23711  txflf  24039  tgphaus  24150  metrest  24557  iccpnfcnv  24979  bcth3  25366  dyadmax  25633  vitalilem2  25644  vitalilem3  25645  mbfimaopnlem  25690  itg2leub  25769  dvres2  25947  ellogdm  26674  reasinsin  26931  leibpilem2  26976  ftalem3  27109  dchreq  27292  bdayimaon  27727  noetainflem4  27774  cuteq1  27880  addsprop  28039  leadds1  28052  negsprop  28098  mulsprop  28193  mulsuniflem  28212  addsdilem1  28214  addsdilem2  28215  mulsasslem1  28226  mulsasslem2  28227  precsexlem10  28279  precsexlem11  28280  onnolt  28329  bdayn0p1  28432  legso  28738  outpasch  28894  axcontlem2  29105  incistruhgr  29219  nbgrel  29480  usgr2pth0  29904  rusgrnumwwlkslem  30111  frgr3v  30416  4cycl2vnunb  30431  frgrncvvdeqlem2  30441  lnon0  30940  spansncvi  31794  pjssmii  31823  nmlnopgt0i  32139  largei  32409  cvexchlem  32510  xfree  32586  nmo  32630  reuxfrdf  32631  fpwrelmapffslem  32877  eliccioo  33062  1arithidom  33687  ufdprmidl  33691  qtophaus  34087  ordtrest2NEWlem  34173  ordtconnlem1  34175  xrge0iifcnv  34184  xrge0iifiso  34186  xrge0iifhom  34188  cntnevol  34479  eulerpartlemgh  34629  ballotlem7  34787  signswch  34812  bnj446  34970  bnj563  34996  bnj110  35110  bnj153  35132  bnj864  35174  bnj865  35175  bnj849  35177  bnj929  35188  bnj1110  35234  fineqvac  35367  axregs  35390  cusgr3cyclex  35434  derang0  35467  iccllysconn  35548  cvmsss2  35572  satf0op  35675  elmrsubrn  35818  rexxfr3dALT  35937  quad3  35968  axacprim  36005  dftr6  36049  elintfv  36063  opelco3  36073  elima4  36074  elpotr  36077  wzel  36120  elfuns  36211  dfiota3  36219  brimg  36233  imagesset  36251  lineunray  36445  ellines  36450  hfninf  36484  in-ax8  36532  ss-ax8  36533  bj-df-sb  37070  bj-elabtru  37307  bj-snglc  37402  bj-mpomptALT  37557  bj-elid7  37611  bj-imdirco  37630  nlpineqsn  37850  curf  38045  tan2h  38059  poimirlem26  38093  poimirlem27  38094  poimirlem30  38097  poimirlem32  38099  poimir  38100  ovoliunnfl  38109  voliunnfl  38111  ftc1anc  38148  inixp  38175  heibor1lem  38256  csbcom2fi  38575  tsna1  38591  anan  38682  brid  38759  ref5  38766  idinxpssinxp4  38773  iss2  38791  raldmqseu  38812  xrninxp  38862  cossssid3  39006  dmqs1cosscnvepreseq  39194  disjxrnres5  39294  dmqsblocks  39414  islshpat  39589  lkr0f  39666  lshpsmreu  39681  cvrnbtwn4  39851  ishlat2  39925  islvol5  40151  tendoeq2  41346  dibelval3  41719  mapdpglem3  42247  hdmapglem7a  42499  4rexfrabdioph  43323  dford4  43554  fgraphopab  43728  onsupmaxb  43764  tfsconcatlem  43861  ifpim123g  44024  ifpbibib  44034  rp-isfinite6  44042  elrncard  44061  undmrnresiss  44128  cnvssco  44130  iunrelexpuztr  44243  dffrege115  44502  brco2f1o  44556  ntrneiiso  44615  ismnuprim  44818  undisjrab  44830  radcnvrat  44838  opelopab4  45075  2sb5nd  45084  un2122  45313  uunT12p4  45326  2sb5ndVD  45433  2sb5ndALT  45455  ndisj2  45579  ssabf  45626  abssf  45638  fourierdlem42  46671  smflimlem4  47296  aiotaexaiotaiota  47636  ndmaovcom  47747  dmafv2rnb  47771  afv2ndeffv0  47802  modm1p1ne  47918  0nelsetpreimafv  47944  usgrexmpl2nb0  48601  usgrexmpl2nb1  48602  gpg5nbgrvtx03starlem1  48638  gpg5nbgrvtx03starlem2  48639  gpg5nbgrvtx03starlem3  48640  gpg5nbgrvtx13starlem1  48641  gpg5nbgrvtx13starlem2  48642  gpg5nbgrvtx13starlem3  48643  pgnbgreunbgrlem2lem2  48685  gpg5edgnedg  48700  eliunxp2  48904  pgrpgt2nabl  48936  islindeps  49023  lindslinindsimp1  49027  lindslinindsimp2  49033