Theorem bitr3i 279

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

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  3bitrri  300  3bitr3i  303  3bitr3ri  304  xchnxbi  334  an13  645  anandi  674  anandir  675  orordi  925  orordir  926  ianor  978  trunantru  1578  falnanfal  1581  had0  1605  nic-axALT  1675  equsexvw  2011  sbiedvw  2104  sbievw2  2107  sbal  2166  sb6a  2259  sb56  2277  sbco4  2284  sbiedw  2332  sbiedwOLD  2333  sbied  2545  sbidm  2552  sbiedALT  2614  mo  2649  2mos  2734  2eu6  2742  cbvabv  2891  cbvabw  2892  cbvab  2893  nabbi  3123  rexcom4a  3253  r19.41v  3349  r19.41  3350  2ralor  3371  spc2ed  3604  2reuswap  3739  2reuswap2  3740  2reu5  3751  2rmoswap  3754  nfcdeq  3770  sbcid  3791  sbcco2  3801  sbc7  3805  sbcie2g  3813  eqsbc3  3819  eqsbc3OLD  3820  sbcralt  3857  cbvralcsf  3927  cbvrabcsf  3930  abss  4042  ssab  4043  raldifb  4123  difrab  4279  euelss  4292  sbccsb  4387  vdif0  4420  difrab0eq  4421  ssunsn2  4762  sspr  4768  sstp  4769  uniintsn  4915  brab1  5116  unopab  5147  axrep5  5198  axrep6  5199  intexab  5244  reusv2lem4  5304  reusv2  5306  wefrc  5551  eliunxp  5710  ralxp  5714  rexxp  5715  opelco  5744  reldm0  5800  resieq  5866  iss  5905  imai  5944  cnvsym  5976  intasym  5977  asymref  5978  codir  5982  poirr2  5986  xpdifid  6027  rninxp  6038  tz6.26  6181  wfis2fg  6187  ordelord  6215  ordtri3  6229  dffun3  6368  funopg  6391  fin  6561  f1cnvcnv  6586  funimass4  6732  fnressn  6922  resoprab  7272  mpo2eqb  7285  elrnmpores  7290  ov6g  7314  offval  7418  uniuni  7486  dfwe2  7498  orduniorsuc  7547  tfinds2  7580  dfopab2  7752  dfoprab3s  7753  fmpox  7767  fparlem1  7809  fparlem2  7810  brtpos0  7901  dftpos3  7912  tpostpos  7914  dfrecs3  8011  tz7.48lem  8079  omeu  8213  ercnv  8312  ixp0  8497  xpcomco  8609  xpassen  8613  php  8703  findcard3  8763  ixpfi2  8824  dfsup2  8910  sup0riota  8931  card2on  9020  infeq5i  9101  cnfcom3lem  9168  r1elss  9237  rankxplim  9310  scott0s  9319  aceq1  9545  dfac5lem1  9551  dfac5lem2  9552  kmlem3  9580  kmlem8  9585  kmlem16  9593  djuinf  9616  cflem  9670  cf0  9675  alephval2  9996  fpwwe2lem8  10061  fpwwe2lem12  10065  rankcf  10201  r1tskina  10206  wfgru  10240  genpass  10433  psslinpr  10455  ltpsrpr  10533  addeq0  11065  infm3  11602  nnwos  12318  ioo0  12766  ico0  12787  ioc0  12788  icc0  12789  elfz2nn0  13001  elfzmlbp  13021  sqeqori  13579  hashgt12el  13786  hashgt12el2  13787  cshwidxmod  14167  clim0  14865  divalglem6  15751  ncoprmlnprm  16070  pceu  16185  prmreclem2  16255  cshwshash  16440  xpscf  16840  acsfn2  16936  invsym2  17035  pospo  17585  issubmndb  17972  f1omvdco3  18579  psgnunilem5  18624  efgrelexlemb  18878  gexex  18975  srgrmhm  19288  lssne0  19724  opsrtoslem1  20266  opsrtoslem2  20267  islindf4  20984  mdetunilem8  21230  cpmatmcllem  21328  pmatcollpw2lem  21387  ntreq0  21687  ordtrest2lem  21813  ist0-3  21955  ist1-2  21957  ist1-3  21959  cmpfi  22018  2ndcctbss  22065  ptbasfi  22191  ptcnplem  22231  hausdiag  22255  hauseqlcld  22256  cnmptcom  22288  txflf  22616  tgphaus  22727  metrest  23136  iccpnfcnv  23550  bcth3  23936  dyadmax  24201  vitalilem2  24212  vitalilem3  24213  mbfimaopnlem  24258  itg2leub  24337  dvres2  24512  ellogdm  25224  reasinsin  25476  leibpilem2  25521  ftalem3  25654  dchreq  25836  legso  26387  outpasch  26543  axcontlem2  26753  incistruhgr  26866  nbgrel  27124  usgr2pth0  27548  rusgrnumwwlkslem  27750  frgr3v  28056  4cycl2vnunb  28071  frgrncvvdeqlem2  28081  lnon0  28577  spansncvi  29431  pjssmii  29460  nmlnopgt0i  29776  largei  30046  cvexchlem  30147  xfree  30223  nmo  30256  reuxfrdf  30257  fpwrelmapffslem  30470  eliccioo  30609  qtophaus  31102  ordtrest2NEWlem  31167  ordtconnlem1  31169  xrge0iifcnv  31178  xrge0iifiso  31180  xrge0iifhom  31182  cntnevol  31489  eulerpartlemgh  31638  ballotlem7  31795  signswch  31833  bnj446  31989  bnj563  32016  bnj110  32132  bnj153  32154  bnj864  32196  bnj865  32197  bnj849  32199  bnj929  32210  bnj1110  32256  cusgr3cyclex  32385  derang0  32418  iccllysconn  32499  cvmsss2  32523  satf0op  32626  elmrsubrn  32769  quad3  32915  axacprim  32935  dftr6  32988  dfpo2  32993  elintfv  33009  opelco3  33020  elima4  33021  setinds2f  33026  elpotr  33028  frpoins2fg  33084  frins2fg  33091  wzel  33113  bdayimaon  33199  elfuns  33378  dfiota3  33386  brimg  33400  imagesset  33416  lineunray  33610  ellines  33615  hfninf  33649  bj-snglc  34283  bj-mpomptALT  34413  bj-elid7  34465  bj-isrvec  34577  nlpineqsn  34691  curf  34872  tan2h  34886  poimirlem26  34920  poimirlem27  34921  poimirlem30  34924  poimirlem32  34926  poimir  34927  ovoliunnfl  34936  voliunnfl  34938  ftc1anc  34977  inixp  35005  heibor1lem  35089  csbcom2fi  35408  tsna1  35424  anan  35501  brid  35566  idinxpssinxp4  35579  iss2  35603  xrninxp  35642  cossssid3  35711  dmqs1cosscnvepreseq  35898  islshpat  36155  lkr0f  36232  lshpsmreu  36247  cvrnbtwn4  36417  ishlat2  36491  islvol5  36717  tendoeq2  37912  dibelval3  38285  mapdpglem3  38813  hdmapglem7a  39065  4rexfrabdioph  39402  dford4  39633  isdomn3  39811  fgraphopab  39817  ifpim123g  39873  ifpbibib  39883  rp-isfinite6  39891  elrncard  39909  undmrnresiss  39971  cnvssco  39973  iunrelexpuztr  40071  dffrege115  40331  brco2f1o  40389  ntrneiiso  40448  ismnuprim  40637  undisjrab  40645  radcnvrat  40653  opelopab4  40892  2sb5nd  40901  un2122  41131  uunT12p4  41144  2sb5ndVD  41251  2sb5ndALT  41273  ndisj2  41320  ssabf  41373  abssf  41385  fourierdlem42  42441  smflimlem4  43057  aiotaexaiotaiota  43299  ndmaovcom  43411  dmafv2rnb  43435  afv2ndeffv0  43466  0nelsetpreimafv  43557  eliunxp2  44389  pgrpgt2nabl  44421  islindeps  44515  lindslinindsimp1  44519  lindslinindsimp2  44525