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 ⊢ (𝜑 ↔ 𝜒)

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  3bitrri  301  3bitr3i  304  3bitr3ri  305  xchnxbi  335  an13  659  anandi  688  anandir  689  orordi  941  orordir  942  ianor  997  trunantru  1609  falnanfal  1612  had0  1632  nic-axALT  1702  equsexvw  2033  sbiedvw  2128  sbievw2  2131  cbvsbv  2133  sbal  2202  sbco4OLD  2207  sb6a  2292  sbiedw  2347  sbied  2533  sbidm  2540  mo  2591  2eu6  2682  cbvab  2833  nabbib  3061  rexcom4a  3293  abv  3465  ceqsex  3500  ceqsexv  3501  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  5316  reusv2lem4  5372  reusv2  5374  elOLD  5420  wefrc  5655  eliunxp  5823  ralxp  5827  rexxp  5828  opelco  5857  reldm0  5918  resieq  5989  iss  6037  imai  6076  intasym  6115  asymref  6116  codir  6120  poirr2  6124  xpdifid  6165  rninxp  6177  dfpo2  6297  frpoins2fg  6345  ordelord  6382  ordtri3  6397  funopg  6570  fin  6758  f1cnvcnv  6785  funimass4  6945  fnressn  7155  resoprab  7528  mpo2eqb  7542  elrnmpores  7548  ov6g  7574  imaeqexov  7648  imaeqalov  7649  offval  7683  uniuni  7760  dfwe2  7772  orduniorsuc  7825  tfinds2  7859  dfopab2  8048  dfoprab3s  8049  fmpox  8063  fparlem1  8106  fparlem2  8107  ralxp3f  8132  frpoins3xpg  8135  brtpos0  8228  dftpos3  8239  tpostpos  8241  dfrecs3  8358  tz7.48lem  8427  omeu  8569  ercnv  8715  ixp0  8928  xpcomco  9054  xpassen  9058  php  9190  findcard3  9242  ixpfi2  9306  dfsup2  9403  sup0riota  9425  card2on  9515  infeq5i  9604  cnfcom3lem  9671  ssttrcl  9683  ttrcltr  9684  ttrclss  9688  setinds2f  9718  frins2f  9724  r1elss  9777  rankxplim  9850  scott0s  9861  aceq1  10100  dfac5lem1  10106  dfac5lem2  10107  kmlem3  10135  kmlem8  10140  kmlem16  10148  djuinf  10171  cflemOLD  10228  cf0  10233  alephval2  10556  fpwwe2lem7  10621  fpwwe2lem11  10625  rankcf  10761  r1tskina  10766  wfgru  10800  genpass  10993  psslinpr  11015  ltpsrpr  11093  addeq0  11636  infm3  12173  nnwos  12938  ioo0  13396  ico0  13417  ioc0  13418  icc0  13419  elfz2nn0  13646  elfzmlbp  13667  sqeqori  14250  hashgt12el  14459  hashgt12el2  14460  cshwidxmod  14840  clim0  15557  divalglem6  16455  ncoprmlnprm  16786  pceu  16905  prmreclem2  16976  cshwshash  17163  xpscf  17618  acsfn2  17718  invsym2  17819  cat1  18153  pospo  18398  issubmndb  18862  f1omvdco3  19518  psgnunilem5  19563  efgrelexlemb  19819  gexex  19922  srgrmhm  20303  isdomn3  20798  isdomn4r  20802  lssne0  21051  islindf4  21967  opsrtoslem1  22185  opsrtoslem2  22186  mdetunilem8  22755  cpmatmcllem  22854  pmatcollpw2lem  22913  ntreq0  23213  ordtrest2lem  23339  ist0-3  23481  ist1-2  23483  ist1-3  23485  cmpfi  23544  2ndcctbss  23591  ptbasfi  23717  ptcnplem  23757  hausdiag  23781  hauseqlcld  23782  cnmptcom  23814  txflf  24142  tgphaus  24253  metrest  24660  iccpnfcnv  25082  bcth3  25469  dyadmax  25736  vitalilem2  25747  vitalilem3  25748  mbfimaopnlem  25793  itg2leub  25872  dvres2  26050  ellogdm  26780  reasinsin  27037  leibpilem2  27082  ftalem3  27215  dchreq  27398  bdayimaon  27833  noetainflem4  27880  cuteq1  27986  addsprop  28145  leadds1  28158  negsprop  28204  mulsprop  28299  mulsuniflem  28318  addsdilem1  28320  addsdilem2  28321  mulsasslem1  28332  mulsasslem2  28333  precsexlem10  28385  precsexlem11  28386  onnolt  28435  bdayn0p1  28538  legso  28844  outpasch  29012  axcontlem2  29281  incistruhgr  29395  nbgrel  29656  usgr2pth0  30080  rusgrnumwwlkslem  30287  frgr3v  30592  4cycl2vnunb  30607  frgrncvvdeqlem2  30617  lnon0  31116  spansncvi  31970  pjssmii  31999  nmlnopgt0i  32315  largei  32585  cvexchlem  32686  xfree  32762  nmo  32802  reuxfrdf  32803  fpwrelmapffslem  33043  eliccioo  33216  1arithidom  33793  ufdprmidl  33797  qtophaus  34192  ordtrest2NEWlem  34278  ordtconnlem1  34280  xrge0iifcnv  34289  xrge0iifiso  34291  xrge0iifhom  34293  cntnevol  34584  eulerpartlemgh  34734  ballotlem7  34892  signswch  34914  bnj446  35072  bnj563  35098  bnj110  35212  bnj153  35234  bnj864  35276  bnj865  35277  bnj849  35279  bnj929  35290  bnj1110  35336  onrankid  35460  fineqvac  35495  axregs  35518  cusgr3cyclex  35594  derang0  35627  iccllysconn  35708  cvmsss2  35732  satf0op  35835  elmrsubrn  35978  rexxfr3dALT  36097  quad3  36128  axacprim  36165  dftr6  36209  elintfv  36223  opelco3  36233  elima4  36234  elpotr  36237  wzel  36280  elfuns  36371  dfiota3  36379  brimg  36393  imagesset  36411  lineunray  36605  ellines  36610  hfninf  36644  in-ax8  36702  ss-ax8  36703  bj-df-sb  37238  bj-elabtru  37475  bj-snglc  37571  bj-mpomptALT  37727  bj-elid7  37781  bj-imdirco  37800  nlpineqsn  38020  curf  38215  tan2h  38229  poimirlem26  38263  poimirlem27  38264  poimirlem30  38267  poimirlem32  38269  poimir  38270  ovoliunnfl  38279  voliunnfl  38281  ftc1anc  38318  inixp  38345  heibor1lem  38426  csbcom2fi  38745  tsna1  38761  anan  38852  brid  38929  ref5  38936  idinxpssinxp4  38943  iss2  38961  raldmqseu  38982  xrninxp  39032  cossssid3  39176  dmqs1cosscnvepreseq  39364  disjxrnres5  39464  dmqsblocks  39584  islshpat  39759  lkr0f  39836  lshpsmreu  39851  cvrnbtwn4  40021  ishlat2  40095  islvol5  40321  tendoeq2  41516  dibelval3  41889  mapdpglem3  42417  hdmapglem7a  42669  4rexfrabdioph  43495  dford4  43726  fgraphopab  43900  onsupmaxb  43936  tfsconcatlem  44033  ifpim123g  44196  ifpbibib  44206  rp-isfinite6  44214  elrncard  44233  undmrnresiss  44300  cnvssco  44302  iunrelexpuztr  44415  dffrege115  44674  brco2f1o  44728  ntrneiiso  44787  ismnuprim  44974  undisjrab  44986  radcnvrat  44994  opelopab4  45230  2sb5nd  45239  un2122  45468  uunT12p4  45481  2sb5ndVD  45588  2sb5ndALT  45610  ndisj2  45741  ssabf  45788  abssf  45800  fourierdlem42  46833  smflimlem4  47458  aiotaexaiotaiota  47798  ndmaovcom  47909  dmafv2rnb  47933  afv2ndeffv0  47964  modm1p1ne  48080  0nelsetpreimafv  48106  usgrexmpl2nb0  48763  usgrexmpl2nb1  48764  gpg5nbgrvtx03starlem1  48800  gpg5nbgrvtx03starlem2  48801  gpg5nbgrvtx03starlem3  48802  gpg5nbgrvtx13starlem1  48803  gpg5nbgrvtx13starlem2  48804  gpg5nbgrvtx13starlem3  48805  pgnbgreunbgrlem2lem2  48847  gpg5edgnedg  48862  eliunxp2  49081  pgrpgt2nabl  49113  islindeps  49200  lindslinindsimp1  49204  lindslinindsimp2  49210