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  659  anandi  688  anandir  689  orordi  941  orordir  942  ianor  996  trunantru  1610  falnanfal  1613  had0  1633  nic-axALT  1703  equsexvw  2034  sbiedvw  2129  sbievw2  2132  cbvsbv  2134  sbal  2203  sbco4OLD  2208  sb6a  2293  sbiedw  2348  sbied  2534  sbidm  2541  mo  2592  2eu6  2683  cbvab  2834  nabbib  3062  rexcom4a  3294  abv  3466  ceqsex  3501  ceqsexv  3502  spc2ed  3559  clel2g  3617  2reuswap  3708  2reuswap2  3709  2reu5  3720  2rmoswap  3723  nfcdeq  3739  sbcid  3760  sbcco2  3770  sbc7  3775  sbcie2g  3783  eqsbc1  3789  sbcralt  3824  cbvralcsf  3894  cbvrabcsf  3897  abss  4015  ssab  4016  raldifb  4102  difrab  4270  euelss  4284  sbccsb  4400  vdif0  4428  difrab0eq  4429  ssunsn2  4792  sspr  4799  sstp  4800  uniintsn  4949  brab1  5158  unopab  5190  axrep5  5245  axrep6OLD  5247  intexab  5315  reusv2lem4  5371  reusv2  5373  el.OLD  5419  wefrc  5654  eliunxp  5822  ralxp  5826  rexxp  5827  opelco  5856  reldm0  5917  resieq  5988  iss  6036  imai  6075  intasym  6114  asymref  6115  codir  6119  poirr2  6123  xpdifid  6164  rninxp  6176  dfpo2  6297  frpoins2fg  6345  ordelord  6382  ordtri3  6397  funopg  6570  fin  6758  f1cnvcnv  6785  funimass4  6945  fnressn  7155  resoprab  7530  mpo2eqb  7544  elrnmpores  7550  ov6g  7576  imaeqexov  7650  imaeqalov  7651  offval  7685  uniuni  7759  dfwe2  7771  orduniorsuc  7824  tfinds2  7858  dfopab2  8047  dfoprab3s  8048  fmpox  8062  fparlem1  8105  fparlem2  8106  ralxp3f  8131  frpoins3xpg  8134  brtpos0  8227  dftpos3  8238  tpostpos  8240  dfrecs3  8357  tz7.48lem  8426  omeu  8568  ercnv  8714  ixp0  8927  xpcomco  9053  xpassen  9057  php  9189  findcard3  9241  ixpfi2  9305  dfsup2  9402  sup0riota  9424  card2on  9514  infeq5i  9603  cnfcom3lem  9670  ssttrcl  9682  ttrcltr  9683  ttrclss  9687  setinds2f  9717  frins2f  9723  r1elss  9776  rankxplim  9849  scott0bs  9871  scott0bsOLD  9872  aceq1  10108  dfac5lem1  10114  dfac5lem2  10115  kmlem3  10143  kmlem8  10148  kmlem16  10156  djuinf  10179  cf0  10240  alephval2  10563  fpwwe2lem7  10628  fpwwe2lem11  10632  rankcf  10768  r1tskina  10773  wfgru  10807  genpass  11000  psslinpr  11022  ltpsrpr  11100  addeq0  11643  infm3  12180  nnwos  12945  ioo0  13403  ico0  13424  ioc0  13425  icc0  13426  elfz2nn0  13653  elfzmlbp  13674  sqeqori  14257  hashgt12el  14466  hashgt12el2  14467  cshwidxmod  14847  clim0  15564  divalglem6  16462  ncoprmlnprm  16793  pceu  16912  prmreclem2  16983  cshwshash  17170  xpscf  17625  acsfn2  17725  invsym2  17826  cat1  18160  pospo  18405  issubmndb  18869  f1omvdco3  19525  psgnunilem5  19570  efgrelexlemb  19826  gexex  19929  srgrmhm  20310  isdomn3  20824  isdomn4r  20828  lssne0  21083  islindf4  21999  opsrtoslem1  22217  opsrtoslem2  22218  mdetunilem8  22787  cpmatmcllem  22886  pmatcollpw2lem  22945  ntreq0  23245  ordtrest2lem  23371  ist0-3  23513  ist1-2  23515  ist1-3  23517  cmpfi  23576  2ndcctbss  23623  ptbasfi  23749  ptcnplem  23789  hausdiag  23813  hauseqlcld  23814  cnmptcom  23846  txflf  24174  tgphaus  24285  metrest  24692  iccpnfcnv  25114  bcth3  25501  dyadmax  25768  vitalilem2  25779  vitalilem3  25780  mbfimaopnlem  25825  itg2leub  25904  dvres2  26082  ellogdm  26815  reasinsin  27072  leibpilem2  27117  ftalem3  27250  dchreq  27433  bdayimaon  27868  noetainflem4  27915  cuteq1  28021  addsprop  28180  leadds1  28193  negsprop  28239  mulsprop  28334  mulsuniflem  28353  addsdilem1  28355  addsdilem2  28356  mulsasslem1  28367  mulsasslem2  28368  precsexlem10  28420  precsexlem11  28421  onnolt  28470  bdayn0p1  28573  legso  28879  outpasch  29048  axcontlem2  29326  incistruhgr  29440  nbgrel  29701  usgr2pth0  30125  rusgrnumwwlkslem  30332  frgr3v  30637  4cycl2vnunb  30652  frgrncvvdeqlem2  30662  lnon0  31161  spansncvi  32015  pjssmii  32044  nmlnopgt0i  32360  largei  32630  cvexchlem  32731  xfree  32807  nmo  32847  reuxfrdf  32848  fpwrelmapffslem  33088  eliccioo  33261  1arithidom  33836  ufdprmidl  33840  qtophaus  34235  ordtrest2NEWlem  34321  ordtconnlem1  34323  xrge0iifcnv  34332  xrge0iifiso  34334  xrge0iifhom  34336  cntnevol  34627  eulerpartlemgh  34777  ballotlem7  34935  signswch  34957  bnj446  35115  bnj563  35141  bnj110  35255  bnj153  35277  bnj864  35319  bnj865  35320  bnj849  35322  bnj929  35333  bnj1110  35379  onrankid  35503  fineqvac  35537  axregs  35560  cusgr3cyclex  35636  derang0  35669  iccllysconn  35750  cvmsss2  35774  satf0op  35877  elmrsubrn  36020  rexxfr3dALT  36139  quad3  36170  axacprim  36207  dftr6  36251  elintfv  36265  opelco3  36275  elima4  36276  elpotr  36279  wzel  36322  elfuns  36413  dfiota3  36421  brimg  36435  imagesset  36453  lineunray  36647  ellines  36652  hfninf  36686  in-ax8  36764  ss-ax8  36765  bj-df-sb  37300  bj-elabtru  37537  bj-snglc  37633  bj-mpomptALT  37789  bj-elid7  37843  bj-imdirco  37862  nlpineqsn  38082  curf  38277  tan2h  38291  poimirlem26  38325  poimirlem27  38326  poimirlem30  38329  poimirlem32  38331  poimir  38332  ovoliunnfl  38341  voliunnfl  38343  ftc1anc  38380  inixp  38407  heibor1lem  38488  csbcom2fi  38805  tsna1  38821  anan  38912  brid  38989  ref5  38996  idinxpssinxp4  39003  iss2  39021  raldmqseu  39042  xrninxp  39092  cossssid3  39236  dmqs1cosscnvepreseq  39424  disjxrnres5  39524  dmqsblocks  39644  islshpat  39819  lkr0f  39896  lshpsmreu  39911  cvrnbtwn4  40081  ishlat2  40155  islvol5  40381  tendoeq2  41576  dibelval3  41949  mapdpglem3  42477  hdmapglem7a  42729  4rexfrabdioph  43553  dford4  43784  fgraphopab  43958  onsupmaxb  43994  tfsconcatlem  44091  ifpim123g  44254  ifpbibib  44264  rp-isfinite6  44272  elrncard  44291  undmrnresiss  44358  cnvssco  44360  iunrelexpuztr  44473  dffrege115  44732  brco2f1o  44786  ntrneiiso  44845  ismnuprim  45032  undisjrab  45044  radcnvrat  45052  opelopab4  45288  2sb5nd  45297  un2122  45526  uunT12p4  45539  2sb5ndVD  45646  2sb5ndALT  45668  ndisj2  45799  ssabf  45846  abssf  45858  fourierdlem42  46891  smflimlem4  47516  aiotaexaiotaiota  47859  ndmaovcom  47970  dmafv2rnb  47994  afv2ndeffv0  48025  modm1p1ne  48141  0nelsetpreimafv  48167  usgrexmpl2nb0  48824  usgrexmpl2nb1  48825  gpg5nbgrvtx03starlem1  48861  gpg5nbgrvtx03starlem2  48862  gpg5nbgrvtx03starlem3  48863  gpg5nbgrvtx13starlem1  48864  gpg5nbgrvtx13starlem2  48865  gpg5nbgrvtx13starlem3  48866  pgnbgreunbgrlem2lem2  48908  gpg5edgnedg  48923  eliunxp2  49142  pgrpgt2nabl  49174  islindeps  49261  lindslinindsimp1  49265  lindslinindsimp2  49271