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  1579  falnanfal  1582  had0  1602  nic-axALT  1672  equsexvw  2003  sbiedvw  2094  sbievw2  2097  cbvsbv  2099  sbal  2168  sbco4OLD  2174  sb6a  2257  sbiedw  2316  sbied  2507  sbidm  2514  mo  2564  2mosOLD  2649  2eu6  2656  cbvab  2813  nabbib  3044  2ralorOLD  3231  rexcom4a  3291  abv  3491  ceqsex  3529  ceqsexv  3531  spc2ed  3602  clel2g  3660  2reuswap  3756  2reuswap2  3757  2reu5  3768  2rmoswap  3771  nfcdeq  3787  sbcid  3809  sbcco2  3819  sbc7  3825  sbcie2g  3835  eqsbc1  3842  sbcralt  3882  cbvralcsf  3954  cbvrabcsf  3957  abss  4074  ssab  4075  raldifb  4160  difrab  4325  euelss  4339  vn0  4352  sbccsb  4443  vdif0  4476  difrab0eq  4477  ssunsn2  4833  sspr  4841  sstp  4842  uniintsn  4991  brab1  5197  unopab  5231  axrep5  5294  axrep6OLD  5296  intexab  5353  reusv2lem4  5408  reusv2  5410  el  5449  wefrc  5684  eliunxp  5852  ralxp  5856  rexxp  5857  opelco  5886  reldm0  5942  resieq  6012  iss  6057  imai  6096  cnvsymOLDOLD  6139  intasym  6140  asymref  6141  codir  6145  poirr2  6149  xpdifid  6193  rninxp  6204  dfpo2  6321  frpoins2fg  6370  tz6.26OLD  6374  wfis2fgOLD  6383  ordelord  6411  ordtri3  6425  dffun3OLD  6581  funopg  6605  fin  6793  f1cnvcnv  6818  funimass4  6977  fnressn  7182  resoprab  7555  mpo2eqb  7569  elrnmpores  7575  ov6g  7601  imaeqexov  7675  imaeqalov  7676  offval  7710  uniuni  7785  dfwe2  7797  orduniorsuc  7854  tfinds2  7889  dfopab2  8082  dfoprab3s  8083  fmpox  8097  fparlem1  8142  fparlem2  8143  ralxp3f  8167  frpoins3xpg  8170  brtpos0  8263  dftpos3  8274  tpostpos  8276  dfrecs3  8417  dfrecs3OLD  8418  tz7.48lem  8486  omeu  8628  ercnv  8771  ixp0  8976  xpcomco  9107  xpassen  9111  php  9251  phpOLD  9263  findcard3  9322  findcard3OLD  9323  ixpfi2  9394  dfsup2  9488  sup0riota  9509  card2on  9598  infeq5i  9680  cnfcom3lem  9747  ssttrcl  9759  ttrcltr  9760  ttrclss  9764  frins2f  9797  r1elss  9850  rankxplim  9923  scott0s  9932  aceq1  10161  dfac5lem1  10167  dfac5lem2  10168  kmlem3  10197  kmlem8  10202  kmlem16  10210  djuinf  10233  cflemOLD  10290  cf0  10295  alephval2  10616  fpwwe2lem7  10681  fpwwe2lem11  10685  rankcf  10821  r1tskina  10826  wfgru  10860  genpass  11053  psslinpr  11075  ltpsrpr  11153  addeq0  11690  infm3  12231  nnwos  12961  ioo0  13415  ico0  13436  ioc0  13437  icc0  13438  elfz2nn0  13661  elfzmlbp  13682  sqeqori  14256  hashgt12el  14464  hashgt12el2  14465  cshwidxmod  14844  clim0  15545  divalglem6  16438  ncoprmlnprm  16768  pceu  16886  prmreclem2  16957  cshwshash  17145  xpscf  17618  acsfn2  17714  invsym2  17817  cat1  18157  pospo  18409  issubmndb  18837  f1omvdco3  19488  psgnunilem5  19533  efgrelexlemb  19789  gexex  19892  srgrmhm  20246  isdomn3  20738  isdomn4r  20742  lssne0  20973  islindf4  21882  opsrtoslem1  22103  opsrtoslem2  22104  mdetunilem8  22647  cpmatmcllem  22746  pmatcollpw2lem  22805  ntreq0  23107  ordtrest2lem  23233  ist0-3  23375  ist1-2  23377  ist1-3  23379  cmpfi  23438  2ndcctbss  23485  ptbasfi  23611  ptcnplem  23651  hausdiag  23675  hauseqlcld  23676  cnmptcom  23708  txflf  24036  tgphaus  24147  metrest  24559  iccpnfcnv  24997  bcth3  25387  dyadmax  25655  vitalilem2  25666  vitalilem3  25667  mbfimaopnlem  25712  itg2leub  25792  dvres2  25970  ellogdm  26704  reasinsin  26962  leibpilem2  27007  ftalem3  27141  dchreq  27325  bdayimaon  27761  noetainflem4  27808  cuteq1  27901  addsprop  28032  sleadd1  28045  negsprop  28090  mulsprop  28179  mulsuniflem  28198  addsdilem1  28200  addsdilem2  28201  mulsasslem1  28212  mulsasslem2  28213  precsexlem10  28263  precsexlem11  28264  legso  28630  outpasch  28786  axcontlem2  29003  incistruhgr  29119  nbgrel  29380  usgr2pth0  29808  rusgrnumwwlkslem  30012  frgr3v  30317  4cycl2vnunb  30332  frgrncvvdeqlem2  30342  lnon0  30840  spansncvi  31694  pjssmii  31723  nmlnopgt0i  32039  largei  32309  cvexchlem  32410  xfree  32486  nmo  32531  reuxfrdf  32532  fpwrelmapffslem  32763  eliccioo  32911  1arithidom  33558  ufdprmidl  33562  qtophaus  33810  ordtrest2NEWlem  33896  ordtconnlem1  33898  xrge0iifcnv  33907  xrge0iifiso  33909  xrge0iifhom  33911  cntnevol  34222  eulerpartlemgh  34373  ballotlem7  34530  signswch  34568  bnj446  34723  bnj563  34749  bnj110  34864  bnj153  34886  bnj864  34928  bnj865  34929  bnj849  34931  bnj929  34942  bnj1110  34988  fineqvac  35103  cusgr3cyclex  35133  derang0  35166  iccllysconn  35247  cvmsss2  35271  satf0op  35374  elmrsubrn  35517  rexxfr3dALT  35636  quad3  35667  axacprim  35699  dftr6  35743  elintfv  35758  opelco3  35768  elima4  35769  setinds2f  35773  elpotr  35775  wzel  35818  elfuns  35909  dfiota3  35917  brimg  35931  imagesset  35947  lineunray  36141  ellines  36146  hfninf  36180  in-ax8  36219  ss-ax8  36220  bj-elabtru  36869  bj-snglc  36964  bj-mpomptALT  37114  bj-elid7  37166  bj-imdirco  37185  nlpineqsn  37403  curf  37597  tan2h  37611  poimirlem26  37645  poimirlem27  37646  poimirlem30  37649  poimirlem32  37651  poimir  37652  ovoliunnfl  37661  voliunnfl  37663  ftc1anc  37700  inixp  37727  heibor1lem  37808  csbcom2fi  38127  tsna1  38143  anan  38222  brid  38300  ref5  38307  idinxpssinxp4  38314  iss2  38338  xrninxp  38386  cossssid3  38463  dmqs1cosscnvepreseq  38656  disjxrnres5  38741  islshpat  39011  lkr0f  39088  lshpsmreu  39103  cvrnbtwn4  39273  ishlat2  39347  islvol5  39574  tendoeq2  40769  dibelval3  41142  mapdpglem3  41670  hdmapglem7a  41922  4rexfrabdioph  42800  dford4  43032  fgraphopab  43206  onsupmaxb  43242  tfsconcatlem  43340  ifpim123g  43504  ifpbibib  43514  rp-isfinite6  43522  elrncard  43541  undmrnresiss  43608  cnvssco  43610  iunrelexpuztr  43723  dffrege115  43982  brco2f1o  44036  ntrneiiso  44095  ismnuprim  44304  undisjrab  44316  radcnvrat  44324  opelopab4  44562  2sb5nd  44571  un2122  44801  uunT12p4  44814  2sb5ndVD  44921  2sb5ndALT  44943  ndisj2  45004  ssabf  45053  abssf  45065  fourierdlem42  46116  smflimlem4  46741  aiotaexaiotaiota  47055  ndmaovcom  47166  dmafv2rnb  47190  afv2ndeffv0  47221  0nelsetpreimafv  47326  usgrexmpl2nb0  47939  usgrexmpl2nb1  47940  gpg5nbgrvtx03starlem1  47973  gpg5nbgrvtx03starlem2  47974  gpg5nbgrvtx03starlem3  47975  gpg5nbgrvtx13starlem1  47976  gpg5nbgrvtx13starlem2  47977  gpg5nbgrvtx13starlem3  47978  eliunxp2  48200  pgrpgt2nabl  48232  islindeps  48320  lindslinindsimp1  48324  lindslinindsimp2  48330