Theorem bitr3i 280

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

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  3bitrri  301  3bitr3i  304  3bitr3ri  305  xchnxbi  335  an13  659  anandi  688  anandir  689  orordi  941  orordir  942  ianor  997  trunantru  1604  falnanfal  1607  had0  1627  nic-axALT  1697  equsexvw  2028  sbiedvw  2132  sbievw2  2135  cbvsbv  2137  sbal  2206  sbco4OLD  2211  sb6a  2296  sbiedw  2351  sbied  2537  sbidm  2544  mo  2595  2eu6  2686  cbvab  2837  nabbib  3063  rexcom4a  3295  abv  3469  ceqsex  3504  ceqsexv  3505  spc2ed  3563  clel2g  3621  2reuswap  3712  2reuswap2  3713  2reu5  3724  2rmoswap  3727  nfcdeq  3743  sbcid  3764  sbcco2  3774  sbc7  3779  sbcie2g  3787  eqsbc1  3793  sbcralt  3828  cbvralcsf  3897  cbvrabcsf  3900  abss  4018  ssab  4019  raldifb  4105  difrab  4273  euelss  4287  sbccsb  4393  vdif0  4426  difrab0eq  4427  ssunsn2  4788  sspr  4796  sstp  4797  uniintsn  4946  brab1  5153  unopab  5185  axrep5  5240  axrep6OLD  5242  intexab  5307  reusv2lem4  5363  reusv2  5365  elOLD  5411  wefrc  5646  eliunxp  5814  ralxp  5818  rexxp  5819  opelco  5848  reldm0  5909  resieq  5980  iss  6028  imai  6067  intasym  6106  asymref  6107  codir  6111  poirr2  6115  xpdifid  6157  rninxp  6169  dfpo2  6287  frpoins2fg  6335  ordelord  6372  ordtri3  6386  funopg  6559  fin  6748  f1cnvcnv  6775  funimass4  6935  fnressn  7145  resoprab  7518  mpo2eqb  7532  elrnmpores  7538  ov6g  7564  imaeqexov  7638  imaeqalov  7639  offval  7673  uniuni  7749  dfwe2  7761  orduniorsuc  7814  tfinds2  7848  dfopab2  8037  dfoprab3s  8038  fmpox  8052  fparlem1  8095  fparlem2  8096  ralxp3f  8121  frpoins3xpg  8124  brtpos0  8217  dftpos3  8228  tpostpos  8230  dfrecs3  8347  tz7.48lem  8416  omeu  8558  ercnv  8704  ixp0  8917  xpcomco  9043  xpassen  9047  php  9179  findcard3  9231  ixpfi2  9295  dfsup2  9392  sup0riota  9414  card2on  9504  infeq5i  9593  cnfcom3lem  9660  ssttrcl  9672  ttrcltr  9673  ttrclss  9677  setinds2f  9707  frins2f  9713  r1elss  9766  rankxplim  9839  scott0s  9850  aceq1  10089  dfac5lem1  10095  dfac5lem2  10096  kmlem3  10124  kmlem8  10129  kmlem16  10137  djuinf  10160  cflemOLD  10217  cf0  10222  alephval2  10545  fpwwe2lem7  10610  fpwwe2lem11  10614  rankcf  10750  r1tskina  10755  wfgru  10789  genpass  10982  psslinpr  11004  ltpsrpr  11082  addeq0  11625  infm3  12165  nnwos  12930  ioo0  13388  ico0  13409  ioc0  13410  icc0  13411  elfz2nn0  13637  elfzmlbp  13658  sqeqori  14241  hashgt12el  14449  hashgt12el2  14450  cshwidxmod  14830  clim0  15547  divalglem6  16446  ncoprmlnprm  16777  pceu  16896  prmreclem2  16967  cshwshash  17154  xpscf  17609  acsfn2  17709  invsym2  17810  cat1  18144  pospo  18389  issubmndb  18853  f1omvdco3  19510  psgnunilem5  19555  efgrelexlemb  19811  gexex  19914  srgrmhm  20295  isdomn3  20790  isdomn4r  20794  lssne0  21041  islindf4  21948  opsrtoslem1  22166  opsrtoslem2  22167  mdetunilem8  22737  cpmatmcllem  22836  pmatcollpw2lem  22895  ntreq0  23195  ordtrest2lem  23321  ist0-3  23463  ist1-2  23465  ist1-3  23467  cmpfi  23526  2ndcctbss  23573  ptbasfi  23699  ptcnplem  23739  hausdiag  23763  hauseqlcld  23764  cnmptcom  23796  txflf  24124  tgphaus  24235  metrest  24642  iccpnfcnv  25064  bcth3  25451  dyadmax  25718  vitalilem2  25729  vitalilem3  25730  mbfimaopnlem  25775  itg2leub  25854  dvres2  26032  ellogdm  26762  reasinsin  27019  leibpilem2  27064  ftalem3  27197  dchreq  27380  bdayimaon  27815  noetainflem4  27862  cuteq1  27968  addsprop  28127  leadds1  28140  negsprop  28186  mulsprop  28281  mulsuniflem  28300  addsdilem1  28302  addsdilem2  28303  mulsasslem1  28314  mulsasslem2  28315  precsexlem10  28367  precsexlem11  28368  onnolt  28417  bdayn0p1  28520  legso  28826  outpasch  28986  axcontlem2  29224  incistruhgr  29338  nbgrel  29599  usgr2pth0  30023  rusgrnumwwlkslem  30230  frgr3v  30535  4cycl2vnunb  30550  frgrncvvdeqlem2  30560  lnon0  31059  spansncvi  31913  pjssmii  31942  nmlnopgt0i  32258  largei  32528  cvexchlem  32629  xfree  32705  nmo  32746  reuxfrdf  32747  fpwrelmapffslem  32989  eliccioo  33163  1arithidom  33744  ufdprmidl  33748  qtophaus  34143  ordtrest2NEWlem  34229  ordtconnlem1  34231  xrge0iifcnv  34240  xrge0iifiso  34242  xrge0iifhom  34244  cntnevol  34535  eulerpartlemgh  34685  ballotlem7  34843  signswch  34865  bnj446  35023  bnj563  35049  bnj110  35163  bnj153  35185  bnj864  35227  bnj865  35228  bnj849  35230  bnj929  35241  bnj1110  35287  fineqvac  35424  axregs  35447  cusgr3cyclex  35499  derang0  35532  iccllysconn  35613  cvmsss2  35637  satf0op  35740  elmrsubrn  35883  rexxfr3dALT  36002  quad3  36033  axacprim  36070  dftr6  36114  elintfv  36128  opelco3  36138  elima4  36139  elpotr  36142  wzel  36185  elfuns  36276  dfiota3  36284  brimg  36298  imagesset  36316  lineunray  36510  ellines  36515  hfninf  36549  in-ax8  36597  ss-ax8  36598  bj-df-sb  37134  bj-elabtru  37371  bj-snglc  37466  bj-mpomptALT  37621  bj-elid7  37675  bj-imdirco  37694  nlpineqsn  37914  curf  38109  tan2h  38123  poimirlem26  38157  poimirlem27  38158  poimirlem30  38161  poimirlem32  38163  poimir  38164  ovoliunnfl  38173  voliunnfl  38175  ftc1anc  38212  inixp  38239  heibor1lem  38320  csbcom2fi  38639  tsna1  38655  anan  38746  brid  38823  ref5  38830  idinxpssinxp4  38837  iss2  38855  raldmqseu  38876  xrninxp  38926  cossssid3  39070  dmqs1cosscnvepreseq  39258  disjxrnres5  39358  dmqsblocks  39478  islshpat  39653  lkr0f  39730  lshpsmreu  39745  cvrnbtwn4  39915  ishlat2  39989  islvol5  40215  tendoeq2  41410  dibelval3  41783  mapdpglem3  42311  hdmapglem7a  42563  4rexfrabdioph  43387  dford4  43618  fgraphopab  43792  onsupmaxb  43828  tfsconcatlem  43925  ifpim123g  44088  ifpbibib  44098  rp-isfinite6  44106  elrncard  44125  undmrnresiss  44192  cnvssco  44194  iunrelexpuztr  44307  dffrege115  44566  brco2f1o  44620  ntrneiiso  44679  ismnuprim  44868  undisjrab  44880  radcnvrat  44888  opelopab4  45125  2sb5nd  45134  un2122  45363  uunT12p4  45376  2sb5ndVD  45483  2sb5ndALT  45505  ndisj2  45629  ssabf  45676  abssf  45688  fourierdlem42  46721  smflimlem4  47346  aiotaexaiotaiota  47686  ndmaovcom  47797  dmafv2rnb  47821  afv2ndeffv0  47852  modm1p1ne  47968  0nelsetpreimafv  47994  usgrexmpl2nb0  48651  usgrexmpl2nb1  48652  gpg5nbgrvtx03starlem1  48688  gpg5nbgrvtx03starlem2  48689  gpg5nbgrvtx03starlem3  48690  gpg5nbgrvtx13starlem1  48691  gpg5nbgrvtx13starlem2  48692  gpg5nbgrvtx13starlem3  48693  pgnbgreunbgrlem2lem2  48735  gpg5edgnedg  48750  eliunxp2  48965  pgrpgt2nabl  48997  islindeps  49084  lindslinindsimp1  49088  lindslinindsimp2  49094