Theorem bitr3i 266

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

Syntax hints:   ↔ wb 196

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 197

This theorem is referenced by:  3bitrri  287  3bitr3i  290  3bitr3ri  291  xchnxbi  322  ianor  509  orordi  552  orordir  553  anandi  871  anandir  872  trunantru  1524  falnanfal  1527  had0  1543  nic-axALT  1599  sbied  2409  sbidm  2414  sb6a  2448  sbelx  2458  sbco4  2466  mo  2508  2eu6  2558  bm1.1  2607  cbvab  2746  nabbi  2896  r19.41v  3089  r19.41  3090  2ralor  3109  rexcom4a  3226  2reuswap  3410  2reu5  3416  nfcdeq  3432  sbcid  3452  sbcco2  3459  sbc7  3463  sbcie2g  3469  eqsbc3  3475  sbcralt  3510  cbvralcsf  3565  cbvrabcsf  3568  abss  3671  ssab  3672  raldifb  3750  difrab  3901  euelss  3914  sbccsb  4004  vdif0  4037  difrab0eq  4038  ssunsn2  4359  sspr  4366  sstp  4367  uniintsn  4514  brab1  4700  unopab  4728  axrep5  4776  axsep  4780  intexab  4822  reusv2lem4  4872  reusv2  4874  reuxfrd  4893  wefrc  5108  eliunxp  5259  ralxp  5263  rexxp  5264  opelco  5293  reldm0  5343  resieq  5407  iss  5447  imai  5478  cnvsym  5510  intasym  5511  asymref  5512  codir  5516  poirr2  5520  xpdifid  5562  rninxp  5573  tz6.26  5711  wfis2fg  5717  ordelord  5745  ordtri3  5759  dffun3  5899  funopg  5922  fin  6085  f1cnvcnv  6109  funimass4  6247  fnressn  6425  resoprab  6756  mpt22eqb  6769  elrnmpt2res  6774  ov6g  6798  offval  6904  uniuni  6971  dfwe2  6981  orduniorsuc  7030  tfinds2  7063  resiexg  7102  dfopab2  7222  dfoprab3s  7223  fmpt2x  7236  fparlem1  7277  fparlem2  7278  brtpos0  7359  dftpos3  7370  tpostpos  7372  dfrecs3  7469  tz7.48lem  7536  omeu  7665  ercnv  7763  ixp0  7941  xpcomco  8050  xpassen  8054  php  8144  findcard3  8203  ixpfi2  8264  dfsup2  8350  sup0riota  8371  card2on  8459  infeq5i  8533  cnfcom3lem  8600  r1elss  8669  rankxplim  8742  scott0s  8751  aceq1  8940  dfac5lem1  8946  dfac5lem2  8947  kmlem3  8974  kmlem8  8979  kmlem16  8987  cflem  9068  cf0  9073  alephval2  9394  rankcf  9599  r1tskina  9604  wfgru  9638  genpass  9831  psslinpr  9853  ltpsrpr  9930  infm3  10982  nnwos  11755  ioo0  12200  ico0  12221  ioc0  12222  icc0  12223  elfz2nn0  12431  elfzmlbp  12450  sqeqori  12976  hashgt12el  13210  hashgt12el2  13211  cshwidxmod  13549  clim0  14237  divalglem6  15121  ncoprmlnprm  15436  pceu  15551  prmreclem2  15621  cshwshash  15811  isstruct  15870  xpscf  16226  acsfn2  16324  invsym2  16423  pospo  16973  f1omvdco3  17869  psgnunilem5  17914  efgrelexlemb  18163  gexex  18256  srgrmhm  18536  lssne0  18951  opsrtoslem1  19484  opsrtoslem2  19485  islindf4  20177  mdetunilem8  20425  cpmatmcllem  20523  pmatcollpw2lem  20582  ntreq0  20881  ordtrest2lem  21007  ist0-3  21149  ist1-2  21151  ist1-3  21153  cmpfi  21211  2ndcctbss  21258  ptbasfi  21384  ptcnplem  21424  hausdiag  21448  hauseqlcld  21449  cnmptcom  21481  txflf  21810  tgphaus  21920  metrest  22329  iccpnfcnv  22743  bcth3  23128  volun  23313  dyadmax  23366  vitalilem2  23378  vitalilem3  23379  mbfimaopnlem  23422  itg2leub  23501  dvres2  23676  ellogdm  24385  reasinsin  24623  leibpilem2  24668  ftalem3  24801  dchreq  24983  legso  25494  outpasch  25647  axcontlem2  25845  incistruhgr  25974  usgr2pth0  26661  rusgrnumwwlkslem  26864  frgr3v  27139  4cycl2vnunb  27154  frgrncvvdeqlem2  27164  lnon0  27653  spansncvi  28511  pjssmii  28540  nmlnopgt0i  28856  largei  29126  cvexchlem  29227  xfree  29303  spc2ed  29312  nmo  29325  2reuswap2  29328  fpwrelmapffslem  29507  addeq0  29510  eliccioo  29639  qtophaus  29903  ordtrest2NEWlem  29968  ordtconnlem1  29970  xrge0iifcnv  29979  xrge0iifiso  29981  xrge0iifhom  29983  cntnevol  30291  eulerpartlemgh  30440  ballotlem7  30597  signswch  30638  bnj446  30783  bnj563  30813  bnj110  30928  bnj153  30950  bnj864  30992  bnj865  30993  bnj849  30995  bnj929  31006  bnj1110  31050  derang0  31151  iccllysconn  31232  cvmsss2  31256  elmrsubrn  31417  quad3  31564  axacprim  31584  dftr6  31640  dfpo2  31645  elintfv  31662  opelco3  31678  elima4  31679  setinds2f  31684  elpotr  31686  frins2fg  31744  wzel  31771  wzelOLD  31772  bdayimaon  31843  elfuns  32022  dfiota3  32030  imagesset  32060  lineunray  32254  ellines  32259  hfninf  32293  bj-axrep5  32792  bj-axsep  32793  bj-rexcom4a  32870  bj-snglc  32957  bj-mpt2mptALT  33072  curf  33387  tan2h  33401  poimirlem26  33435  poimirlem27  33436  poimirlem30  33439  poimirlem32  33441  poimir  33442  ovoliunnfl  33451  voliunnfl  33453  ftc1anc  33493  inixp  33523  heibor1lem  33608  csbcom2fi  33934  tsna1  33951  anan  33999  brid  34077  idinxpssinxp4  34091  iss2  34112  islshpat  34304  lkr0f  34381  lshpsmreu  34396  cvrnbtwn4  34566  ishlat2  34640  islvol5  34865  tendoeq2  36062  dibelval3  36436  mapdpglem3  36964  hdmapglem7a  37219  4rexfrabdioph  37362  dford4  37596  isdomn3  37782  fgraphopab  37788  ifpim123g  37845  ifpbibib  37855  undmrnresiss  37910  cnvssco  37912  iunrelexpuztr  38011  dffrege115  38272  brco2f1o  38330  ntrneiiso  38389  undisjrab  38505  radcnvrat  38513  opelopab4  38767  2sb5nd  38776  un2122  39017  uunT12p4  39030  onfrALTlem5VD  39121  2sb5ndVD  39146  2sb5ndALT  39168  ndisj2  39218  ssabf  39280  abssf  39295  fourierdlem42  40366  smflimlem4  40982  2rmoswap  41184  ndmaovcom  41285  eliunxp2  42112  pgrpgt2nabl  42147  islindeps  42242  lindslinindsimp1  42246  lindslinindsimp2  42252