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  2038  sbiedvw  2132  sbievw2  2135  cbvsbv  2137  sbal  2206  sbco4OLD  2211  sb6a  2294  sbiedw  2348  sbied  2534  sbidm  2541  mo  2592  2eu6  2683  cbvab  2834  nabbib  3062  rexcom4a  3294  abv  3465  ceqsex  3500  ceqsexv  3501  spc2ed  3558  clel2g  3616  2reuswap  3707  2reuswap2  3708  2reu5  3719  2rmoswap  3722  nfcdeq  3738  sbcid  3759  sbcco2  3769  sbc7  3774  sbcie2g  3782  eqsbc1  3788  sbcralt  3822  cbvralcsf  3892  cbvrabcsf  3895  abss  4013  ssab  4014  raldifb  4099  difrab  4267  euelss  4281  sbccsb  4397  vdif0  4425  difrab0eq  4426  ssunsn2  4791  sspr  4798  sstp  4799  uniintsn  4948  brab1  5157  unopab  5189  axrep5  5244  axrep6OLD  5246  intexab  5314  reusv2lem4  5370  reusv2  5372  el.OLD  5418  wefrc  5653  eliunxp  5821  ralxp  5825  rexxp  5826  opelco  5855  reldm0  5916  resieq  5987  iss  6035  imai  6074  intasym  6113  asymref  6114  codir  6118  poirr2  6122  xpdifid  6164  rninxp  6176  dfpo2  6298  frpoins2fg  6346  ordelord  6383  ordtri3  6398  funopg  6571  fin  6759  f1cnvcnv  6786  funimass4  6946  fnressn  7158  resoprab  7534  mpo2eqb  7548  elrnmpores  7554  ov6g  7580  imaeqexov  7655  imaeqalov  7656  offval  7690  uniuni  7764  dfwe2  7776  orduniorsuc  7829  tfinds2  7863  dfopab2  8052  dfoprab3s  8053  fmpox  8067  fparlem1  8112  fparlem2  8113  ralxp3f  8138  frpoins3xpg  8141  brtpos0  8234  dftpos3  8245  tpostpos  8247  dfrecs3  8364  tz7.48lem  8433  omeu  8575  ercnv  8721  curf  8872  ixp0  8941  xpcomco  9068  xpassen  9072  php  9204  findcard3  9256  ixpfi2  9320  dfsup2  9417  sup0riota  9439  card2on  9529  infeq5i  9618  cnfcom3lem  9685  ssttrcl  9697  ttrcltr  9698  ttrclss  9702  setinds2f  9732  frins2f  9738  r1elss  9791  rankxplim  9864  scott0bs  9886  scott0bsOLD  9887  aceq1  10123  dfac5lem1  10129  dfac5lem2  10130  kmlem3  10158  kmlem8  10163  kmlem16  10171  djuinf  10194  cf0  10255  alephval2  10584  fpwwe2lem7  10649  fpwwe2lem11  10653  rankcf  10789  r1tskina  10794  wfgru  10828  genpass  11021  psslinpr  11043  ltpsrpr  11121  addeq0  11664  infm3  12201  nnwos  12967  ioo0  13425  ico0  13446  ioc0  13447  icc0  13448  elfz2nn0  13675  elfzmlbp  13696  sqeqori  14280  hashgt12el  14489  hashgt12el2  14490  cshwidxmod  14876  clim0  15595  divalglem6  16492  ncoprmlnprm  16823  pceu  16942  prmreclem2  17013  cshwshash  17200  xpscf  17655  acsfn2  17755  invsym2  17856  cat1  18190  pospo  18435  issubmndb  18917  f1omvdco3  19580  psgnunilem5  19625  efgrelexlemb  19881  gexex  19984  srgrmhm  20365  isdomn3  20880  isdomn4r  20884  lssne0  21139  islindf4  22055  opsrtoslem1  22275  opsrtoslem2  22276  mdetunilem8  22845  cpmatmcllem  22947  pmatcollpw2lem  23006  ntreq0  23306  ordtrest2lem  23432  ist0-3  23574  ist1-2  23576  ist1-3  23578  cmpfi  23637  2ndcctbss  23685  ptbasfi  23811  ptcnplem  23851  hausdiag  23875  hauseqlcld  23876  cnmptcom  23908  txflf  24236  tgphaus  24347  metrest  24754  iccpnfcnv  25176  bcth3  25563  dyadmax  25830  vitalilem2  25841  vitalilem3  25842  mbfimaopnlem  25887  itg2leub  25966  dvres2  26144  ellogdm  26877  reasinsin  27134  leibpilem2  27179  ftalem3  27312  dchreq  27495  bdayimaon  27930  noetainflem4  27977  cuteq1  28083  addsprop  28242  leadds1  28255  negsprop  28301  mulsprop  28396  mulsuniflem  28415  addsdilem1  28417  addsdilem2  28418  mulsasslem1  28429  mulsasslem2  28430  precsexlem10  28482  precsexlem11  28483  onnolt  28532  bdayn0p1  28635  legso  28942  outpasch  29113  axcontlem2  29423  incistruhgr  29537  nbgrel  29801  usgr2pth0  30231  rusgrnumwwlkslem  30441  frgr3v  30756  4cycl2vnunb  30771  frgrncvvdeqlem2  30781  lnon0  31280  spansncvi  32134  pjssmii  32163  nmlnopgt0i  32479  largei  32749  cvexchlem  32850  xfree  32926  nmo  32966  reuxfrdf  32967  fpwrelmapffslem  33205  eliccioo  33378  1arithidom  33949  ufdprmidl  33953  qtophaus  34348  ordtrest2NEWlem  34434  ordtconnlem1  34436  xrge0iifcnv  34445  xrge0iifiso  34447  xrge0iifhom  34449  cntnevol  34741  eulerpartlemgh  34891  ballotlem7  35049  signswch  35071  bnj446  35229  bnj563  35255  bnj110  35369  bnj153  35391  bnj864  35433  bnj865  35434  bnj849  35436  bnj929  35447  bnj1110  35493  onrankid  35610  fineqvac  35644  axregs  35667  cusgr3cyclex  35727  derang0  35750  iccllysconn  35831  cvmsss2  35855  satf0op  35958  elmrsubrn  36101  rexxfr3dALT  36220  quad3  36251  axacprim  36288  dftr6  36332  elintfv  36346  opelco3  36356  elima4  36357  elpotr  36360  wzel  36403  elfuns  36494  dfiota3  36502  brimg  36516  imagesset  36534  lineunray  36729  ellines  36734  hfninf  36768  in-ax8  36846  ss-ax8  36847  bj-df-sb  37382  bj-elabtru  37619  bj-snglc  37715  bj-mpomptALT  37871  bj-elid7  37925  bj-imdirco  37944  nlpineqsn  38164  tan2h  38368  poimirlem26  38397  poimirlem27  38398  poimirlem30  38401  poimirlem32  38403  poimir  38404  ovoliunnfl  38413  voliunnfl  38415  ftc1anc  38452  inixp  38480  heibor1lem  38561  csbcom2fi  38878  tsna1  38894  anan  38985  brid  39062  ref5  39069  idinxpssinxp4  39076  iss2  39094  raldmqseu  39115  xrninxp  39165  cossssid3  39309  dmqs1cosscnvepreseq  39497  disjxrnres5  39597  dmqsblocks  39717  islshpat  39892  lkr0f  39969  lshpsmreu  39984  cvrnbtwn4  40154  ishlat2  40228  islvol5  40454  tendoeq2  41649  dibelval3  42022  mapdpglem3  42550  hdmapglem7a  42802  4rexfrabdioph  43641  dford4  43872  fgraphopab  44046  onsupmaxb  44082  tfsconcatlem  44179  ifpim123g  44342  ifpbibib  44352  rp-isfinite6  44360  elrncard  44379  undmrnresiss  44446  cnvssco  44448  iunrelexpuztr  44561  dffrege115  44820  brco2f1o  44874  ntrneiiso  44933  ismnuprim  45120  undisjrab  45132  radcnvrat  45140  opelopab4  45376  2sb5nd  45385  un2122  45614  uunT12p4  45627  2sb5ndVD  45734  2sb5ndALT  45756  ndisj2  45887  ssabf  45934  abssf  45946  fourierdlem42  46979  smflimlem4  47604  aiotaexaiotaiota  47984  ndmaovcom  48095  dmafv2rnb  48119  afv2ndeffv0  48150  modm1p1ne  48266  0nelsetpreimafv  48292  usgrexmpl2nb0  48949  usgrexmpl2nb1  48950  gpg5nbgrvtx03starlem1  48986  gpg5nbgrvtx03starlem2  48987  gpg5nbgrvtx03starlem3  48988  gpg5nbgrvtx13starlem1  48989  gpg5nbgrvtx13starlem2  48990  gpg5nbgrvtx13starlem3  48991  pgnbgreunbgrlem2lem2  49033  gpg5edgnedg  49048  eliunxp2  49266  pgrpgt2nabl  49298  islindeps  49385  lindslinindsimp1  49389  lindslinindsimp2  49395