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  645  anandi  674  anandir  675  orordi  925  orordir  926  ianor  978  trunantru  1574  falnanfal  1577  had0  1601  nic-axALT  1671  equsexvw  2007  sbiedvw  2100  sbievw2  2103  sbal  2161  sb6a  2254  sb56  2273  sbco4  2280  sbiedw  2328  sbiedwOLD  2329  sbied  2541  sbidm  2548  sbiedALT  2610  mo  2645  2mos  2730  2eu6  2740  cbvabv  2889  cbvabw  2890  cbvab  2891  nabbi  3121  rexcom4a  3251  r19.41v  3347  r19.41  3348  2ralor  3370  spc2ed  3602  2reuswap  3737  2reuswap2  3738  2reu5  3749  2rmoswap  3752  nfcdeq  3768  sbcid  3789  sbcco2  3799  sbc7  3803  sbcie2g  3811  eqsbc3  3817  eqsbc3OLD  3818  sbcralt  3855  cbvralcsf  3925  cbvrabcsf  3928  abss  4040  ssab  4041  raldifb  4121  difrab  4277  euelss  4290  sbccsb  4385  vdif0  4418  difrab0eq  4419  ssunsn2  4754  sspr  4760  sstp  4761  uniintsn  4906  brab1  5107  unopab  5138  axrep5  5189  axrep6  5190  intexab  5235  reusv2lem4  5294  reusv2  5296  wefrc  5544  eliunxp  5703  ralxp  5707  rexxp  5708  opelco  5737  reldm0  5793  resieq  5859  iss  5898  imai  5937  cnvsym  5969  intasym  5970  asymref  5971  codir  5975  poirr2  5979  xpdifid  6020  rninxp  6031  tz6.26  6174  wfis2fg  6180  ordelord  6208  ordtri3  6222  dffun3  6361  funopg  6384  fin  6554  f1cnvcnv  6579  funimass4  6725  fnressn  6915  resoprab  7264  mpo2eqb  7277  elrnmpores  7282  ov6g  7306  offval  7410  uniuni  7478  dfwe2  7490  orduniorsuc  7539  tfinds2  7572  dfopab2  7744  dfoprab3s  7745  fmpox  7759  fparlem1  7801  fparlem2  7802  brtpos0  7893  dftpos3  7904  tpostpos  7906  dfrecs3  8003  tz7.48lem  8071  omeu  8205  ercnv  8304  ixp0  8489  xpcomco  8601  xpassen  8605  php  8695  findcard3  8755  ixpfi2  8816  dfsup2  8902  sup0riota  8923  card2on  9012  infeq5i  9093  cnfcom3lem  9160  r1elss  9229  rankxplim  9302  scott0s  9311  aceq1  9537  dfac5lem1  9543  dfac5lem2  9544  kmlem3  9572  kmlem8  9577  kmlem16  9585  djuinf  9608  cflem  9662  cf0  9667  alephval2  9988  fpwwe2lem8  10053  fpwwe2lem12  10057  rankcf  10193  r1tskina  10198  wfgru  10232  genpass  10425  psslinpr  10447  ltpsrpr  10525  addeq0  11057  infm3  11594  nnwos  12309  ioo0  12757  ico0  12778  ioc0  12779  icc0  12780  elfz2nn0  12992  elfzmlbp  13012  sqeqori  13570  hashgt12el  13777  hashgt12el2  13778  cshwidxmod  14159  clim0  14857  divalglem6  15743  ncoprmlnprm  16062  pceu  16177  prmreclem2  16247  cshwshash  16432  xpscf  16832  acsfn2  16928  invsym2  17027  pospo  17577  issubmndb  17964  f1omvdco3  18571  psgnunilem5  18616  efgrelexlemb  18870  gexex  18967  srgrmhm  19280  lssne0  19716  opsrtoslem1  20258  opsrtoslem2  20259  islindf4  20976  mdetunilem8  21222  cpmatmcllem  21320  pmatcollpw2lem  21379  ntreq0  21679  ordtrest2lem  21805  ist0-3  21947  ist1-2  21949  ist1-3  21951  cmpfi  22010  2ndcctbss  22057  ptbasfi  22183  ptcnplem  22223  hausdiag  22247  hauseqlcld  22248  cnmptcom  22280  txflf  22608  tgphaus  22719  metrest  23128  iccpnfcnv  23542  bcth3  23928  dyadmax  24193  vitalilem2  24204  vitalilem3  24205  mbfimaopnlem  24250  itg2leub  24329  dvres2  24504  ellogdm  25216  reasinsin  25468  leibpilem2  25513  ftalem3  25646  dchreq  25828  legso  26379  outpasch  26535  axcontlem2  26745  incistruhgr  26858  nbgrel  27116  usgr2pth0  27540  rusgrnumwwlkslem  27742  frgr3v  28048  4cycl2vnunb  28063  frgrncvvdeqlem2  28073  lnon0  28569  spansncvi  29423  pjssmii  29452  nmlnopgt0i  29768  largei  30038  cvexchlem  30139  xfree  30215  nmo  30248  reuxfrdf  30249  fpwrelmapffslem  30462  eliccioo  30602  qtophaus  31095  ordtrest2NEWlem  31160  ordtconnlem1  31162  xrge0iifcnv  31171  xrge0iifiso  31173  xrge0iifhom  31175  cntnevol  31482  eulerpartlemgh  31631  ballotlem7  31788  signswch  31826  bnj446  31982  bnj563  32009  bnj110  32125  bnj153  32147  bnj864  32189  bnj865  32190  bnj849  32192  bnj929  32203  bnj1110  32249  cusgr3cyclex  32378  derang0  32411  iccllysconn  32492  cvmsss2  32516  satf0op  32619  elmrsubrn  32762  quad3  32908  axacprim  32928  dftr6  32981  dfpo2  32986  elintfv  33002  opelco3  33013  elima4  33014  setinds2f  33019  elpotr  33021  frpoins2fg  33077  frins2fg  33084  wzel  33106  bdayimaon  33192  elfuns  33371  dfiota3  33379  brimg  33393  imagesset  33409  lineunray  33603  ellines  33608  hfninf  33642  bj-snglc  34276  bj-mpomptALT  34405  bj-elid7  34457  bj-isrvec  34569  nlpineqsn  34683  curf  34864  tan2h  34878  poimirlem26  34912  poimirlem27  34913  poimirlem30  34916  poimirlem32  34918  poimir  34919  ovoliunnfl  34928  voliunnfl  34930  ftc1anc  34969  inixp  34997  heibor1lem  35081  csbcom2fi  35400  tsna1  35416  anan  35493  brid  35558  idinxpssinxp4  35571  iss2  35595  xrninxp  35634  cossssid3  35703  dmqs1cosscnvepreseq  35890  islshpat  36147  lkr0f  36224  lshpsmreu  36239  cvrnbtwn4  36409  ishlat2  36483  islvol5  36709  tendoeq2  37904  dibelval3  38277  mapdpglem3  38805  hdmapglem7a  39057  4rexfrabdioph  39388  dford4  39619  isdomn3  39797  fgraphopab  39803  ifpim123g  39859  ifpbibib  39869  rp-isfinite6  39877  elrncard  39895  undmrnresiss  39957  cnvssco  39959  iunrelexpuztr  40057  dffrege115  40317  brco2f1o  40375  ntrneiiso  40434  ismnuprim  40623  undisjrab  40631  radcnvrat  40639  opelopab4  40878  2sb5nd  40887  un2122  41117  uunT12p4  41130  2sb5ndVD  41237  2sb5ndALT  41259  ndisj2  41306  ssabf  41359  abssf  41371  fourierdlem42  42427  smflimlem4  43043  aiotaexaiotaiota  43285  ndmaovcom  43397  dmafv2rnb  43421  afv2ndeffv0  43452  0nelsetpreimafv  43543  eliunxp2  44375  pgrpgt2nabl  44407  islindeps  44501  lindslinindsimp1  44505  lindslinindsimp2  44511