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  646  anandi  675  anandir  676  orordi  927  orordir  928  ianor  982  trunantru  1578  falnanfal  1581  had0  1601  nic-axALT  1672  equsexvw  2004  sbiedvw  2095  sbievw2  2098  cbvsbv  2100  sbal  2170  sbco4OLD  2176  sb6a  2259  sb56OLD  2279  sbiedw  2320  sbied  2511  sbidm  2518  mo  2568  2mosOLD  2653  2eu6  2660  cbvab  2817  nabbib  3051  2ralorOLD  3238  rexcom4a  3298  abv  3500  ceqsex  3540  ceqsexv  3542  spc2ed  3614  clel2g  3672  2reuswap  3768  2reuswap2  3769  2reu5  3780  2rmoswap  3783  nfcdeq  3799  sbcid  3821  sbcco2  3831  sbc7  3837  sbcie2g  3847  eqsbc1  3854  sbcralt  3894  cbvralcsf  3966  cbvrabcsf  3969  abss  4086  ssab  4087  raldifb  4172  difrab  4337  euelss  4351  vn0  4368  sbccsb  4459  vdif0  4492  difrab0eq  4493  ssunsn2  4852  sspr  4860  sstp  4861  uniintsn  5009  brab1  5214  unopab  5248  axrep5  5309  axrep6  5310  intexab  5364  reusv2lem4  5419  reusv2  5421  el  5457  wefrc  5694  eliunxp  5862  ralxp  5866  rexxp  5867  opelco  5896  reldm0  5952  resieq  6020  iss  6064  imai  6103  cnvsymOLDOLD  6146  intasym  6147  asymref  6148  codir  6152  poirr2  6156  xpdifid  6199  rninxp  6210  dfpo2  6327  frpoins2fg  6376  tz6.26OLD  6380  wfis2fgOLD  6389  ordelord  6417  ordtri3  6431  dffun3OLD  6588  funopg  6612  fin  6801  f1cnvcnv  6826  funimass4  6986  fnressn  7192  resoprab  7568  mpo2eqb  7582  elrnmpores  7588  ov6g  7614  imaeqexov  7688  imaeqalov  7689  offval  7723  uniuni  7797  dfwe2  7809  orduniorsuc  7866  tfinds2  7901  dfopab2  8093  dfoprab3s  8094  fmpox  8108  fparlem1  8153  fparlem2  8154  ralxp3f  8178  frpoins3xpg  8181  brtpos0  8274  dftpos3  8285  tpostpos  8287  dfrecs3  8428  dfrecs3OLD  8429  tz7.48lem  8497  omeu  8641  ercnv  8784  ixp0  8989  xpcomco  9128  xpassen  9132  php  9273  phpOLD  9285  findcard3  9346  findcard3OLD  9347  ixpfi2  9420  dfsup2  9513  sup0riota  9534  card2on  9623  infeq5i  9705  cnfcom3lem  9772  ssttrcl  9784  ttrcltr  9785  ttrclss  9789  frins2f  9822  r1elss  9875  rankxplim  9948  scott0s  9957  aceq1  10186  dfac5lem1  10192  dfac5lem2  10193  kmlem3  10222  kmlem8  10227  kmlem16  10235  djuinf  10258  cflemOLD  10315  cf0  10320  alephval2  10641  fpwwe2lem7  10706  fpwwe2lem11  10710  rankcf  10846  r1tskina  10851  wfgru  10885  genpass  11078  psslinpr  11100  ltpsrpr  11178  addeq0  11713  infm3  12254  nnwos  12980  ioo0  13432  ico0  13453  ioc0  13454  icc0  13455  elfz2nn0  13675  elfzmlbp  13696  sqeqori  14263  hashgt12el  14471  hashgt12el2  14472  cshwidxmod  14851  clim0  15552  divalglem6  16446  ncoprmlnprm  16775  pceu  16893  prmreclem2  16964  cshwshash  17152  xpscf  17625  acsfn2  17721  invsym2  17824  cat1  18164  pospo  18415  issubmndb  18840  f1omvdco3  19491  psgnunilem5  19536  efgrelexlemb  19792  gexex  19895  srgrmhm  20249  isdomn3  20737  isdomn4r  20741  lssne0  20972  islindf4  21881  opsrtoslem1  22102  opsrtoslem2  22103  mdetunilem8  22646  cpmatmcllem  22745  pmatcollpw2lem  22804  ntreq0  23106  ordtrest2lem  23232  ist0-3  23374  ist1-2  23376  ist1-3  23378  cmpfi  23437  2ndcctbss  23484  ptbasfi  23610  ptcnplem  23650  hausdiag  23674  hauseqlcld  23675  cnmptcom  23707  txflf  24035  tgphaus  24146  metrest  24558  iccpnfcnv  24994  bcth3  25384  dyadmax  25652  vitalilem2  25663  vitalilem3  25664  mbfimaopnlem  25709  itg2leub  25789  dvres2  25967  ellogdm  26699  reasinsin  26957  leibpilem2  27002  ftalem3  27136  dchreq  27320  bdayimaon  27756  noetainflem4  27803  cuteq1  27896  addsprop  28027  sleadd1  28040  negsprop  28085  mulsprop  28174  mulsuniflem  28193  addsdilem1  28195  addsdilem2  28196  mulsasslem1  28207  mulsasslem2  28208  precsexlem10  28258  precsexlem11  28259  legso  28625  outpasch  28781  axcontlem2  28998  incistruhgr  29114  nbgrel  29375  usgr2pth0  29801  rusgrnumwwlkslem  30002  frgr3v  30307  4cycl2vnunb  30322  frgrncvvdeqlem2  30332  lnon0  30830  spansncvi  31684  pjssmii  31713  nmlnopgt0i  32029  largei  32299  cvexchlem  32400  xfree  32476  nmo  32518  reuxfrdf  32519  fpwrelmapffslem  32746  eliccioo  32895  1arithidom  33530  ufdprmidl  33534  qtophaus  33782  ordtrest2NEWlem  33868  ordtconnlem1  33870  xrge0iifcnv  33879  xrge0iifiso  33881  xrge0iifhom  33883  cntnevol  34192  eulerpartlemgh  34343  ballotlem7  34500  signswch  34538  bnj446  34693  bnj563  34719  bnj110  34834  bnj153  34856  bnj864  34898  bnj865  34899  bnj849  34901  bnj929  34912  bnj1110  34958  fineqvac  35073  cusgr3cyclex  35104  derang0  35137  iccllysconn  35218  cvmsss2  35242  satf0op  35345  elmrsubrn  35488  rexxfr3dALT  35607  quad3  35638  axacprim  35669  dftr6  35713  elintfv  35728  opelco3  35738  elima4  35739  setinds2f  35743  elpotr  35745  wzel  35788  elfuns  35879  dfiota3  35887  brimg  35901  imagesset  35917  lineunray  36111  ellines  36116  hfninf  36150  in-ax8  36190  ss-ax8  36191  bj-elabtru  36840  bj-snglc  36935  bj-mpomptALT  37085  bj-elid7  37137  bj-imdirco  37156  nlpineqsn  37374  curf  37558  tan2h  37572  poimirlem26  37606  poimirlem27  37607  poimirlem30  37610  poimirlem32  37612  poimir  37613  ovoliunnfl  37622  voliunnfl  37624  ftc1anc  37661  inixp  37688  heibor1lem  37769  csbcom2fi  38088  tsna1  38104  anan  38183  brid  38262  ref5  38269  idinxpssinxp4  38276  iss2  38300  xrninxp  38348  cossssid3  38425  dmqs1cosscnvepreseq  38618  disjxrnres5  38703  islshpat  38973  lkr0f  39050  lshpsmreu  39065  cvrnbtwn4  39235  ishlat2  39309  islvol5  39536  tendoeq2  40731  dibelval3  41104  mapdpglem3  41632  hdmapglem7a  41884  4rexfrabdioph  42754  dford4  42986  fgraphopab  43164  onsupmaxb  43200  tfsconcatlem  43298  ifpim123g  43462  ifpbibib  43472  rp-isfinite6  43480  elrncard  43499  undmrnresiss  43566  cnvssco  43568  iunrelexpuztr  43681  dffrege115  43940  brco2f1o  43994  ntrneiiso  44053  ismnuprim  44263  undisjrab  44275  radcnvrat  44283  opelopab4  44522  2sb5nd  44531  un2122  44761  uunT12p4  44774  2sb5ndVD  44881  2sb5ndALT  44903  ndisj2  44953  ssabf  45002  abssf  45014  fourierdlem42  46070  smflimlem4  46695  aiotaexaiotaiota  47009  ndmaovcom  47120  dmafv2rnb  47144  afv2ndeffv0  47175  0nelsetpreimafv  47264  usgrexmpl2nb0  47846  usgrexmpl2nb1  47847  eliunxp2  48058  pgrpgt2nabl  48091  islindeps  48182  lindslinindsimp1  48186  lindslinindsimp2  48192