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  1610  falnanfal  1613  had0OLD  1635  nic-axALT  1706  equsexvw  2037  sbiedvw  2131  sbievw2  2134  cbvsbv  2136  sbal  2205  sb6a  2292  sbiedw  2346  sbied  2532  sbidm  2539  mo  2590  2eu6  2681  cbvab  2832  nabbib  3060  rexcom4a  3292  abv  3462  ceqsex  3497  ceqsexv  3498  spc2ed  3555  clel2g  3612  2reuswap  3703  2reuswap2  3704  2reu5  3715  2rmoswap  3718  nfcdeq  3734  sbcid  3755  sbcco2  3765  sbc7  3770  sbcie2g  3778  eqsbc1  3784  sbcralt  3818  cbvralcsf  3888  cbvrabcsf  3891  abss  3987  ssab  3988  raldifb  4085  difrab  4263  euelss  4277  sbccsb  4393  vdif0  4421  difrab0eq  4422  ssunsn2  4787  sspr  4794  sstp  4795  uniintsn  4944  brab1  5152  unopab  5184  axrep5  5238  intexab  5306  reusv2lem4  5362  reusv2  5364  el.OLD  5406  wefrc  5644  eliunxp  5813  ralxp  5817  rexxp  5818  opelco  5848  reldm0  5909  resieq  5980  iss  6026  imai  6071  intasym  6108  asymref  6109  codir  6113  poirr2  6117  xpdifid  6158  rninxp  6170  dfpo2  6299  frpoins2fg  6347  ordelord  6384  ordtri3  6399  funopg  6574  fin  6762  f1cnvcnv  6789  funimass4  6949  fnressn  7162  resoprab  7538  mpo2eqb  7552  elrnmpores  7558  ov6g  7584  imaeqexov  7659  imaeqalov  7660  mpt3mpt  7685  offval  7702  uniuni  7776  dfwe2  7788  orduniorsuc  7841  tfinds2  7875  dfopab2  8063  dfoprab3s  8064  fmpox  8078  fparlem1  8123  fparlem2  8124  ralxp3f  8154  frpoins3xpg  8157  brtpos0  8251  dftpos3  8262  tpostpos  8264  dfrecs3  8381  tz7.48lemOLD  8452  omeu  8594  ercnv  8740  curf  8891  ixp0  8960  xpcomco  9087  xpassen  9091  php  9223  findcard3  9275  ixpfi2  9340  dfsup2  9437  sup0riota  9459  card2on  9549  infeq5i  9638  cnfcom3lem  9705  ssttrcl  9717  ttrcltr  9718  ttrclss  9722  setinds2f  9752  frins2f  9758  r1elss  9815  rankxplim  9897  scott0bs  9945  scott0bsOLD  9946  aceq1  10197  dfac5lem1  10203  dfac5lem2  10204  kmlem3  10232  kmlem8  10237  kmlem16  10245  djuinf  10268  cf0  10329  alephval2  10658  fpwwe2lem7  10723  fpwwe2lem11  10727  rankcf  10863  r1tskina  10868  wfgru  10902  genpass  11095  psslinpr  11117  ltpsrpr  11195  addeq0  11740  infm3  12277  nnwos  13043  ioo0  13502  ico0  13523  ioc0  13524  icc0  13525  elfz2nn0  13753  elfzmlbp  13774  sqeqori  14359  hashgt12el  14568  hashgt12el2  14569  cshwidxmod  14955  clim0  15674  divalglem6  16569  ncoprmlnprm  16905  pceu  17025  prmreclem2  17096  cshwshash  17283  xpscf  17738  acsfn2  17838  invsym2  17939  cat1  18273  pospo  18518  issubmndb  19001  f1omvdco3  19664  psgnunilem5  19709  efgrelexlemb  19965  gexex  20068  srgrmhm  20449  dfring3  20519  isdomn3  20967  isdomn4r  20971  lssne0  21227  islindf4  22145  opsrtoslem1  22365  opsrtoslem2  22366  mdetunilem8  22935  cpmatmcllem  23037  pmatcollpw2lem  23096  ntreq0  23396  ordtrest2lem  23522  ist0-3  23664  ist1-2  23666  ist1-3  23668  cmpfi  23727  2ndcctbss  23775  ptbasfi  23901  ptcnplem  23941  hausdiag  23965  hauseqlcld  23966  cnmptcom  23998  txflf  24326  tgphaus  24437  metrest  24844  iccpnfcnv  25266  bcth3  25653  dyadmax  25920  vitalilem2  25931  vitalilem3  25932  mbfimaopnlem  25977  itg2leub  26056  dvres2  26233  ellogdm  26968  reasinsin  27225  leibpilem2  27270  ftalem3  27403  dchreq  27586  bdayimaon  28051  noetainflem4  28098  cuteq1  28204  addsprop  28363  leadds1  28376  negsprop  28422  mulsprop  28517  mulsuniflem  28536  addsdilem1  28538  addsdilem2  28539  mulsasslem1  28550  mulsasslem2  28551  precsexlem10  28603  precsexlem11  28604  onnolt  28653  bdayn0p1  28756  legso  29063  outpasch  29234  axcontlem2  29544  incistruhgr  29658  nbgrel  29922  usgr2pth0  30352  rusgrnumwwlkslem  30562  frgr3v  30877  4cycl2vnunb  30892  frgrncvvdeqlem2  30902  lnon0  31401  spansncvi  32255  pjssmii  32284  nmlnopgt0i  32600  largei  32870  cvexchlem  32971  xfree  33089  nmo  33129  reuxfrdf  33130  fpwrelmapffslem  33367  eliccioo  33540  1arithidom  34112  ufdprmidl  34116  qtophaus  34511  ordtrest2NEWlem  34597  ordtconnlem1  34599  xrge0iifcnv  34608  xrge0iifiso  34610  xrge0iifhom  34612  cntnevol  34904  eulerpartlemgh  35053  ballotlem7  35211  signswch  35233  bnj446  35391  bnj563  35417  bnj110  35531  bnj153  35553  bnj864  35595  bnj865  35596  bnj849  35598  bnj929  35609  bnj1110  35655  onrankid  35772  fineqvac  35833  axregs  35856  cusgr3cyclex  35980  derang0  36003  iccllysconn  36084  cvmsss2  36108  satf0op  36211  elmrsubrn  36354  rexxfr3dALT  36473  quad3  36504  axacprim  36547  dftr6  36591  elintfv  36605  opelco3  36614  elima4  36615  elpotr  36618  wzel  36661  elfuns  36752  dfiota3  36760  brimg  36774  imagesset  36792  lineunray  36987  ellines  36992  hfninf  37010  in-ax8  37088  ss-ax8  37089  bj-df-sb  37624  bj-elabtru  37861  bj-snglc  37957  bj-mpomptALT  38116  bj-elid7  38168  bj-imdirco  38187  nlpineqsn  38407  tan2h  38611  poimirlem26  38640  poimirlem27  38641  poimirlem30  38644  poimirlem32  38646  poimir  38647  ovoliunnfl  38656  voliunnfl  38658  ftc1anc  38695  inixp  38738  heibor1lem  38819  csbcom2fi  39136  tsna1  39152  anan  39243  brid  39320  ref5  39327  idinxpssinxp4  39334  iss2  39352  raldmqseu  39373  xrninxp  39423  cossssid3  39567  dmqs1cosscnvepreseq  39755  disjxrnres5  39855  dmqsblocks  39975  islshpat  40150  lkr0f  40227  lshpsmreu  40242  cvrnbtwn4  40412  ishlat2  40486  islvol5  40712  tendoeq2  41907  dibelval3  42280  mapdpglem3  42808  hdmapglem7a  43060  4rexfrabdioph  43881  dford4  44112  fgraphopab  44281  onsupmaxb  44317  tfsconcatlem  44414  ifpim123g  44577  ifpbibib  44587  rp-isfinite6  44595  elrncard  44614  undmrnresiss  44680  cnvssco  44682  iunrelexpuztr  44795  dffrege115  45054  brco2f1o  45108  ntrneiiso  45167  ismnuprim  45354  undisjrab  45366  radcnvrat  45374  opelopab4  45610  2sb5nd  45619  un2122  45848  uunT12p4  45861  2sb5ndVD  45968  2sb5ndALT  45990  ndisj2  46144  ssabf  46191  abssf  46203  fourierdlem42  47235  smflimlem4  47860  aiotaexaiotaiota  48240  ndmaovcom  48351  dmafv2rnb  48375  afv2ndeffv0  48406  modm1p1ne  48522  0nelsetpreimafv  48548  usgrexmpl2nb0  49205  usgrexmpl2nb1  49206  gpg5nbgrvtx03starlem1  49242  gpg5nbgrvtx03starlem2  49243  gpg5nbgrvtx03starlem3  49244  gpg5nbgrvtx13starlem1  49245  gpg5nbgrvtx13starlem2  49246  gpg5nbgrvtx13starlem3  49247  pgnbgreunbgrlem2lem2  49289  gpg5edgnedg  49304  eliunxp2  49522  pgrpgt2nabl  49554  islindeps  49641  lindslinindsimp1  49645  lindslinindsimp2  49651