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  2098  sbievw2  2101  cbvsbv  2103  sbal  2172  sbco4OLD  2178  sb6a  2261  sbiedw  2317  sbied  2503  sbidm  2510  mo  2560  2mosOLD  2645  2eu6  2652  cbvab  2803  nabbib  3031  rexcom4a  3262  abv  3448  ceqsex  3485  ceqsexv  3486  spc2ed  3551  clel2g  3609  2reuswap  3700  2reuswap2  3701  2reu5  3712  2rmoswap  3715  nfcdeq  3731  sbcid  3753  sbcco2  3763  sbc7  3768  sbcie2g  3777  eqsbc1  3783  sbcralt  3818  cbvralcsf  3887  cbvrabcsf  3890  abss  4009  ssab  4010  raldifb  4096  difrab  4265  euelss  4279  sbccsb  4383  vdif0  4416  difrab0eq  4417  ssunsn2  4776  sspr  4784  sstp  4785  uniintsn  4933  brab1  5137  unopab  5169  axrep5  5223  axrep6OLD  5225  intexab  5282  reusv2lem4  5337  reusv2  5339  el  5378  wefrc  5608  eliunxp  5776  ralxp  5780  rexxp  5781  opelco  5810  reldm0  5867  resieq  5938  iss  5983  imai  6022  intasym  6061  asymref  6062  codir  6066  poirr2  6070  xpdifid  6115  rninxp  6126  dfpo2  6243  frpoins2fg  6291  ordelord  6328  ordtri3  6342  funopg  6515  fin  6703  f1cnvcnv  6728  funimass4  6886  fnressn  7091  resoprab  7464  mpo2eqb  7478  elrnmpores  7484  ov6g  7510  imaeqexov  7584  imaeqalov  7585  offval  7619  uniuni  7695  dfwe2  7707  orduniorsuc  7760  tfinds2  7794  dfopab2  7984  dfoprab3s  7985  fmpox  7999  fparlem1  8042  fparlem2  8043  ralxp3f  8067  frpoins3xpg  8070  brtpos0  8163  dftpos3  8174  tpostpos  8176  dfrecs3  8292  tz7.48lem  8360  omeu  8500  ercnv  8643  ixp0  8855  xpcomco  8980  xpassen  8984  php  9116  findcard3  9167  ixpfi2  9234  dfsup2  9328  sup0riota  9350  card2on  9440  infeq5i  9526  cnfcom3lem  9593  ssttrcl  9605  ttrcltr  9606  ttrclss  9610  setinds2f  9640  frins2f  9646  r1elss  9699  rankxplim  9772  scott0s  9781  aceq1  10008  dfac5lem1  10014  dfac5lem2  10015  kmlem3  10044  kmlem8  10049  kmlem16  10057  djuinf  10080  cflemOLD  10137  cf0  10142  alephval2  10463  fpwwe2lem7  10528  fpwwe2lem11  10532  rankcf  10668  r1tskina  10673  wfgru  10707  genpass  10900  psslinpr  10922  ltpsrpr  11000  addeq0  11540  infm3  12081  nnwos  12813  ioo0  13270  ico0  13291  ioc0  13292  icc0  13293  elfz2nn0  13518  elfzmlbp  13539  sqeqori  14121  hashgt12el  14329  hashgt12el2  14330  cshwidxmod  14710  clim0  15413  divalglem6  16309  ncoprmlnprm  16639  pceu  16758  prmreclem2  16829  cshwshash  17016  xpscf  17469  acsfn2  17569  invsym2  17670  cat1  18004  pospo  18249  issubmndb  18713  f1omvdco3  19361  psgnunilem5  19406  efgrelexlemb  19662  gexex  19765  srgrmhm  20140  isdomn3  20630  isdomn4r  20634  lssne0  20884  islindf4  21775  opsrtoslem1  21990  opsrtoslem2  21991  mdetunilem8  22534  cpmatmcllem  22633  pmatcollpw2lem  22692  ntreq0  22992  ordtrest2lem  23118  ist0-3  23260  ist1-2  23262  ist1-3  23264  cmpfi  23323  2ndcctbss  23370  ptbasfi  23496  ptcnplem  23536  hausdiag  23560  hauseqlcld  23561  cnmptcom  23593  txflf  23921  tgphaus  24032  metrest  24439  iccpnfcnv  24869  bcth3  25258  dyadmax  25526  vitalilem2  25537  vitalilem3  25538  mbfimaopnlem  25583  itg2leub  25662  dvres2  25840  ellogdm  26575  reasinsin  26833  leibpilem2  26878  ftalem3  27012  dchreq  27196  bdayimaon  27632  noetainflem4  27679  cuteq1  27778  addsprop  27919  sleadd1  27932  negsprop  27977  mulsprop  28069  mulsuniflem  28088  addsdilem1  28090  addsdilem2  28091  mulsasslem1  28102  mulsasslem2  28103  precsexlem10  28154  precsexlem11  28155  onnolt  28203  bdayn0p1  28294  legso  28577  outpasch  28733  axcontlem2  28943  incistruhgr  29057  nbgrel  29318  usgr2pth0  29743  rusgrnumwwlkslem  29950  frgr3v  30255  4cycl2vnunb  30270  frgrncvvdeqlem2  30280  lnon0  30778  spansncvi  31632  pjssmii  31661  nmlnopgt0i  31977  largei  32247  cvexchlem  32348  xfree  32424  nmo  32469  reuxfrdf  32470  fpwrelmapffslem  32715  eliccioo  32911  1arithidom  33502  ufdprmidl  33506  qtophaus  33849  ordtrest2NEWlem  33935  ordtconnlem1  33937  xrge0iifcnv  33946  xrge0iifiso  33948  xrge0iifhom  33950  cntnevol  34241  eulerpartlemgh  34391  ballotlem7  34549  signswch  34574  bnj446  34729  bnj563  34755  bnj110  34870  bnj153  34892  bnj864  34934  bnj865  34935  bnj849  34937  bnj929  34948  bnj1110  34994  fineqvac  35139  axregs  35145  cusgr3cyclex  35180  derang0  35213  iccllysconn  35294  cvmsss2  35318  satf0op  35421  elmrsubrn  35564  rexxfr3dALT  35683  quad3  35714  axacprim  35751  dftr6  35795  elintfv  35809  opelco3  35819  elima4  35820  elpotr  35823  wzel  35866  elfuns  35957  dfiota3  35965  brimg  35979  imagesset  35997  lineunray  36191  ellines  36196  hfninf  36230  in-ax8  36268  ss-ax8  36269  bj-elabtru  36918  bj-snglc  37013  bj-mpomptALT  37163  bj-elid7  37215  bj-imdirco  37234  nlpineqsn  37452  curf  37637  tan2h  37651  poimirlem26  37685  poimirlem27  37686  poimirlem30  37689  poimirlem32  37691  poimir  37692  ovoliunnfl  37701  voliunnfl  37703  ftc1anc  37740  inixp  37767  heibor1lem  37848  csbcom2fi  38167  tsna1  38183  anan  38269  brid  38343  ref5  38350  idinxpssinxp4  38357  iss2  38375  xrninxp  38438  cossssid3  38570  dmqs1cosscnvepreseq  38759  disjxrnres5  38844  dmqsblocks  38950  islshpat  39115  lkr0f  39192  lshpsmreu  39207  cvrnbtwn4  39377  ishlat2  39451  islvol5  39677  tendoeq2  40872  dibelval3  41245  mapdpglem3  41773  hdmapglem7a  42025  4rexfrabdioph  42890  dford4  43121  fgraphopab  43295  onsupmaxb  43331  tfsconcatlem  43428  ifpim123g  43592  ifpbibib  43602  rp-isfinite6  43610  elrncard  43629  undmrnresiss  43696  cnvssco  43698  iunrelexpuztr  43811  dffrege115  44070  brco2f1o  44124  ntrneiiso  44183  ismnuprim  44386  undisjrab  44398  radcnvrat  44406  opelopab4  44643  2sb5nd  44652  un2122  44881  uunT12p4  44894  2sb5ndVD  45001  2sb5ndALT  45023  ndisj2  45147  ssabf  45196  abssf  45208  fourierdlem42  46246  smflimlem4  46871  aiotaexaiotaiota  47193  ndmaovcom  47304  dmafv2rnb  47328  afv2ndeffv0  47359  modm1p1ne  47469  0nelsetpreimafv  47489  usgrexmpl2nb0  48130  usgrexmpl2nb1  48131  gpg5nbgrvtx03starlem1  48167  gpg5nbgrvtx03starlem2  48168  gpg5nbgrvtx03starlem3  48169  gpg5nbgrvtx13starlem1  48170  gpg5nbgrvtx13starlem2  48171  gpg5nbgrvtx13starlem3  48172  pgnbgreunbgrlem2lem2  48214  gpg5edgnedg  48229  eliunxp2  48433  pgrpgt2nabl  48465  islindeps  48553  lindslinindsimp1  48557  lindslinindsimp2  48563