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  5220  axrep6OLD  5222  intexab  5281  reusv2lem4  5336  reusv2  5338  elOLD  5384  wefrc  5616  eliunxp  5784  ralxp  5788  rexxp  5789  opelco  5818  reldm0  5875  resieq  5947  iss  5992  imai  6031  intasym  6070  asymref  6071  codir  6075  poirr2  6079  xpdifid  6124  rninxp  6135  dfpo2  6252  frpoins2fg  6300  ordelord  6337  ordtri3  6351  funopg  6524  fin  6712  f1cnvcnv  6737  funimass4  6896  fnressn  7103  resoprab  7476  mpo2eqb  7490  elrnmpores  7496  ov6g  7522  imaeqexov  7596  imaeqalov  7597  offval  7631  uniuni  7707  dfwe2  7719  orduniorsuc  7772  tfinds2  7806  dfopab2  7996  dfoprab3s  7997  fmpox  8011  fparlem1  8053  fparlem2  8054  ralxp3f  8078  frpoins3xpg  8081  brtpos0  8174  dftpos3  8185  tpostpos  8187  dfrecs3  8303  tz7.48lem  8371  omeu  8511  ercnv  8656  ixp0  8870  xpcomco  8996  xpassen  9000  php  9132  findcard3  9184  ixpfi2  9251  dfsup2  9348  sup0riota  9370  card2on  9460  infeq5i  9546  cnfcom3lem  9613  ssttrcl  9625  ttrcltr  9626  ttrclss  9630  setinds2f  9660  frins2f  9666  r1elss  9719  rankxplim  9792  scott0s  9801  aceq1  10028  dfac5lem1  10034  dfac5lem2  10035  kmlem3  10064  kmlem8  10069  kmlem16  10077  djuinf  10100  cflemOLD  10157  cf0  10162  alephval2  10484  fpwwe2lem7  10549  fpwwe2lem11  10553  rankcf  10689  r1tskina  10694  wfgru  10728  genpass  10921  psslinpr  10943  ltpsrpr  11021  addeq0  11562  infm3  12104  nnwos  12854  ioo0  13312  ico0  13333  ioc0  13334  icc0  13335  elfz2nn0  13561  elfzmlbp  13582  sqeqori  14165  hashgt12el  14373  hashgt12el2  14374  cshwidxmod  14754  clim0  15457  divalglem6  16356  ncoprmlnprm  16687  pceu  16806  prmreclem2  16877  cshwshash  17064  xpscf  17518  acsfn2  17618  invsym2  17719  cat1  18053  pospo  18298  issubmndb  18762  f1omvdco3  19413  psgnunilem5  19458  efgrelexlemb  19714  gexex  19817  srgrmhm  20192  isdomn3  20681  isdomn4r  20685  lssne0  20935  islindf4  21826  opsrtoslem1  22042  opsrtoslem2  22043  mdetunilem8  22593  cpmatmcllem  22692  pmatcollpw2lem  22751  ntreq0  23051  ordtrest2lem  23177  ist0-3  23319  ist1-2  23321  ist1-3  23323  cmpfi  23382  2ndcctbss  23429  ptbasfi  23555  ptcnplem  23595  hausdiag  23619  hauseqlcld  23620  cnmptcom  23652  txflf  23980  tgphaus  24091  metrest  24498  iccpnfcnv  24920  bcth3  25307  dyadmax  25574  vitalilem2  25585  vitalilem3  25586  mbfimaopnlem  25631  itg2leub  25710  dvres2  25888  ellogdm  26619  reasinsin  26877  leibpilem2  26922  ftalem3  27056  dchreq  27240  bdayimaon  27676  noetainflem4  27723  cuteq1  27828  addsprop  27987  leadds1  28000  negsprop  28046  mulsprop  28141  mulsuniflem  28160  addsdilem1  28162  addsdilem2  28163  mulsasslem1  28174  mulsasslem2  28175  precsexlem10  28227  precsexlem11  28228  onnolt  28277  bdayn0p1  28380  legso  28686  outpasch  28842  axcontlem2  29053  incistruhgr  29167  nbgrel  29428  usgr2pth0  29853  rusgrnumwwlkslem  30060  frgr3v  30365  4cycl2vnunb  30380  frgrncvvdeqlem2  30390  lnon0  30889  spansncvi  31743  pjssmii  31772  nmlnopgt0i  32088  largei  32358  cvexchlem  32459  xfree  32535  nmo  32579  reuxfrdf  32580  fpwrelmapffslem  32825  eliccioo  33010  1arithidom  33617  ufdprmidl  33621  qtophaus  34001  ordtrest2NEWlem  34087  ordtconnlem1  34089  xrge0iifcnv  34098  xrge0iifiso  34100  xrge0iifhom  34102  cntnevol  34393  eulerpartlemgh  34543  ballotlem7  34701  signswch  34726  bnj446  34881  bnj563  34907  bnj110  35021  bnj153  35043  bnj864  35085  bnj865  35086  bnj849  35088  bnj929  35099  bnj1110  35145  fineqvac  35281  axregs  35304  cusgr3cyclex  35339  derang0  35372  iccllysconn  35453  cvmsss2  35477  satf0op  35580  elmrsubrn  35723  rexxfr3dALT  35842  quad3  35873  axacprim  35910  dftr6  35954  elintfv  35968  opelco3  35978  elima4  35979  elpotr  35982  wzel  36025  elfuns  36116  dfiota3  36124  brimg  36138  imagesset  36156  lineunray  36350  ellines  36355  hfninf  36389  in-ax8  36427  ss-ax8  36428  bj-df-sb  36957  bj-elabtru  37194  bj-snglc  37289  bj-mpomptALT  37444  bj-elid7  37498  bj-imdirco  37517  nlpineqsn  37735  curf  37930  tan2h  37944  poimirlem26  37978  poimirlem27  37979  poimirlem30  37982  poimirlem32  37984  poimir  37985  ovoliunnfl  37994  voliunnfl  37996  ftc1anc  38033  inixp  38060  heibor1lem  38141  csbcom2fi  38460  tsna1  38476  anan  38567  brid  38644  ref5  38651  idinxpssinxp4  38658  iss2  38676  raldmqseu  38697  xrninxp  38747  cossssid3  38891  dmqs1cosscnvepreseq  39079  disjxrnres5  39179  dmqsblocks  39299  islshpat  39474  lkr0f  39551  lshpsmreu  39566  cvrnbtwn4  39736  ishlat2  39810  islvol5  40036  tendoeq2  41231  dibelval3  41604  mapdpglem3  42132  hdmapglem7a  42384  4rexfrabdioph  43241  dford4  43472  fgraphopab  43646  onsupmaxb  43682  tfsconcatlem  43779  ifpim123g  43942  ifpbibib  43952  rp-isfinite6  43960  elrncard  43979  undmrnresiss  44046  cnvssco  44048  iunrelexpuztr  44161  dffrege115  44420  brco2f1o  44474  ntrneiiso  44533  ismnuprim  44736  undisjrab  44748  radcnvrat  44756  opelopab4  44993  2sb5nd  45002  un2122  45231  uunT12p4  45244  2sb5ndVD  45351  2sb5ndALT  45373  ndisj2  45497  ssabf  45545  abssf  45557  fourierdlem42  46592  smflimlem4  47217  aiotaexaiotaiota  47539  ndmaovcom  47650  dmafv2rnb  47674  afv2ndeffv0  47705  modm1p1ne  47821  0nelsetpreimafv  47847  usgrexmpl2nb0  48504  usgrexmpl2nb1  48505  gpg5nbgrvtx03starlem1  48541  gpg5nbgrvtx03starlem2  48542  gpg5nbgrvtx03starlem3  48543  gpg5nbgrvtx13starlem1  48544  gpg5nbgrvtx13starlem2  48545  gpg5nbgrvtx13starlem3  48546  pgnbgreunbgrlem2lem2  48588  gpg5edgnedg  48603  eliunxp2  48807  pgrpgt2nabl  48839  islindeps  48926  lindslinindsimp1  48930  lindslinindsimp2  48936