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  641  mpbiran  708  biadaniALT  820  imor  852  imimorb  951  pm5.6  1002  nbi2  1016  casesifp  1078  3ancoma  1098  3ancomb  1099  3anrev  1101  dfnan2  1491  nannan  1494  nanbi  1497  xorcom  1511  xorneg  1520  xorbi12i  1521  norcom  1527  noran  1529  norasslem1  1531  trunortru  1586  trunorfal  1587  cadan  1606  cadcomb  1610  nic-ax  1671  nic-axALT  1672  nf3  1784  nfnbiOLD  1854  19.43  1881  equsv  2002  sbrimvw  2091  sbcom2  2174  sb5  2277  nf5  2286  nf6  2287  sbrim  2308  sbnf  2316  sb6x  2472  2sb5rf  2480  2sb6rf  2481  sb4b  2483  sb5f  2506  sbequ8  2509  sbhb  2529  eu6lem  2576  eu1  2613  iseqsetv-cleq  2809  issettru  2822  iseqsetv-clel  2823  issetlem  2824  cleqh  2874  cleqf  2940  sbabel  2944  necon3bii  2999  neor  3040  neorian  3043  rextru  3083  r19.26m  3116  r19.43  3128  r2allem  3148  r19.23t  3261  ralcom4  3292  rexcomOLD  3297  moel  3410  moelOLD  3413  rabid2f  3476  rabid2OLD  3479  eqv  3498  eqvf  3499  ralv  3516  rexv  3517  reuv  3518  rmov  3519  rexcom4b  3521  ceqsex4v  3550  ceqsex8v  3552  ceqsrexv  3668  rexab  3716  ralrab2  3720  rexrab2  3722  reu2  3747  reu3  3749  reueq  3759  2reuswap  3768  2reuswap2  3769  reuind  3775  2reu5lem3  3779  2rmoswap  3783  rmo2  3909  rmoanim  3916  rmoanimALT  3917  dfss3  3997  dfss3f  4000  ssabral  4088  rabss  4095  ssrabeq  4107  uniiunlem  4110  sspsstri  4128  npss  4136  dfdif3OLD  4141  raldifb  4172  uncom  4181  inass  4249  elsymdifxor  4279  nsspssun  4287  dfss4  4288  dfun2  4289  dfin2  4290  indi  4303  reupick3  4349  eq0f  4370  neq0f  4371  eq0  4373  eq0ALT  4374  dfnf5  4405  rabn0  4412  csbab  4463  vss  4469  disj  4473  disj3  4477  undisj1  4485  undisj2  4486  inundif  4502  undif  4505  undifr  4506  rabsssn  4690  exsnrex  4704  euabsn2  4750  euabsn  4751  raldifsni  4820  tppreqb  4830  pwpw0  4838  prssg  4844  ssunsn  4853  preqsn  4886  pwpr  4925  dfuni2  4933  unissb  4963  unissbOLD  4964  elint2  4977  ssint  4988  uniintab  5010  dfiin2g  5055  iunid  5083  iunn0  5090  iunxun  5117  iunxiun  5120  iinpw  5129  disjor  5148  disjxiun  5163  dftr2  5285  dftr5OLD  5288  dftr3  5289  dftr4  5290  axrep6  5310  vnex  5332  inuni  5368  eusv2  5414  reusv2lem4  5419  rexxfr  5434  sspwb  5469  opthneg  5501  pwssun  5590  dfid3  5596  dffr6  5655  dffr2  5661  dffr2ALT  5662  opthprc  5764  elxp3  5766  xpiundir  5771  elvv  5774  reliun  5840  inxpOLD  5857  raliunxp  5864  cnvuni  5911  dmopab2rex  5942  dm0rn0  5949  dfres3  6014  ssdmres  6042  elidinxp  6073  idinxpres  6076  dfima2  6091  args  6122  dffr3  6129  cotrg  6139  cotrgOLD  6140  cotrgOLDOLD  6141  intasym  6147  asymref  6148  intirr  6150  xpnz  6190  xp11  6206  ssrnres  6209  xpimasn  6216  coiun  6287  coass  6296  cnvso  6319  elsnxp  6322  dfpo2  6327  imaindm  6330  dffr4  6352  dfse3  6368  frpoind  6374  wfiOLD  6383  dflim2  6452  orddif  6491  dffun2OLDOLD  6585  dffun6  6586  dffun6f  6591  dffun7  6605  dffun9  6607  funfn  6608  svrelfun  6650  mptfnf  6715  dffn2  6749  dffn3  6759  fint  6800  dffn4  6840  dff1o4  6870  brprcneu  6910  brprcneuALT  6911  eqfnfv3  7066  fnreseql  7081  fsn  7169  ftpg  7190  abrexco  7281  imaiun  7282  dff13  7292  isof1oidb  7360  isof1oopb  7361  isocnv2  7367  eloprabga  7558  mpo2eqb  7582  elovmpo  7695  sorpss  7763  abexex  8012  elxp6  8064  elxp7  8065  releldm2  8084  opiota  8100  fnmpo  8110  frxp  8167  frxp2  8185  soseq  8200  cnvimadfsn  8213  mpoxneldm  8253  dftpos4  8286  frrlem9  8335  wfrlem8OLD  8372  wfrfunOLD  8375  dfrecs3  8428  dfrecs3OLD  8429  tfrlem7  8439  ondif1  8557  oarec  8618  oeeu  8659  brinxper  8792  0er  8801  eroveu  8870  erovlem  8871  elixpconst  8963  domen  9021  brsdom  9035  brdom2  9042  reuen1  9090  sbthlem10  9158  brsdom2  9163  xpf1o  9205  unfi  9238  sbthfilem  9264  onfin2  9294  0sdom1domALT  9302  modom  9307  marypha2lem3  9506  wemapsolem  9619  elom3  9717  dfom5  9719  brttrcl2  9783  ttrcltr  9785  ttrclse  9796  trcl  9797  epfrs  9800  frind  9819  rankf  9863  scottexs  9956  scott0s  9957  cplem1  9958  hta  9966  djuexb  9978  pm54.43lem  10069  alephsuc2  10149  iscard3  10162  aceq0  10187  aceq3lem  10189  dfac3  10190  dfac5lem2  10193  dfac5  10198  dfac7  10202  dfac12a  10218  kmlem12  10231  kmlem14  10233  kmlem15  10234  infmap2  10286  ackbij2  10311  dfacfin7  10468  ituniiun  10491  zorng  10573  brdom7disj  10600  entri2  10627  alephreg  10651  fpwwe2lem11  10710  fpwwe2lem12  10711  pwfseqlem1  10727  grutsk  10891  axgroth4  10901  grothprim  10903  grothtsk  10904  elni2  10946  ltsopi  10957  genpass  11078  psslinpr  11100  ltexprlem4  11108  ltresr  11209  1re  11290  infm3  12254  elnnz  12649  dfz2  12658  2rexuz  12965  nnwos  12980  eluz2b1  12984  qexALT  13029  elxr  13179  dflt2  13210  xrsupss  13371  xrinfmss  13372  elixx1  13416  elioo2  13448  dfrp2  13456  elioopnf  13503  elicopnf  13505  elfz1  13572  fznn  13652  fzp1nel  13668  fznn0  13676  preduz  13707  prinfzo0  13755  injresinj  13838  nn0opthlem1  14317  faclbnd4lem1  14342  hashfxnn0  14386  hashprdifel  14447  hashgt23el  14473  hashfun  14486  hashf1  14506  fz1isolem  14510  f1oun2prg  14966  brtrclfv  15051  shftdm  15120  rediv  15180  imdiv  15187  rexanre  15395  caubnd  15407  climreu  15602  prodmo  15984  dvdslelem  16357  3dvdsdec  16380  3dvds2dec  16381  bitsval  16470  smueqlem  16536  algcvgblem  16624  lcmfunsnlem2  16687  isprm2  16729  isprm3  16730  isprm4  16731  pythagtriplem2  16864  elgz  16978  hashbc0  17052  0ram  17067  isstruct  17199  issect  17814  isfull2  17978  isfth2  17982  fucinv  18043  eldmcoa  18132  isdrs  18371  submacs  18862  isnsg4  19207  isgim  19302  gaorb  19347  oppgid  19399  oppgsubm  19405  oppgcntz  19407  ispgp  19634  efgsdm  19772  efgcpbllema  19796  iscyg2  19924  isrng  20181  isring  20264  isirred2  20447  opprirred  20448  isrnghm  20467  dfrhm2  20500  isnzr2  20544  opprsubrng  20585  opprsubrg  20621  isdomn3  20737  drngid2  20774  issdrg  20811  islmod  20884  lss1d  20984  islmhm  21049  islmim  21084  lbsextlem2  21184  lidlnz  21275  dfprm2  21507  isphl  21669  elocv  21709  iunocv  21722  isobs  21763  islinds  21852  1mavmul  22575  toprntopon  22952  isbasis3g  22977  fctop  23032  cctop  23034  isclo2  23117  restsn  23199  lmbr  23287  ist0-3  23374  2ndcdisj  23485  1stccnp  23491  islocfin  23546  1stckgenlem  23582  txbas  23596  ptbasin  23606  tx2cn  23639  fbfinnfr  23870  fbasrn  23913  filuni  23914  ufinffr  23958  fin1aufil  23961  rnelfmlem  23981  flimrest  24012  alexsubALTlem3  24078  alexsubALTlem4  24079  tgphaus  24146  istlm  24214  iscusp2  24332  metuel2  24599  isngp2  24631  isnlm  24717  isphtpc  25045  phtpcer  25046  om1elbas  25084  isclm  25116  iscvsp  25180  iscph  25223  iscau3  25331  minveclem3b  25481  elovolm  25529  ioombl1lem4  25615  dyaddisj  25650  vitali  25667  itg1climres  25769  itg2seq  25797  itg2monolem1  25805  itg2mono  25808  limcrcl  25929  lhop1  26073  itgsubst  26110  mdegleb  26123  isuc1p  26200  ismon1p  26202  plydivex  26357  ellogdm  26699  1cubr  26903  atandm2  26938  birthdaylem3  27014  dmarea  27018  dchrelbas2  27299  dchrelbas4  27305  elno3  27718  nosgnn0  27721  nosepon  27728  nocvxminlem  27840  scutcut  27864  scutbday  27867  dmscut  27874  scutf  27875  sltrec  27883  made0  27930  addsprop  28027  negsproplem2  28079  negsprop  28085  mulsprop  28174  precsexlem10  28258  elzs2  28403  elnnzs  28405  recut  28446  0reno  28447  axcontlem7  29003  nb3grpr  29417  nb3grpr2  29418  upgrwlkcompim  29679  wlkson  29692  wlkonprop  29694  wksonproplem  29740  wksonproplemOLD  29741  ispth  29759  wwlknon  29890  wwlksnextinj  29932  wspthsnwspthsnon  29949  elwspths2spth  30000  rusgrnumwwlkl1  30001  clwwlkccatlem  30021  erclwwlkref  30052  frgr3v  30307  nmoubi  30804  nmobndseqi  30811  nmobndseqiALT  30812  minvecolem1  30906  isch2  31255  hlimreui  31271  isch3  31273  ocsh  31315  dfch2  31439  spanuni  31576  nonbooli  31683  5oalem7  31692  adjsym  31865  elbdop2  31903  dmadjss  31919  nmopub  31940  nmfnleub  31957  nmop0h  32023  pjssposi  32204  pjordi  32205  cvbr2  32315  cvnbtwn2  32319  mdsl2i  32354  cvmdi  32356  elat2  32372  atom1d  32385  chirredi  32426  cdj3i  32473  or3di  32488  opreu2reu1  32512  mo5f  32517  reuxfrdf  32519  rexunirn  32520  difrab2  32526  rabsspr  32529  rabsstp  32530  iuninc  32583  disjorf  32601  disjunsn  32616  rabfmpunirn  32671  aciunf1  32681  funcnv5mpt  32686  eliccelico  32782  elicoelioo  32783  isomnd  33051  omndmul2  33062  isslmd  33181  islinds5  33360  ismxidl  33455  1arithufdlem4  33540  hasheuni  34049  pwsiga  34094  sigainb  34100  issros  34139  2ndmbfm  34226  omssubaddlem  34264  omssubadd  34265  sitgaddlemb  34313  eulerpartlemgvv  34341  eulerpartlemn  34346  probun  34384  ballotlem2  34453  ballotlemodife  34462  bnj252  34679  bnj253  34680  bnj255  34681  bnj345  34690  bnj133  34703  bnj976  34753  bnj1098  34759  bnj121  34846  bnj130  34850  bnj150  34852  bnj581  34884  bnj607  34892  bnj865  34899  bnj917  34910  bnj934  34911  bnj964  34919  bnj983  34927  bnj996  34932  bnj1021  34942  bnj1033  34945  bnj1047  34949  bnj1049  34950  bnj1090  34955  bnj1128  34966  bnj1175  34980  bnj1189  34985  bnj1253  34993  bnj1312  35034  exdifsn  35055  fineqvrep  35071  fineqvac  35073  erdszelem9  35167  erdszelem10  35168  pconnconn  35199  cvmliftiota  35269  fmlaomn0  35358  fmla0disjsuc  35366  fmlasucdisj  35367  dmopab3rexdif  35373  elmthm  35544  nepss  35680  xpab  35688  dfso2  35717  elrn3  35724  elpotr  35745  dfon2lem5  35751  dfon2lem7  35753  dfon2lem8  35754  elwlim  35787  wzel  35788  brtxp2  35845  brpprod3a  35850  eltrans  35855  dfon3  35856  dffix2  35869  dffun10  35878  elfuns  35879  brsingle  35881  brimg  35901  funpartfun  35907  funpartfv  35909  cgrxfr  36019  segletr  36078  outsideoftr  36093  neifg  36337  filnetlem4  36347  df3nandALT1  36365  weiunlem2  36429  bj-consensusALT  36545  bj-df-ifc  36546  bj-biexal3  36673  bj-nfnnfTEMP  36724  bj-denoteslem  36837  bj-denotesALTV  36838  bj-ralvw  36845  bj-rexvw  36846  bj-rexcom4bv  36848  bj-rexcom4b  36849  bj-sbeq  36867  bj-inrab  36893  bj-rcleqf  36991  bj-dfmpoa  37084  bj-imdirco  37156  topdifinffinlem  37313  topdifinfeq  37316  relowlssretop  37329  relowlpssretop  37330  rdgeqoa  37336  domalom  37370  nlpineqsn  37374  fvineqsneq  37378  wl-ifpimpr  37432  wl-df3xor3  37436  wl-3xorbi  37439  wl-3xorbi2  37440  wl-2xor  37449  wl-2mintru2  37457  wl-dfclab  37550  rabiun  37553  phpreu  37564  fin2solem  37566  matunitlindflem2  37577  ptrest  37579  poimirlem25  37605  poimirlem27  37607  poimirlem30  37610  ismblfin  37621  ovoliunnfl  37622  voliunnfl  37624  volsupnfl  37625  itg2addnclem2  37632  fdc  37705  prdstotbnd  37754  isdrngo1  37916  ispridl  37994  ismaxidl  38000  impor  38041  selconj  38060  tradd  38065  scott0f  38129  r2alan  38205  inxpss3  38270  idinxpssinxp2  38274  idinxpssinxp3  38275  dfrel5  38302  ineleq  38310  moantr  38320  dfxrn2  38332  inxpxrn  38351  rnxrnres  38355  coss1cnvres  38373  1cossres  38385  cocossss  38392  cossssid4  38426  cossssid5  38427  cosscnvssid5  38434  cossid  38436  dfssr2  38455  cnvrefrelcoss2  38493  cosselcnvrefrels2  38494  eqvrelcoss  38573  eqvrelcoss2  38575  dfcoeleqvrel  38578  refrelredund4  38591  cnvepresdmqs  38609  dfcomember  38628  dfdisjALTV  38669  dfeldisj3  38675  dfeldisj4  38676  dfeldisj5  38677  disjres  38700  prter1  38835  islshp  38935  islshpat  38973  lcvbr2  38978  lcvnbtwn2  38983  cvrnbtwn3  39232  isatl  39255  ishlat1  39308  ishlat2  39309  cvrat4  39400  pmapglbx  39726  lhpexle3  39969  dib1dim  41122  diblsmopel  41128  lcfls1lem  41491  prjsperref  42561  prjspeclsp  42567  euabsn2w  42634  rexrabdioph  42750  dford4  42986  onsupuni  43190  dflim6  43226  tfsconcatlem  43298  naddgeoa  43356  ifpdfor2  43423  ifpdfan2  43425  ifpdfor  43427  ifpdfan  43428  ifpnot23b  43444  ifpnot23c  43446  ifpnot23d  43447  ifpim123g  43462  ifpbibib  43472  clss2lem  43573  imaiun1  43613  coiun1  43614  brfvrcld2  43654  iunrelexp0  43664  brtrclfv2  43689  snhesn  43748  dffrege76  43901  frege97  43922  frege98  43923  frege109  43934  frege110  43935  dffrege115  43940  frege131  43956  frege133  43958  ntrneineine1lem  44046  ntrneiel2  44048  ntrneiiso  44053  gneispace3  44095  scotteld  44215  ismnuprim  44263  ismnushort  44270  dfuniv2  44271  pm11.52  44356  pm11.58  44359  pm13.192  44379  impexpdcom  44486  sbc3or  44503  opelopab4  44522  uunT12p1  44771  uunT12p2  44772  uunT12p3  44773  uun2221  44784  uun2221p1  44785  uun2221p2  44786  undif3VD  44853  ndisj2  44953  nssrex  44988  rabssf  45021  bothtbothsame  46814  bothfbothsame  46815  aiffbtbat  46823  reuabaiotaiota  47002  2reu8i  47028  2reuimp0  47029  ichn  47330  dfodd2  47510  dfeven5  47540  dfodd7  47541  1nevenALTV  47565  oddprmne2  47589  dfvopnbgr2  47725  isuspgrim0lem  47755  islindeps2  48212  isldepslvec2  48214  line2xlem  48487  rmotru  48536  reutru  48537  isnrm4  48610  iscnrm4  48634  isthincd2  48705  thinccic  48728  setrec1lem3  48781  aacllem  48895