Theorem bitr4i 278

Description: An inference from transitive law for logical equivalence. (Contributed by NM, 3-Jan-1993.)

Hypotheses

Ref	Expression
bitr4i.1	⊢ (𝜑 ↔ 𝜓)
bitr4i.2	⊢ (𝜒 ↔ 𝜓)

Assertion

Ref	Expression
bitr4i	⊢ (𝜑 ↔ 𝜒)

Proof of Theorem bitr4i

Step	Hyp	Ref	Expression
1		bitr4i.1	. 2 ⊢ (𝜑 ↔ 𝜓)
2		bitr4i.2	. . 3 ⊢ (𝜒 ↔ 𝜓)
3	2	bicomi 224	. 2 ⊢ (𝜓 ↔ 𝜒)
4	1, 3	bitri 275	1 ⊢ (𝜑 ↔ 𝜒)

Syntax hints:   ↔ wb 206

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 207

This theorem is referenced by:  3bitr2i  299  3bitr2ri  300  3bitr4i  303  3bitr4ri  304  biluk  385  biancomi  462  dfbi2  474  imdistan  567  pm5.32  573  bianass  642  mpbiran  709  biadaniALT  820  imor  853  imimorb  952  pm5.6  1003  nbi2  1017  casesifp  1077  3ancoma  1097  3ancomb  1098  3anrev  1100  dfnan2  1494  nannan  1497  nanbi  1500  xorcom  1514  xorneg  1523  xorbi12i  1524  norcom  1530  noran  1532  norasslem1  1534  trunortru  1589  trunorfal  1590  cadan  1609  cadcomb  1613  nic-ax  1673  nic-axALT  1674  nf3  1786  19.43  1882  equsv  2003  sbrimvw  2092  sbcom2  2174  sb5  2276  nf5  2282  nf6  2283  sbrim  2304  sbnf  2311  sb6x  2463  2sb5rf  2471  2sb6rf  2472  sb4b  2474  sb5f  2497  sbequ8  2500  sbhb  2520  eu6lem  2567  eu1  2604  iseqsetv-cleq  2794  issettru  2807  iseqsetv-clel  2808  issetlem  2809  cleqh  2858  cleqf  2921  sbabel  2925  necon3bii  2978  neor  3018  neorian  3021  rextru  3061  r19.26m  3091  r19.43  3102  3r19.43  3103  r2allem  3122  r19.23t  3234  ralcom4  3264  rexcomOLD  3268  moel  3378  rabid2f  3440  eqv  3460  eqvf  3461  ralv  3477  rexv  3478  reuv  3479  rmov  3480  rexcom4b  3482  ceqsex4v  3507  ceqsex8v  3509  ceqsrexv  3624  rexab  3669  ralrab2  3672  rexrab2  3674  reu2  3699  reu3  3701  reueq  3711  2reuswap  3720  2reuswap2  3721  reuind  3727  2reu5lem3  3731  2rmoswap  3735  rmo2  3853  rmoanim  3860  rmoanimALT  3861  dfss3  3938  dfss3f  3941  ssabral  4031  rabss  4038  ssrabeq  4050  uniiunlem  4053  sspsstri  4071  npss  4079  dfdif3OLD  4084  raldifb  4115  uncom  4124  inass  4194  elsymdifxor  4226  nsspssun  4234  dfss4  4235  dfun2  4236  dfin2  4237  indi  4250  reupick3  4296  eq0f  4313  neq0f  4314  eq0  4316  eq0ALT  4317  dfnf5  4348  rabn0  4355  csbab  4406  vss  4412  disj  4416  disj3  4420  undisj1  4428  undisj2  4429  inundif  4445  undif  4448  undifr  4449  rabsssn  4635  exsnrex  4647  euabsn2  4692  euabsn  4693  raldifsni  4762  tppreqb  4772  pwpw0  4780  prssg  4786  ssunsn  4795  prneimg2  4822  preqsn  4829  pwpr  4868  dfuni2  4876  unissb  4906  unissbOLD  4907  elint2  4920  ssint  4931  uniintab  4953  dfiin2g  4999  iunid  5027  iunn0  5034  iunxun  5061  iunxiun  5064  iinpw  5073  disjor  5092  disjxiun  5107  dftr2  5219  dftr5OLD  5222  dftr3  5223  dftr4  5224  axrep6OLD  5247  vnex  5272  inuni  5308  eusv2  5354  reusv2lem4  5359  rexxfr  5374  sspwb  5412  opthneg  5444  pwssun  5533  dfid3  5539  dffr6  5597  dffr2  5602  dffr2ALT  5603  opthprc  5705  elxp3  5707  xpiundir  5713  elvv  5716  reliun  5782  inxpOLD  5799  raliunxp  5806  cnvuni  5853  dmopab2rex  5884  dm0rn0  5891  dfres3  5958  ssdmres  5987  elidinxp  6018  idinxpres  6021  dfima2  6036  args  6066  dffr3  6073  cotrg  6083  cotrgOLD  6084  cotrgOLDOLD  6085  intasym  6091  asymref  6092  intirr  6094  xpnz  6135  xp11  6151  ssrnres  6154  xpimasn  6161  coiun  6232  coass  6241  cnvso  6264  elsnxp  6267  dfpo2  6272  imaindm  6275  dffr4  6296  dfse3  6312  frpoind  6318  dflim2  6393  orddif  6433  dffun2OLDOLD  6526  dffun6  6527  dffun6f  6532  dffun7  6546  dffun9  6548  funfn  6549  svrelfun  6591  mptfnf  6656  dffn2  6693  dffn3  6703  fint  6742  dffn4  6781  dff1o4  6811  brprcneu  6851  brprcneuALT  6852  eqfnfv3  7008  fnreseql  7023  fsn  7110  ftpg  7131  abrexco  7221  imaiun  7222  dff13  7232  isof1oidb  7302  isof1oopb  7303  isocnv2  7309  eloprabga  7501  mpo2eqb  7524  elovmpo  7637  sorpss  7707  abexex  7953  elxp6  8005  elxp7  8006  releldm2  8025  opiota  8041  fnmpo  8051  frxp  8108  frxp2  8126  soseq  8141  cnvimadfsn  8154  mpoxneldm  8194  dftpos4  8227  frrlem9  8276  dfrecs3  8344  tfrlem7  8354  ondif1  8468  oarec  8529  oeeu  8570  brinxper  8703  0er  8712  eroveu  8788  erovlem  8789  elixpconst  8881  domen  8936  brsdom  8949  brdom2  8956  reuen1  9000  sbthlem10  9066  brsdom2  9071  xpf1o  9109  unfi  9141  sbthfilem  9168  onfin2  9186  0sdom1domALT  9193  modom  9198  marypha2lem3  9395  wemapsolem  9510  elom3  9608  dfom5  9610  brttrcl2  9674  ttrcltr  9676  ttrclse  9687  trcl  9688  epfrs  9691  frind  9710  rankf  9754  scottexs  9847  scott0s  9848  cplem1  9849  hta  9857  djuexb  9869  pm54.43lem  9960  alephsuc2  10040  iscard3  10053  aceq0  10078  aceq3lem  10080  dfac3  10081  dfac5lem2  10084  dfac5  10089  dfac7  10093  dfac12a  10109  kmlem12  10122  kmlem14  10124  kmlem15  10125  infmap2  10177  ackbij2  10202  dfacfin7  10359  ituniiun  10382  zorng  10464  brdom7disj  10491  entri2  10518  alephreg  10542  fpwwe2lem11  10601  fpwwe2lem12  10602  pwfseqlem1  10618  grutsk  10782  axgroth4  10792  grothprim  10794  grothtsk  10795  elni2  10837  ltsopi  10848  genpass  10969  psslinpr  10991  ltexprlem4  10999  ltresr  11100  infm3  12149  elnnz  12546  dfz2  12555  2rexuz  12866  nnwos  12881  eluz2b1  12885  qexALT  12930  elxr  13083  dflt2  13115  xrsupss  13276  xrinfmss  13277  elixx1  13322  elioo2  13354  dfrp2  13362  elioopnf  13411  elicopnf  13413  elfz1  13480  fznn  13560  fzp1nel  13579  fznn0  13587  preduz  13618  prinfzo0  13666  injresinj  13756  nn0opthlem1  14240  faclbnd4lem1  14265  hashfxnn0  14309  hashprdifel  14370  hashgt23el  14396  hashfun  14409  hashf1  14429  fz1isolem  14433  f1oun2prg  14890  brtrclfv  14975  shftdm  15044  rediv  15104  imdiv  15111  rexanre  15320  caubnd  15332  climreu  15529  prodmo  15909  dvdslelem  16286  3dvdsdec  16309  3dvds2dec  16310  bitsval  16401  smueqlem  16467  algcvgblem  16554  lcmfunsnlem2  16617  isprm2  16659  isprm3  16660  isprm4  16661  pythagtriplem2  16795  elgz  16909  hashbc0  16983  0ram  16998  isstruct  17129  issect  17722  isfull2  17882  isfth2  17886  fucinv  17945  eldmcoa  18034  isdrs  18269  submacs  18761  isnsg4  19106  isgim  19201  gaorb  19246  oppgid  19295  oppgsubm  19301  oppgcntz  19303  ispgp  19529  efgsdm  19667  efgcpbllema  19691  iscyg2  19819  isrng  20070  isring  20153  isirred2  20337  opprirred  20338  isrnghm  20357  dfrhm2  20390  isnzr2  20434  opprsubrng  20475  opprsubrg  20509  isdomn3  20631  drngid2  20668  issdrg  20704  islmod  20777  lss1d  20876  islmhm  20941  islmim  20976  lbsextlem2  21076  lidlnz  21159  dfprm2  21390  isphl  21544  elocv  21584  iunocv  21597  isobs  21636  islinds  21725  1mavmul  22442  toprntopon  22819  isbasis3g  22843  fctop  22898  cctop  22900  isclo2  22982  restsn  23064  lmbr  23152  ist0-3  23239  2ndcdisj  23350  1stccnp  23356  islocfin  23411  1stckgenlem  23447  txbas  23461  ptbasin  23471  tx2cn  23504  fbfinnfr  23735  fbasrn  23778  filuni  23779  ufinffr  23823  fin1aufil  23826  rnelfmlem  23846  flimrest  23877  alexsubALTlem3  23943  alexsubALTlem4  23944  tgphaus  24011  istlm  24079  iscusp2  24196  metuel2  24460  isngp2  24492  isnlm  24570  isphtpc  24900  phtpcer  24901  om1elbas  24939  isclm  24971  iscvsp  25035  iscph  25077  iscau3  25185  minveclem3b  25335  elovolm  25383  ioombl1lem4  25469  dyaddisj  25504  vitali  25521  itg1climres  25622  itg2seq  25650  itg2monolem1  25658  itg2mono  25661  limcrcl  25782  lhop1  25926  itgsubst  25963  mdegleb  25976  isuc1p  26053  ismon1p  26055  plydivex  26212  ellogdm  26555  1cubr  26759  atandm2  26794  birthdaylem3  26870  dmarea  26874  dchrelbas2  27155  dchrelbas4  27161  elno3  27574  nosgnn0  27577  nosepon  27584  nocvxminlem  27696  scutcut  27720  scutbday  27723  dmscut  27730  scutf  27731  sltrec  27739  made0  27792  addsprop  27890  negsproplem2  27942  negsprop  27948  mulsprop  28040  precsexlem10  28125  elzs2  28294  elnnzs  28296  recut  28354  0reno  28355  axcontlem7  28904  nb3grpr  29316  nb3grpr2  29317  upgrwlkcompim  29578  wlkson  29591  wlkonprop  29593  wksonproplem  29639  wksonproplemOLD  29640  ispth  29658  wwlknon  29794  wwlksnextinj  29836  wspthsnwspthsnon  29853  elwspths2spth  29904  rusgrnumwwlkl1  29905  clwwlkccatlem  29925  erclwwlkref  29956  frgr3v  30211  nmoubi  30708  nmobndseqi  30715  nmobndseqiALT  30716  minvecolem1  30810  isch2  31159  hlimreui  31175  isch3  31177  ocsh  31219  dfch2  31343  spanuni  31480  nonbooli  31587  5oalem7  31596  adjsym  31769  elbdop2  31807  dmadjss  31823  nmopub  31844  nmfnleub  31861  nmop0h  31927  pjssposi  32108  pjordi  32109  cvbr2  32219  cvnbtwn2  32223  mdsl2i  32258  cvmdi  32260  elat2  32276  atom1d  32289  chirredi  32330  cdj3i  32377  or3di  32395  opreu2reu1  32420  mo5f  32425  reuxfrdf  32427  rexunirn  32428  difrab2  32434  rabsspr  32437  rabsstp  32438  tpssg  32473  iuninc  32496  disjorf  32515  disjunsn  32530  rabfmpunirn  32584  aciunf1  32594  funcnv5mpt  32599  eliccelico  32707  elicoelioo  32708  isomnd  33022  omndmul2  33033  isslmd  33162  islinds5  33345  ismxidl  33440  1arithufdlem4  33525  hasheuni  34082  pwsiga  34127  sigainb  34133  issros  34172  2ndmbfm  34259  omssubaddlem  34297  omssubadd  34298  sitgaddlemb  34346  eulerpartlemgvv  34374  eulerpartlemn  34379  probun  34417  ballotlem2  34487  ballotlemodife  34496  bnj252  34700  bnj253  34701  bnj255  34702  bnj345  34711  bnj133  34724  bnj976  34774  bnj1098  34780  bnj121  34867  bnj130  34871  bnj150  34873  bnj581  34905  bnj607  34913  bnj865  34920  bnj917  34931  bnj934  34932  bnj964  34940  bnj983  34948  bnj996  34953  bnj1021  34963  bnj1033  34966  bnj1047  34970  bnj1049  34971  bnj1090  34976  bnj1128  34987  bnj1175  35001  bnj1189  35006  bnj1253  35014  bnj1312  35055  exdifsn  35076  fineqvrep  35092  fineqvac  35094  onvf1odlem4  35100  vonf1owev  35102  erdszelem9  35193  erdszelem10  35194  pconnconn  35225  cvmliftiota  35295  fmlaomn0  35384  fmla0disjsuc  35392  fmlasucdisj  35393  dmopab3rexdif  35399  elmthm  35570  antnestALT  35688  nepss  35712  xpab  35720  dfso2  35749  elrn3  35756  elpotr  35776  dfon2lem5  35782  dfon2lem7  35784  dfon2lem8  35785  elwlim  35818  wzel  35819  brtxp2  35876  brpprod3a  35881  eltrans  35886  dfon3  35887  dffix2  35900  dffun10  35909  elfuns  35910  brsingle  35912  brimg  35932  funpartfun  35938  funpartfv  35940  cgrxfr  36050  segletr  36109  outsideoftr  36124  neifg  36366  filnetlem4  36376  df3nandALT1  36394  weiunlem2  36458  bj-consensusALT  36574  bj-df-ifc  36575  bj-biexal3  36702  bj-nfnnfTEMP  36753  bj-denoteslem  36866  bj-denotesALTV  36867  bj-ralvw  36874  bj-rexvw  36875  bj-rexcom4bv  36877  bj-rexcom4b  36878  bj-sbeq  36896  bj-inrab  36922  bj-rcleqf  37020  bj-dfmpoa  37113  bj-imdirco  37185  topdifinffinlem  37342  topdifinfeq  37345  relowlssretop  37358  relowlpssretop  37359  rdgeqoa  37365  domalom  37399  nlpineqsn  37403  fvineqsneq  37407  wl-ifpimpr  37461  wl-df3xor3  37465  wl-3xorbi  37468  wl-3xorbi2  37469  wl-2xor  37478  wl-2mintru2  37486  wl-dfclab  37591  rabiun  37594  phpreu  37605  fin2solem  37607  matunitlindflem2  37618  ptrest  37620  poimirlem25  37646  poimirlem27  37648  poimirlem30  37651  ismblfin  37662  ovoliunnfl  37663  voliunnfl  37665  volsupnfl  37666  itg2addnclem2  37673  fdc  37746  prdstotbnd  37795  isdrngo1  37957  ispridl  38035  ismaxidl  38041  impor  38082  selconj  38101  tradd  38106  scott0f  38170  r2alan  38245  inxpss3  38309  idinxpssinxp2  38313  idinxpssinxp3  38314  dfrel5  38335  ineleq  38343  moantr  38353  dfxrn2  38365  inxpxrn  38388  rnxrnres  38392  coss1cnvres  38415  1cossres  38427  cocossss  38434  cossssid4  38468  cossssid5  38469  cosscnvssid5  38476  cossid  38478  dfssr2  38497  cnvrefrelcoss2  38535  cosselcnvrefrels2  38536  eqvrelcoss  38615  eqvrelcoss2  38617  dfcoeleqvrel  38620  refrelredund4  38633  cnvepresdmqs  38652  dfcomember  38671  dfdisjALTV  38712  dfeldisj3  38718  dfeldisj4  38719  dfeldisj5  38720  disjres  38743  prter1  38879  islshp  38979  islshpat  39017  lcvbr2  39022  lcvnbtwn2  39027  cvrnbtwn3  39276  isatl  39299  ishlat1  39352  ishlat2  39353  cvrat4  39444  pmapglbx  39770  lhpexle3  40013  dib1dim  41166  diblsmopel  41172  lcfls1lem  41535  prjsperref  42601  prjspeclsp  42607  euabsn2w  42674  rexrabdioph  42789  dford4  43025  onsupuni  43225  dflim6  43260  tfsconcatlem  43332  naddgeoa  43390  ifpdfor2  43457  ifpdfan2  43459  ifpdfor  43461  ifpdfan  43462  ifpnot23b  43478  ifpnot23c  43480  ifpnot23d  43481  ifpim123g  43496  ifpbibib  43506  clss2lem  43607  imaiun1  43647  coiun1  43648  brfvrcld2  43688  iunrelexp0  43698  brtrclfv2  43723  snhesn  43782  dffrege76  43935  frege97  43956  frege98  43957  frege109  43968  frege110  43969  dffrege115  43974  frege131  43990  frege133  43992  ntrneineine1lem  44080  ntrneiel2  44082  ntrneiiso  44087  gneispace3  44129  scotteld  44242  ismnuprim  44290  ismnushort  44297  dfuniv2  44298  pm11.52  44383  pm11.58  44386  pm13.192  44406  impexpdcom  44512  sbc3or  44529  opelopab4  44548  uunT12p1  44796  uunT12p2  44797  uunT12p3  44798  uun2221  44809  uun2221p1  44810  uun2221p2  44811  undif3VD  44878  modelaxreplem3  44977  permaxext  45002  permac8prim  45011  ndisj2  45052  nssrex  45087  rabssf  45120  bothtbothsame  46904  bothfbothsame  46905  aiffbtbat  46913  reuabaiotaiota  47092  2reu8i  47118  2reuimp0  47119  ichn  47461  dfodd2  47641  dfeven5  47671  dfodd7  47672  1nevenALTV  47696  oddprmne2  47720  dfvopnbgr2  47857  isuspgrim0lem  47897  gpg5nbgrvtx03starlem1  48063  gpg5nbgrvtx03starlem2  48064  gpg5nbgrvtx03starlem3  48065  gpg5nbgrvtx13starlem1  48066  gpg5nbgrvtx13starlem2  48067  gpg5nbgrvtx13starlem3  48068  islindeps2  48476  isldepslvec2  48478  line2xlem  48746  rmotru  48795  reutru  48796  isnrm4  48923  iscnrm4  48946  homf0  49002  fuco2el  49305  isthincd2  49430  thinccic  49464  istermc2  49468  istermc3  49469  dftermc3  49524  setrec1lem3  49682  aacllem  49794