Theorem bitr3i 279

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

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  3bitrri  300  3bitr3i  303  3bitr3ri  304  xchnxbi  334  an13  654  anandi  683  anandir  684  orordi  935  orordir  936  ianor  990  trunantru  1589  falnanfal  1592  had0  1612  nic-axALT  1682  equsexvw  2013  sbiedvw  2108  sbievw2  2111  cbvsbv  2113  sbal  2182  sbco4OLD  2187  sb6a  2272  sbiedw  2327  sbied  2513  sbidm  2520  mo  2571  2eu6  2662  cbvab  2813  nabbib  3039  rexcom4a  3271  abv  3445  ceqsex  3480  ceqsexv  3481  spc2ed  3540  clel2g  3598  2reuswap  3688  2reuswap2  3689  2reu5  3700  2rmoswap  3703  nfcdeq  3719  sbcid  3741  sbcco2  3751  sbc7  3756  sbcie2g  3764  eqsbc1  3770  sbcralt  3805  cbvralcsf  3874  cbvrabcsf  3877  abss  3995  ssab  3996  raldifb  4081  difrab  4248  euelss  4262  sbccsb  4366  vdif0  4399  difrab0eq  4400  ssunsn2  4760  sspr  4768  sstp  4769  uniintsn  4917  brab1  5122  unopab  5154  axrep5  5209  axrep6OLD  5211  intexab  5276  reusv2lem4  5332  reusv2  5334  elOLD  5380  wefrc  5614  eliunxp  5781  ralxp  5785  rexxp  5786  opelco  5815  reldm0  5876  resieq  5948  iss  5993  imai  6032  intasym  6071  asymref  6072  codir  6076  poirr2  6080  xpdifid  6122  rninxp  6133  dfpo2  6250  frpoins2fg  6298  ordelord  6335  ordtri3  6349  funopg  6522  fin  6710  f1cnvcnv  6735  funimass4  6894  fnressn  7104  resoprab  7477  mpo2eqb  7491  elrnmpores  7497  ov6g  7523  imaeqexov  7597  imaeqalov  7598  offval  7632  uniuni  7708  dfwe2  7720  orduniorsuc  7773  tfinds2  7807  dfopab2  7996  dfoprab3s  7997  fmpox  8011  fparlem1  8053  fparlem2  8054  ralxp3f  8079  frpoins3xpg  8082  brtpos0  8175  dftpos3  8186  tpostpos  8188  dfrecs3  8305  tz7.48lem  8374  omeu  8514  ercnv  8659  ixp0  8873  xpcomco  8999  xpassen  9003  php  9135  findcard3  9187  ixpfi2  9254  dfsup2  9351  sup0riota  9373  card2on  9463  infeq5i  9552  cnfcom3lem  9619  ssttrcl  9631  ttrcltr  9632  ttrclss  9636  setinds2f  9666  frins2f  9672  r1elss  9725  rankxplim  9798  scott0s  9807  aceq1  10034  dfac5lem1  10040  dfac5lem2  10041  kmlem3  10070  kmlem8  10075  kmlem16  10083  djuinf  10106  cflemOLD  10163  cf0  10168  alephval2  10491  fpwwe2lem7  10556  fpwwe2lem11  10560  rankcf  10696  r1tskina  10701  wfgru  10735  genpass  10928  psslinpr  10950  ltpsrpr  11028  addeq0  11569  infm3  12110  nnwos  12860  ioo0  13318  ico0  13339  ioc0  13340  icc0  13341  elfz2nn0  13567  elfzmlbp  13588  sqeqori  14171  hashgt12el  14379  hashgt12el2  14380  cshwidxmod  14760  clim0  15463  divalglem6  16362  ncoprmlnprm  16693  pceu  16812  prmreclem2  16883  cshwshash  17070  xpscf  17524  acsfn2  17624  invsym2  17725  cat1  18059  pospo  18304  issubmndb  18768  f1omvdco3  19418  psgnunilem5  19463  efgrelexlemb  19719  gexex  19822  srgrmhm  20197  isdomn3  20690  isdomn4r  20694  lssne0  20944  islindf4  21816  opsrtoslem1  22034  opsrtoslem2  22035  mdetunilem8  22605  cpmatmcllem  22704  pmatcollpw2lem  22763  ntreq0  23063  ordtrest2lem  23189  ist0-3  23331  ist1-2  23333  ist1-3  23335  cmpfi  23394  2ndcctbss  23441  ptbasfi  23567  ptcnplem  23607  hausdiag  23631  hauseqlcld  23632  cnmptcom  23664  txflf  23992  tgphaus  24103  metrest  24510  iccpnfcnv  24932  bcth3  25319  dyadmax  25586  vitalilem2  25597  vitalilem3  25598  mbfimaopnlem  25643  itg2leub  25722  dvres2  25900  ellogdm  26624  reasinsin  26881  leibpilem2  26926  ftalem3  27059  dchreq  27242  bdayimaon  27677  noetainflem4  27724  cuteq1  27829  addsprop  27988  leadds1  28001  negsprop  28047  mulsprop  28142  mulsuniflem  28161  addsdilem1  28163  addsdilem2  28164  mulsasslem1  28175  mulsasslem2  28176  precsexlem10  28228  precsexlem11  28229  onnolt  28278  bdayn0p1  28381  legso  28687  outpasch  28843  axcontlem2  29054  incistruhgr  29168  nbgrel  29429  usgr2pth0  29853  rusgrnumwwlkslem  30060  frgr3v  30365  4cycl2vnunb  30380  frgrncvvdeqlem2  30390  lnon0  30889  spansncvi  31743  pjssmii  31772  nmlnopgt0i  32088  largei  32358  cvexchlem  32459  xfree  32535  nmo  32579  reuxfrdf  32580  fpwrelmapffslem  32826  eliccioo  33011  1arithidom  33630  ufdprmidl  33634  qtophaus  34030  ordtrest2NEWlem  34116  ordtconnlem1  34118  xrge0iifcnv  34127  xrge0iifiso  34129  xrge0iifhom  34131  cntnevol  34422  eulerpartlemgh  34572  ballotlem7  34730  signswch  34755  bnj446  34913  bnj563  34939  bnj110  35053  bnj153  35075  bnj864  35117  bnj865  35118  bnj849  35120  bnj929  35131  bnj1110  35177  fineqvac  35310  axregs  35333  cusgr3cyclex  35377  derang0  35410  iccllysconn  35491  cvmsss2  35515  satf0op  35618  elmrsubrn  35761  rexxfr3dALT  35880  quad3  35911  axacprim  35948  dftr6  35992  elintfv  36006  opelco3  36016  elima4  36017  elpotr  36020  wzel  36063  elfuns  36154  dfiota3  36162  brimg  36176  imagesset  36194  lineunray  36388  ellines  36393  hfninf  36427  in-ax8  36465  ss-ax8  36466  bj-df-sb  37003  bj-elabtru  37240  bj-snglc  37335  bj-mpomptALT  37490  bj-elid7  37544  bj-imdirco  37563  nlpineqsn  37783  curf  37978  tan2h  37992  poimirlem26  38026  poimirlem27  38027  poimirlem30  38030  poimirlem32  38032  poimir  38033  ovoliunnfl  38042  voliunnfl  38044  ftc1anc  38081  inixp  38108  heibor1lem  38189  csbcom2fi  38508  tsna1  38524  anan  38615  brid  38692  ref5  38699  idinxpssinxp4  38706  iss2  38724  raldmqseu  38745  xrninxp  38795  cossssid3  38939  dmqs1cosscnvepreseq  39127  disjxrnres5  39227  dmqsblocks  39347  islshpat  39522  lkr0f  39599  lshpsmreu  39614  cvrnbtwn4  39784  ishlat2  39858  islvol5  40084  tendoeq2  41279  dibelval3  41652  mapdpglem3  42180  hdmapglem7a  42432  4rexfrabdioph  43256  dford4  43487  fgraphopab  43661  onsupmaxb  43697  tfsconcatlem  43794  ifpim123g  43957  ifpbibib  43967  rp-isfinite6  43975  elrncard  43994  undmrnresiss  44061  cnvssco  44063  iunrelexpuztr  44176  dffrege115  44435  brco2f1o  44489  ntrneiiso  44548  ismnuprim  44751  undisjrab  44763  radcnvrat  44771  opelopab4  45008  2sb5nd  45017  un2122  45246  uunT12p4  45259  2sb5ndVD  45366  2sb5ndALT  45388  ndisj2  45512  ssabf  45559  abssf  45571  fourierdlem42  46604  smflimlem4  47229  aiotaexaiotaiota  47569  ndmaovcom  47680  dmafv2rnb  47704  afv2ndeffv0  47735  modm1p1ne  47851  0nelsetpreimafv  47877  usgrexmpl2nb0  48534  usgrexmpl2nb1  48535  gpg5nbgrvtx03starlem1  48571  gpg5nbgrvtx03starlem2  48572  gpg5nbgrvtx03starlem3  48573  gpg5nbgrvtx13starlem1  48574  gpg5nbgrvtx13starlem2  48575  gpg5nbgrvtx13starlem3  48576  pgnbgreunbgrlem2lem2  48618  gpg5edgnedg  48633  eliunxp2  48837  pgrpgt2nabl  48869  islindeps  48956  lindslinindsimp1  48960  lindslinindsimp2  48966