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  647  anandi  676  anandir  677  orordi  928  orordir  929  ianor  983  trunantru  1581  falnanfal  1584  had0  1604  nic-axALT  1674  equsexvw  2005  sbiedvw  2096  sbievw2  2099  cbvsbv  2101  sbal  2170  sbco4OLD  2176  sb6a  2259  sbiedw  2315  sbied  2501  sbidm  2508  mo  2558  2mosOLD  2643  2eu6  2650  cbvab  2801  nabbib  3028  rexcom4a  3267  abv  3459  ceqsex  3496  ceqsexv  3498  spc2ed  3567  clel2g  3625  2reuswap  3717  2reuswap2  3718  2reu5  3729  2rmoswap  3732  nfcdeq  3748  sbcid  3770  sbcco2  3780  sbc7  3785  sbcie2g  3794  eqsbc1  3800  sbcralt  3835  cbvralcsf  3904  cbvrabcsf  3907  abss  4026  ssab  4027  raldifb  4112  difrab  4281  euelss  4295  vn0  4308  sbccsb  4399  vdif0  4432  difrab0eq  4433  ssunsn2  4791  sspr  4799  sstp  4800  uniintsn  4949  brab1  5155  unopab  5187  axrep5  5242  axrep6OLD  5244  intexab  5301  reusv2lem4  5356  reusv2  5358  el  5397  wefrc  5632  eliunxp  5801  ralxp  5805  rexxp  5806  opelco  5835  reldm0  5891  resieq  5961  iss  6006  imai  6045  cnvsymOLDOLD  6087  intasym  6088  asymref  6089  codir  6093  poirr2  6097  xpdifid  6141  rninxp  6152  dfpo2  6269  frpoins2fg  6317  ordelord  6354  ordtri3  6368  dffun3OLD  6526  funopg  6550  fin  6740  f1cnvcnv  6765  funimass4  6925  fnressn  7130  resoprab  7507  mpo2eqb  7521  elrnmpores  7527  ov6g  7553  imaeqexov  7627  imaeqalov  7628  offval  7662  uniuni  7738  dfwe2  7750  orduniorsuc  7805  tfinds2  7840  dfopab2  8031  dfoprab3s  8032  fmpox  8046  fparlem1  8091  fparlem2  8092  ralxp3f  8116  frpoins3xpg  8119  brtpos0  8212  dftpos3  8223  tpostpos  8225  dfrecs3  8341  tz7.48lem  8409  omeu  8549  ercnv  8692  ixp0  8904  xpcomco  9031  xpassen  9035  php  9171  findcard3  9229  findcard3OLD  9230  ixpfi2  9301  dfsup2  9395  sup0riota  9417  card2on  9507  infeq5i  9589  cnfcom3lem  9656  ssttrcl  9668  ttrcltr  9669  ttrclss  9673  frins2f  9706  r1elss  9759  rankxplim  9832  scott0s  9841  aceq1  10070  dfac5lem1  10076  dfac5lem2  10077  kmlem3  10106  kmlem8  10111  kmlem16  10119  djuinf  10142  cflemOLD  10199  cf0  10204  alephval2  10525  fpwwe2lem7  10590  fpwwe2lem11  10594  rankcf  10730  r1tskina  10735  wfgru  10769  genpass  10962  psslinpr  10984  ltpsrpr  11062  addeq0  11601  infm3  12142  nnwos  12874  ioo0  13331  ico0  13352  ioc0  13353  icc0  13354  elfz2nn0  13579  elfzmlbp  13600  sqeqori  14179  hashgt12el  14387  hashgt12el2  14388  cshwidxmod  14768  clim0  15472  divalglem6  16368  ncoprmlnprm  16698  pceu  16817  prmreclem2  16888  cshwshash  17075  xpscf  17528  acsfn2  17624  invsym2  17725  cat1  18059  pospo  18304  issubmndb  18732  f1omvdco3  19379  psgnunilem5  19424  efgrelexlemb  19680  gexex  19783  srgrmhm  20131  isdomn3  20624  isdomn4r  20628  lssne0  20857  islindf4  21747  opsrtoslem1  21962  opsrtoslem2  21963  mdetunilem8  22506  cpmatmcllem  22605  pmatcollpw2lem  22664  ntreq0  22964  ordtrest2lem  23090  ist0-3  23232  ist1-2  23234  ist1-3  23236  cmpfi  23295  2ndcctbss  23342  ptbasfi  23468  ptcnplem  23508  hausdiag  23532  hauseqlcld  23533  cnmptcom  23565  txflf  23893  tgphaus  24004  metrest  24412  iccpnfcnv  24842  bcth3  25231  dyadmax  25499  vitalilem2  25510  vitalilem3  25511  mbfimaopnlem  25556  itg2leub  25635  dvres2  25813  ellogdm  26548  reasinsin  26806  leibpilem2  26851  ftalem3  26985  dchreq  27169  bdayimaon  27605  noetainflem4  27652  cuteq1  27746  addsprop  27883  sleadd1  27896  negsprop  27941  mulsprop  28033  mulsuniflem  28052  addsdilem1  28054  addsdilem2  28055  mulsasslem1  28066  mulsasslem2  28067  precsexlem10  28118  precsexlem11  28119  onnolt  28167  bdayn0p1  28258  legso  28526  outpasch  28682  axcontlem2  28892  incistruhgr  29006  nbgrel  29267  usgr2pth0  29695  rusgrnumwwlkslem  29899  frgr3v  30204  4cycl2vnunb  30219  frgrncvvdeqlem2  30229  lnon0  30727  spansncvi  31581  pjssmii  31610  nmlnopgt0i  31926  largei  32196  cvexchlem  32297  xfree  32373  nmo  32419  reuxfrdf  32420  fpwrelmapffslem  32655  eliccioo  32851  1arithidom  33508  ufdprmidl  33512  qtophaus  33826  ordtrest2NEWlem  33912  ordtconnlem1  33914  xrge0iifcnv  33923  xrge0iifiso  33925  xrge0iifhom  33927  cntnevol  34218  eulerpartlemgh  34369  ballotlem7  34527  signswch  34552  bnj446  34707  bnj563  34733  bnj110  34848  bnj153  34870  bnj864  34912  bnj865  34913  bnj849  34915  bnj929  34926  bnj1110  34972  fineqvac  35087  cusgr3cyclex  35123  derang0  35156  iccllysconn  35237  cvmsss2  35261  satf0op  35364  elmrsubrn  35507  rexxfr3dALT  35626  quad3  35657  axacprim  35694  dftr6  35738  elintfv  35752  opelco3  35762  elima4  35763  setinds2f  35767  elpotr  35769  wzel  35812  elfuns  35903  dfiota3  35911  brimg  35925  imagesset  35941  lineunray  36135  ellines  36140  hfninf  36174  in-ax8  36212  ss-ax8  36213  bj-elabtru  36862  bj-snglc  36957  bj-mpomptALT  37107  bj-elid7  37159  bj-imdirco  37178  nlpineqsn  37396  curf  37592  tan2h  37606  poimirlem26  37640  poimirlem27  37641  poimirlem30  37644  poimirlem32  37646  poimir  37647  ovoliunnfl  37656  voliunnfl  37658  ftc1anc  37695  inixp  37722  heibor1lem  37803  csbcom2fi  38122  tsna1  38138  anan  38217  brid  38294  ref5  38301  idinxpssinxp4  38308  iss2  38326  xrninxp  38378  cossssid3  38460  dmqs1cosscnvepreseq  38654  disjxrnres5  38739  dmqsblocks  38845  islshpat  39010  lkr0f  39087  lshpsmreu  39102  cvrnbtwn4  39272  ishlat2  39346  islvol5  39573  tendoeq2  40768  dibelval3  41141  mapdpglem3  41669  hdmapglem7a  41921  4rexfrabdioph  42786  dford4  43018  fgraphopab  43192  onsupmaxb  43228  tfsconcatlem  43325  ifpim123g  43489  ifpbibib  43499  rp-isfinite6  43507  elrncard  43526  undmrnresiss  43593  cnvssco  43595  iunrelexpuztr  43708  dffrege115  43967  brco2f1o  44021  ntrneiiso  44080  ismnuprim  44283  undisjrab  44295  radcnvrat  44303  opelopab4  44541  2sb5nd  44550  un2122  44779  uunT12p4  44792  2sb5ndVD  44899  2sb5ndALT  44921  ndisj2  45045  ssabf  45094  abssf  45106  fourierdlem42  46147  smflimlem4  46772  aiotaexaiotaiota  47095  ndmaovcom  47206  dmafv2rnb  47230  afv2ndeffv0  47261  modm1p1ne  47371  0nelsetpreimafv  47391  usgrexmpl2nb0  48022  usgrexmpl2nb1  48023  gpg5nbgrvtx03starlem1  48059  gpg5nbgrvtx03starlem2  48060  gpg5nbgrvtx03starlem3  48061  gpg5nbgrvtx13starlem1  48062  gpg5nbgrvtx13starlem2  48063  gpg5nbgrvtx13starlem3  48064  pgnbgreunbgrlem2lem2  48105  eliunxp2  48322  pgrpgt2nabl  48354  islindeps  48442  lindslinindsimp1  48446  lindslinindsimp2  48452