Theorem bitr3i 280

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

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3bitrri  301  3bitr3i  304  3bitr3ri  305  xchnxbi  335  an13  660  anandi  689  anandir  690  orordi  942  orordir  943  ianor  997  trunantru  1611  falnanfal  1614  had0OLD  1636  nic-axALT  1707  equsexvw  2040  sbiedvw  2134  sbievw2  2137  cbvsbv  2139  sbal  2209  sb6a  2296  sbiedw  2350  sbied  2535  sbidm  2542  mo  2593  2eu6  2684  cbvab  2836  nabbib  3064  rexcom4a  3296  abv  3466  ceqsex  3501  ceqsexv  3502  spc2ed  3559  clel2g  3616  2reuswap  3707  2reuswap2  3708  2reu5  3719  2rmoswap  3722  nfcdeq  3738  sbcid  3759  sbcco2  3769  sbc7  3774  sbcie2g  3782  eqsbc1  3788  sbcralt  3823  cbvralcsf  3893  cbvrabcsf  3896  abss  3990  ssab  3991  raldifb  4088  difrab  4266  euelss  4280  sbccsb  4397  vdif0  4425  difrab0eq  4426  ssunsn2  4786  sspr  4793  sstp  4794  uniintsn  4948  brab1  5156  unopab  5188  axrep5  5242  intexab  5311  reusv2lem4  5367  reusv2  5369  el.OLD  5411  wefrc  5649  eliunxp  5820  ralxp  5824  rexxp  5825  opelco  5856  reldm0  5917  resieq  5992  iss  6039  imai  6084  intasym  6121  asymref  6122  codir  6126  poirr2  6130  xpdifid  6171  rninxp  6183  dfpo2  6317  frpoins2fg  6365  ordelord  6402  ordtri3  6417  funopg  6594  fin  6784  f1cnvcnv  6811  funimass4  6972  fnressn  7186  resoprab  7561  mpo2eqb  7575  elrnmpores  7582  ov6g  7608  imaeqexov  7683  imaeqalov  7684  mpt3mpt  7709  offval  7726  uniuni  7800  dfwe2  7812  orduniorsuc  7865  tfinds2  7899  dfopab2  8088  dfoprab3s  8089  fmpox  8103  fparlem1  8150  fparlem2  8151  ralxp3f  8181  frpoins3xpg  8184  brtpos0  8278  dftpos3  8289  tpostpos  8291  dfrecs3  8408  tz7.48lemOLD  8479  omeu  8621  ercnv  8767  curf  8918  ixp0  8987  xpcomco  9114  xpassen  9118  php  9250  findcard3  9302  ixpfi2  9367  dfsup2  9463  sup0riota  9485  card2on  9575  infeq5i  9664  cnfcom3lem  9731  ssttrcl  9743  ttrcltr  9744  ttrclss  9748  setinds2f  9778  frins2f  9784  r1elss  9841  rankxplim  9923  scott0bs  9971  scott0bsOLD  9972  aceq1  10223  dfac5lem1  10229  dfac5lem2  10230  kmlem3  10258  kmlem8  10263  kmlem16  10271  djuinf  10294  cf0  10355  alephval2  10684  fpwwe2lem7  10749  fpwwe2lem11  10753  rankcf  10889  r1tskina  10894  wfgru  10928  genpass  11121  psslinpr  11143  ltpsrpr  11221  addeq0  11766  infm3  12303  nnwos  13069  ioo0  13528  ico0  13549  ioc0  13550  icc0  13551  elfz2nn0  13779  elfzmlbp  13800  sqeqori  14385  hashgt12el  14594  hashgt12el2  14595  cshwidxmod  14982  clim0  15702  divalglem6  16597  ncoprmlnprm  16933  pceu  17053  prmreclem2  17124  cshwshash  17311  xpscf  17766  acsfn2  17866  invsym2  17967  cat1  18301  pospo  18546  issubmndb  19029  f1omvdco3  19693  psgnunilem5  19738  efgrelexlemb  19994  gexex  20097  srgrmhm  20478  dfring3  20548  isdomn3  20996  isdomn4r  21000  lssne0  21256  islindf4  22174  opsrtoslem1  22394  opsrtoslem2  22395  mdetunilem8  22964  cpmatmcllem  23066  pmatcollpw2lem  23125  ntreq0  23425  ordtrest2lem  23551  ist0-3  23693  ist1-2  23695  ist1-3  23697  cmpfi  23756  2ndcctbss  23804  ptbasfi  23930  ptcnplem  23970  hausdiag  23994  hauseqlcld  23995  cnmptcom  24027  txflf  24355  tgphaus  24466  metrest  24873  iccpnfcnv  25295  bcth3  25682  dyadmax  25949  vitalilem2  25960  vitalilem3  25961  mbfimaopnlem  26006  itg2leub  26085  dvres2  26262  ellogdm  26997  reasinsin  27254  leibpilem2  27299  ftalem3  27432  dchreq  27615  bdayimaon  28080  noetainflem4  28127  cuteq1  28233  addsprop  28392  leadds1  28405  negsprop  28451  mulsprop  28546  mulsuniflem  28565  addsdilem1  28567  addsdilem2  28568  mulsasslem1  28579  mulsasslem2  28580  precsexlem10  28632  precsexlem11  28633  onnolt  28682  bdayn0p1  28785  legso  29092  outpasch  29263  axcontlem2  29573  incistruhgr  29687  nbgrel  29951  usgr2pth0  30381  rusgrnumwwlkslem  30591  frgr3v  30906  4cycl2vnunb  30921  frgrncvvdeqlem2  30931  lnon0  31430  spansncvi  32284  pjssmii  32313  nmlnopgt0i  32629  largei  32899  cvexchlem  33000  xfree  33118  nmo  33158  reuxfrdf  33159  fpwrelmapffslem  33394  eliccioo  33567  1arithidom  34139  ufdprmidl  34143  qtophaus  34538  ordtrest2NEWlem  34624  ordtconnlem1  34626  xrge0iifcnv  34635  xrge0iifiso  34637  xrge0iifhom  34639  cntnevol  34931  eulerpartlemgh  35080  ballotlem7  35238  signswch  35260  bnj446  35418  bnj563  35444  bnj110  35558  bnj153  35580  bnj864  35622  bnj865  35623  bnj849  35625  bnj929  35636  bnj1110  35682  onrankid  35811  erscottd  35843  fineqvac  35884  axregs  35907  fnlfvk30  36027  fnlfvk3n0  36028  cusgr3cyclex  36068  derang0  36101  iccllysconn  36182  cvmsss2  36206  satf0op  36309  elmrsubrn  36452  rexxfr3dALT  36571  quad3  36602  axacprim  36650  dftr6  36694  elintfv  36708  opelco3  36717  elima4  36718  elpotr  36721  wzel  36764  elfuns  36855  dfiota3  36863  brimg  36877  imagesset  36895  lineunray  37090  ellines  37095  hfninf  37113  in-ax8  37191  ss-ax8  37192  bj-df-sb  37727  bj-elabtru  37964  bj-snglc  38060  bj-mpomptALT  38232  bj-elid7  38284  bj-imdirco  38303  nlpineqsn  38523  tan2h  38727  poimirlem26  38756  poimirlem27  38757  poimirlem30  38760  poimirlem32  38762  poimir  38763  ovoliunnfl  38772  voliunnfl  38774  ftc1anc  38811  inixp  38854  heibor1lem  38935  csbcom2fi  39252  tsna1  39268  anan  39359  brid  39436  ref5  39443  idinxpssinxp4  39450  iss2  39468  raldmqseu  39489  xrninxp  39539  cossssid3  39683  dmqs1cosscnvepreseq  39871  disjxrnres5  39971  dmqsblocks  40091  islshpat  40266  lkr0f  40343  lshpsmreu  40358  cvrnbtwn4  40528  ishlat2  40602  islvol5  40828  tendoeq2  42023  dibelval3  42396  mapdpglem3  42924  hdmapglem7a  43176  4rexfrabdioph  43998  dford4  44229  fgraphopab  44397  onsupmaxb  44433  tfsconcatlem  44530  ifpim123g  44693  ifpbibib  44703  rp-isfinite6  44711  elrncard  44730  undmrnresiss  44796  cnvssco  44798  iunrelexpuztr  44911  dffrege115  45170  brco2f1o  45224  ntrneiiso  45283  ismnuprim  45470  undisjrab  45482  radcnvrat  45490  opelopab4  45725  2sb5nd  45734  un2122  45963  uunT12p4  45976  2sb5ndVD  46083  2sb5ndALT  46105  ndisj2  46273  ssabf  46320  abssf  46332  fourierdlem42  47364  smflimlem4  47989  aiotaexaiotaiota  48369  ndmaovcom  48480  dmafv2rnb  48504  afv2ndeffv0  48535  modm1p1ne  48651  0nelsetpreimafv  48677  usgrexmpl2nb0  49334  usgrexmpl2nb1  49335  gpg5nbgrvtx03starlem1  49371  gpg5nbgrvtx03starlem2  49372  gpg5nbgrvtx03starlem3  49373  gpg5nbgrvtx13starlem1  49374  gpg5nbgrvtx13starlem2  49375  gpg5nbgrvtx13starlem3  49376  pgnbgreunbgrlem2lem2  49418  gpg5edgnedg  49433  eliunxp2  49651  pgrpgt2nabl  49683  islindeps  49770  lindslinindsimp1  49774  lindslinindsimp2  49780