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  1582  falnanfal  1585  had0  1605  nic-axALT  1675  equsexvw  2006  sbiedvw  2100  sbievw2  2103  cbvsbv  2105  sbal  2174  sbco4OLD  2180  sb6a  2263  sbiedw  2319  sbied  2505  sbidm  2512  mo  2562  2mosOLD  2647  2eu6  2654  cbvab  2805  nabbib  3033  rexcom4a  3264  abv  3450  ceqsex  3487  ceqsexv  3488  spc2ed  3553  clel2g  3611  2reuswap  3702  2reuswap2  3703  2reu5  3714  2rmoswap  3717  nfcdeq  3733  sbcid  3755  sbcco2  3765  sbc7  3770  sbcie2g  3779  eqsbc1  3785  sbcralt  3820  cbvralcsf  3889  cbvrabcsf  3892  abss  4012  ssab  4013  raldifb  4100  difrab  4269  euelss  4283  sbccsb  4387  vdif0  4420  difrab0eq  4421  ssunsn2  4780  sspr  4788  sstp  4789  uniintsn  4937  brab1  5143  unopab  5175  axrep5  5229  axrep6OLD  5231  intexab  5288  reusv2lem4  5343  reusv2  5345  el  5384  wefrc  5615  eliunxp  5784  ralxp  5788  rexxp  5789  opelco  5818  reldm0  5875  resieq  5946  iss  5991  imai  6030  intasym  6069  asymref  6070  codir  6074  poirr2  6078  xpdifid  6123  rninxp  6134  dfpo2  6251  frpoins2fg  6299  ordelord  6336  ordtri3  6350  funopg  6523  fin  6711  f1cnvcnv  6736  funimass4  6895  fnressn  7100  resoprab  7473  mpo2eqb  7487  elrnmpores  7493  ov6g  7519  imaeqexov  7593  imaeqalov  7594  offval  7628  uniuni  7704  dfwe2  7716  orduniorsuc  7769  tfinds2  7803  dfopab2  7993  dfoprab3s  7994  fmpox  8008  fparlem1  8051  fparlem2  8052  ralxp3f  8076  frpoins3xpg  8079  brtpos0  8172  dftpos3  8183  tpostpos  8185  dfrecs3  8301  tz7.48lem  8369  omeu  8509  ercnv  8652  ixp0  8864  xpcomco  8990  xpassen  8994  php  9126  findcard3  9177  ixpfi2  9244  dfsup2  9338  sup0riota  9360  card2on  9450  infeq5i  9536  cnfcom3lem  9603  ssttrcl  9615  ttrcltr  9616  ttrclss  9620  setinds2f  9650  frins2f  9656  r1elss  9709  rankxplim  9782  scott0s  9791  aceq1  10018  dfac5lem1  10024  dfac5lem2  10025  kmlem3  10054  kmlem8  10059  kmlem16  10067  djuinf  10090  cflemOLD  10147  cf0  10152  alephval2  10473  fpwwe2lem7  10538  fpwwe2lem11  10542  rankcf  10678  r1tskina  10683  wfgru  10717  genpass  10910  psslinpr  10932  ltpsrpr  11010  addeq0  11550  infm3  12091  nnwos  12823  ioo0  13280  ico0  13301  ioc0  13302  icc0  13303  elfz2nn0  13528  elfzmlbp  13549  sqeqori  14131  hashgt12el  14339  hashgt12el2  14340  cshwidxmod  14720  clim0  15423  divalglem6  16319  ncoprmlnprm  16649  pceu  16768  prmreclem2  16839  cshwshash  17026  xpscf  17479  acsfn2  17579  invsym2  17680  cat1  18014  pospo  18259  issubmndb  18723  f1omvdco3  19371  psgnunilem5  19416  efgrelexlemb  19672  gexex  19775  srgrmhm  20150  isdomn3  20640  isdomn4r  20644  lssne0  20894  islindf4  21785  opsrtoslem1  22000  opsrtoslem2  22001  mdetunilem8  22544  cpmatmcllem  22643  pmatcollpw2lem  22702  ntreq0  23002  ordtrest2lem  23128  ist0-3  23270  ist1-2  23272  ist1-3  23274  cmpfi  23333  2ndcctbss  23380  ptbasfi  23506  ptcnplem  23546  hausdiag  23570  hauseqlcld  23571  cnmptcom  23603  txflf  23931  tgphaus  24042  metrest  24449  iccpnfcnv  24879  bcth3  25268  dyadmax  25536  vitalilem2  25547  vitalilem3  25548  mbfimaopnlem  25593  itg2leub  25672  dvres2  25850  ellogdm  26585  reasinsin  26843  leibpilem2  26888  ftalem3  27022  dchreq  27206  bdayimaon  27642  noetainflem4  27689  cuteq1  27788  addsprop  27929  sleadd1  27942  negsprop  27987  mulsprop  28079  mulsuniflem  28098  addsdilem1  28100  addsdilem2  28101  mulsasslem1  28112  mulsasslem2  28113  precsexlem10  28164  precsexlem11  28165  onnolt  28213  bdayn0p1  28304  legso  28587  outpasch  28743  axcontlem2  28954  incistruhgr  29068  nbgrel  29329  usgr2pth0  29754  rusgrnumwwlkslem  29961  frgr3v  30266  4cycl2vnunb  30281  frgrncvvdeqlem2  30291  lnon0  30789  spansncvi  31643  pjssmii  31672  nmlnopgt0i  31988  largei  32258  cvexchlem  32359  xfree  32435  nmo  32480  reuxfrdf  32481  fpwrelmapffslem  32726  eliccioo  32922  1arithidom  33513  ufdprmidl  33517  qtophaus  33860  ordtrest2NEWlem  33946  ordtconnlem1  33948  xrge0iifcnv  33957  xrge0iifiso  33959  xrge0iifhom  33961  cntnevol  34252  eulerpartlemgh  34402  ballotlem7  34560  signswch  34585  bnj446  34740  bnj563  34766  bnj110  34881  bnj153  34903  bnj864  34945  bnj865  34946  bnj849  34948  bnj929  34959  bnj1110  35005  fineqvac  35150  axregs  35156  cusgr3cyclex  35191  derang0  35224  iccllysconn  35305  cvmsss2  35329  satf0op  35432  elmrsubrn  35575  rexxfr3dALT  35694  quad3  35725  axacprim  35762  dftr6  35806  elintfv  35820  opelco3  35830  elima4  35831  elpotr  35834  wzel  35877  elfuns  35968  dfiota3  35976  brimg  35990  imagesset  36008  lineunray  36202  ellines  36207  hfninf  36241  in-ax8  36279  ss-ax8  36280  bj-elabtru  36929  bj-snglc  37024  bj-mpomptALT  37174  bj-elid7  37226  bj-imdirco  37245  nlpineqsn  37463  curf  37648  tan2h  37662  poimirlem26  37696  poimirlem27  37697  poimirlem30  37700  poimirlem32  37702  poimir  37703  ovoliunnfl  37712  voliunnfl  37714  ftc1anc  37751  inixp  37778  heibor1lem  37859  csbcom2fi  38178  tsna1  38194  anan  38280  brid  38354  ref5  38361  idinxpssinxp4  38368  iss2  38386  xrninxp  38449  cossssid3  38581  dmqs1cosscnvepreseq  38770  disjxrnres5  38855  dmqsblocks  38961  islshpat  39126  lkr0f  39203  lshpsmreu  39218  cvrnbtwn4  39388  ishlat2  39462  islvol5  39688  tendoeq2  40883  dibelval3  41256  mapdpglem3  41784  hdmapglem7a  42036  4rexfrabdioph  42905  dford4  43136  fgraphopab  43310  onsupmaxb  43346  tfsconcatlem  43443  ifpim123g  43607  ifpbibib  43617  rp-isfinite6  43625  elrncard  43644  undmrnresiss  43711  cnvssco  43713  iunrelexpuztr  43826  dffrege115  44085  brco2f1o  44139  ntrneiiso  44198  ismnuprim  44401  undisjrab  44413  radcnvrat  44421  opelopab4  44658  2sb5nd  44667  un2122  44896  uunT12p4  44909  2sb5ndVD  45016  2sb5ndALT  45038  ndisj2  45162  ssabf  45211  abssf  45223  fourierdlem42  46261  smflimlem4  46886  aiotaexaiotaiota  47208  ndmaovcom  47319  dmafv2rnb  47343  afv2ndeffv0  47374  modm1p1ne  47484  0nelsetpreimafv  47504  usgrexmpl2nb0  48145  usgrexmpl2nb1  48146  gpg5nbgrvtx03starlem1  48182  gpg5nbgrvtx03starlem2  48183  gpg5nbgrvtx03starlem3  48184  gpg5nbgrvtx13starlem1  48185  gpg5nbgrvtx13starlem2  48186  gpg5nbgrvtx13starlem3  48187  pgnbgreunbgrlem2lem2  48229  gpg5edgnedg  48244  eliunxp2  48448  pgrpgt2nabl  48480  islindeps  48568  lindslinindsimp1  48572  lindslinindsimp2  48578