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  1495  nannan  1498  nanbi  1501  xorcom  1515  xorneg  1524  xorbi12i  1525  norcom  1531  noran  1533  norasslem1  1535  trunortru  1590  trunorfal  1591  cadan  1610  cadcomb  1614  nic-ax  1674  nic-axALT  1675  nf3  1787  19.43  1883  equsv  2004  sbrimvw  2096  sbcom2  2178  sb5  2282  nf5  2288  nf6  2289  sbrim  2310  sbnf  2317  sb6x  2468  2sb5rf  2476  2sb6rf  2477  sb4b  2479  sb5f  2502  sbequ8  2505  sbhb  2525  eu6lem  2573  eu1  2610  iseqsetv-cleq  2800  issettru  2814  iseqsetv-clel  2815  issetlem  2816  cleqh  2865  cleqf  2927  sbabel  2931  necon3bii  2984  neor  3024  neorian  3027  rextru  3067  r19.26m  3095  r19.43  3104  3r19.43  3105  r2allem  3124  r19.23t  3232  ralcom4  3262  moel  3370  rabid2f  3430  eqv  3450  eqvf  3451  ralv  3467  rexv  3468  reuv  3469  rmov  3470  rexcom4b  3472  ceqsex4v  3496  ceqsex8v  3498  ceqsrexv  3609  rexab  3653  ralrab2  3656  rexrab2  3658  reu2  3683  reu3  3685  reueq  3695  2reuswap  3704  2reuswap2  3705  reuind  3711  2reu5lem3  3715  2rmoswap  3719  rmo2  3837  rmoanim  3844  rmoanimALT  3845  dfss3  3922  dfss3f  3925  ssabral  4016  rabss  4022  ssrabeq  4036  uniiunlem  4039  sspsstri  4057  npss  4065  dfdif3OLD  4070  raldifb  4101  uncom  4110  inass  4180  elsymdifxor  4212  nsspssun  4220  dfss4  4221  dfun2  4222  dfin2  4223  indi  4236  reupick3  4282  eq0f  4299  neq0f  4300  eq0ALT  4303  dfnf5  4334  rabn0  4341  csbab  4392  vss  4398  disj  4402  disj3  4406  undisj1  4414  undisj2  4415  inundif  4431  undif  4434  undifr  4435  rabsssn  4625  exsnrex  4637  euabsn2  4682  euabsn  4683  raldifsni  4751  tppreqb  4761  pwpw0  4769  prssg  4775  ssunsn  4784  prneimg2  4811  preqsn  4818  pwpr  4857  dfuni2  4865  unissb  4896  elint2  4909  ssint  4919  uniintab  4941  dfiin2g  4986  iunid  5016  iunn0  5022  iunxun  5049  iunxiun  5052  iinpw  5061  disjor  5080  disjxiun  5095  dftr2  5207  dftr3  5210  dftr4  5211  axrep6OLD  5234  vnex  5259  inuni  5295  eusv2  5341  reusv2lem4  5346  rexxfr  5361  sspwb  5397  opthneg  5429  pwssun  5516  dfid3  5522  dffr6  5580  dffr2  5585  dffr2ALT  5586  opthprc  5688  elxp3  5690  xpiundir  5696  elvv  5699  inxpOLD  5781  raliunxp  5788  cnvuni  5835  dmopab2rex  5866  dm0rn0OLD  5874  dfres3  5943  ssdmres  5972  elidinxp  6003  idinxpres  6006  dfima2  6021  args  6051  dffr3  6058  cotrg  6068  intasym  6072  asymref  6073  intirr  6075  xpnz  6117  xp11  6133  ssrnres  6136  xpimasn  6143  coiun  6215  coass  6224  cnvso  6246  elsnxp  6249  dfpo2  6254  imaindm  6257  dffr4  6278  dfse3  6294  frpoind  6300  dflim2  6375  orddif  6415  dffun6  6503  dffun6f  6507  dffun7  6519  dffun9  6521  funfn  6522  svrelfun  6564  mptfnf  6627  dffn2  6664  dffn3  6674  fint  6713  dffn4  6752  dff1o4  6782  brprcneu  6824  brprcneuALT  6825  eqfnfv3  6978  fnreseql  6993  fsn  7080  ftpg  7101  abrexco  7190  imaiun  7191  dff13  7200  isof1oidb  7270  isof1oopb  7271  isocnv2  7277  eloprabga  7467  mpo2eqb  7490  elovmpo  7603  sorpss  7673  abexex  7915  elxp6  7967  elxp7  7968  releldm2  7987  opiota  8003  fnmpo  8013  frxp  8068  frxp2  8086  soseq  8101  cnvimadfsn  8114  mpoxneldm  8154  dftpos4  8187  frrlem9  8236  dfrecs3  8304  tfrlem7  8314  ondif1  8428  oarec  8489  oeeu  8531  brinxper  8664  0er  8673  eroveu  8749  erovlem  8750  elixpconst  8843  domen  8898  brsdom  8911  brdom2  8919  reuen1  8963  sbthlem10  9024  brsdom2  9029  xpf1o  9067  unfi  9095  sbthfilem  9122  onfin2  9141  0sdom1domALT  9147  modom  9151  marypha2lem3  9340  wemapsolem  9455  elom3  9557  dfom5  9559  brttrcl2  9623  ttrcltr  9625  ttrclse  9636  trcl  9637  epfrs  9640  frind  9662  rankf  9706  scottexs  9799  scott0s  9800  cplem1  9801  hta  9809  djuexb  9821  pm54.43lem  9912  alephsuc2  9990  iscard3  10003  aceq0  10028  aceq3lem  10030  dfac3  10031  dfac5lem2  10034  dfac5  10039  dfac7  10043  dfac12a  10059  kmlem12  10072  kmlem14  10074  kmlem15  10075  infmap2  10127  ackbij2  10152  dfacfin7  10309  ituniiun  10332  zorng  10414  brdom7disj  10441  entri2  10468  alephreg  10493  fpwwe2lem11  10552  fpwwe2lem12  10553  pwfseqlem1  10569  grutsk  10733  axgroth4  10743  grothprim  10745  grothtsk  10746  elni2  10788  ltsopi  10799  genpass  10920  psslinpr  10942  ltexprlem4  10950  ltresr  11051  infm3  12101  elnnz  12498  dfz2  12507  2rexuz  12813  nnwos  12828  eluz2b1  12832  qexALT  12877  elxr  13030  dflt2  13062  xrsupss  13224  xrinfmss  13225  elixx1  13270  elioo2  13302  dfrp2  13310  elioopnf  13359  elicopnf  13361  elfz1  13428  fznn  13508  fzp1nel  13527  fznn0  13535  preduz  13566  prinfzo0  13614  injresinj  13707  nn0opthlem1  14191  faclbnd4lem1  14216  hashfxnn0  14260  hashprdifel  14321  hashgt23el  14347  hashfun  14360  hashf1  14380  fz1isolem  14384  f1oun2prg  14840  brtrclfv  14925  shftdm  14994  rediv  15054  imdiv  15061  rexanre  15270  caubnd  15282  climreu  15479  prodmo  15859  dvdslelem  16236  3dvdsdec  16259  3dvds2dec  16260  bitsval  16351  smueqlem  16417  algcvgblem  16504  lcmfunsnlem2  16567  isprm2  16609  isprm3  16610  isprm4  16611  pythagtriplem2  16745  elgz  16859  hashbc0  16933  0ram  16948  isstruct  17079  issect  17677  isfull2  17837  isfth2  17841  fucinv  17900  eldmcoa  17989  isdrs  18224  submacs  18752  isnsg4  19096  isgim  19191  gaorb  19236  oppgid  19285  oppgsubm  19291  oppgcntz  19293  ispgp  19521  efgsdm  19659  efgcpbllema  19683  iscyg2  19811  isomnd  20052  omndmul2  20062  isrng  20089  isring  20172  isirred2  20357  opprirred  20358  isrnghm  20377  dfrhm2  20410  isnzr2  20451  opprsubrng  20492  opprsubrg  20526  isdomn3  20648  drngid2  20685  issdrg  20721  islmod  20815  lss1d  20914  islmhm  20979  islmim  21014  lbsextlem2  21114  lidlnz  21197  dfprm2  21428  isphl  21583  elocv  21623  iunocv  21636  isobs  21675  islinds  21764  1mavmul  22492  toprntopon  22869  isbasis3g  22893  fctop  22948  cctop  22950  isclo2  23032  restsn  23114  lmbr  23202  ist0-3  23289  2ndcdisj  23400  1stccnp  23406  islocfin  23461  1stckgenlem  23497  txbas  23511  ptbasin  23521  tx2cn  23554  fbfinnfr  23785  fbasrn  23828  filuni  23829  ufinffr  23873  fin1aufil  23876  rnelfmlem  23896  flimrest  23927  alexsubALTlem3  23993  alexsubALTlem4  23994  tgphaus  24061  istlm  24129  iscusp2  24245  metuel2  24509  isngp2  24541  isnlm  24619  isphtpc  24949  phtpcer  24950  om1elbas  24988  isclm  25020  iscvsp  25084  iscph  25126  iscau3  25234  minveclem3b  25384  elovolm  25432  ioombl1lem4  25518  dyaddisj  25553  vitali  25570  itg1climres  25671  itg2seq  25699  itg2monolem1  25707  itg2mono  25710  limcrcl  25831  lhop1  25975  itgsubst  26012  mdegleb  26025  isuc1p  26102  ismon1p  26104  plydivex  26261  ellogdm  26604  1cubr  26808  atandm2  26843  birthdaylem3  26919  dmarea  26923  dchrelbas2  27204  dchrelbas4  27210  elno3  27623  nosgnn0  27626  nosepon  27633  nocvxminlem  27750  cutcuts  27777  cutbday  27780  dmcuts  27787  cutsf  27788  ltsrec  27797  made0  27859  addsprop  27972  negsproplem2  28025  negsprop  28031  mulsprop  28126  precsexlem10  28212  elzs2  28395  elnnzs  28397  bdayfinbndlem1  28463  recut  28490  axcontlem7  29043  nb3grpr  29455  nb3grpr2  29456  upgrwlkcompim  29716  wlkson  29728  wlkonprop  29730  wksonproplem  29776  ispth  29794  wwlknon  29930  wwlksnextinj  29972  wspthsnwspthsnon  29989  elwspths2spth  30043  rusgrnumwwlkl1  30044  clwwlkccatlem  30064  erclwwlkref  30095  frgr3v  30350  nmoubi  30847  nmobndseqi  30854  nmobndseqiALT  30855  minvecolem1  30949  isch2  31298  hlimreui  31314  isch3  31316  ocsh  31358  dfch2  31482  spanuni  31619  nonbooli  31726  5oalem7  31735  adjsym  31908  elbdop2  31946  dmadjss  31962  nmopub  31983  nmfnleub  32000  nmop0h  32066  pjssposi  32247  pjordi  32248  cvbr2  32358  cvnbtwn2  32362  mdsl2i  32397  cvmdi  32399  elat2  32415  atom1d  32428  chirredi  32469  cdj3i  32516  or3di  32533  opreu2reu1  32558  mo5f  32563  reuxfrdf  32565  rexunirn  32566  difrab2  32572  rabsspr  32576  rabsstp  32577  tpssg  32612  iuninc  32635  disjorf  32654  disjunsn  32669  rabfmpunirn  32731  aciunf1  32741  funcnv5mpt  32746  eliccelico  32857  elicoelioo  32858  isslmd  33284  islinds5  33448  ismxidl  33543  1arithufdlem4  33628  hasheuni  34242  pwsiga  34287  sigainb  34293  issros  34332  2ndmbfm  34418  omssubaddlem  34456  omssubadd  34457  sitgaddlemb  34505  eulerpartlemgvv  34533  eulerpartlemn  34538  probun  34576  ballotlem2  34646  ballotlemodife  34655  bnj252  34859  bnj253  34860  bnj255  34861  bnj345  34870  bnj133  34883  bnj976  34933  bnj1098  34939  bnj121  35026  bnj130  35030  bnj150  35032  bnj581  35064  bnj607  35072  bnj865  35079  bnj917  35090  bnj934  35091  bnj964  35099  bnj983  35107  bnj996  35112  bnj1021  35122  bnj1033  35125  bnj1047  35129  bnj1049  35130  bnj1090  35135  bnj1128  35146  bnj1175  35160  bnj1189  35165  bnj1253  35173  bnj1312  35214  exdifsn  35235  fineqvrep  35270  fineqvac  35272  onvf1odlem4  35300  vonf1owev  35302  erdszelem9  35393  erdszelem10  35394  pconnconn  35425  cvmliftiota  35495  fmlaomn0  35584  fmla0disjsuc  35592  fmlasucdisj  35593  dmopab3rexdif  35599  elmthm  35770  antnestALT  35888  nepss  35912  xpab  35920  dfso2  35949  elrn3  35956  elpotr  35973  dfon2lem5  35979  dfon2lem7  35981  dfon2lem8  35982  elwlim  36015  wzel  36016  brtxp2  36073  brpprod3a  36078  eltrans  36083  dfon3  36084  dffix2  36097  dffun10  36106  elfuns  36107  brsingle  36109  brimg  36129  funpartfun  36137  funpartfv  36139  cgrxfr  36249  segletr  36308  outsideoftr  36323  neifg  36565  filnetlem4  36575  df3nandALT1  36593  weiunlem  36657  bj-consensusALT  36779  bj-df-ifc  36780  bj-biexal3  36908  bj-nfnnfTEMP  36959  bj-denoteslem  37072  bj-denotesALTV  37073  bj-ralvw  37080  bj-rexvw  37081  bj-rexcom4bv  37083  bj-rexcom4b  37084  bj-sbeq  37102  bj-inrab  37128  bj-rcleqf  37226  bj-dfmpoa  37323  bj-imdirco  37395  topdifinffinlem  37552  topdifinfeq  37555  relowlssretop  37568  relowlpssretop  37569  rdgeqoa  37575  domalom  37609  nlpineqsn  37613  fvineqsneq  37617  wl-ifpimpr  37671  wl-df3xor3  37675  wl-3xorbi  37678  wl-3xorbi2  37679  wl-2xor  37688  wl-2mintru2  37696  wl-dfclab  37790  rabiun  37794  phpreu  37805  fin2solem  37807  matunitlindflem2  37818  ptrest  37820  poimirlem25  37846  poimirlem27  37848  poimirlem30  37851  ismblfin  37862  ovoliunnfl  37863  voliunnfl  37865  volsupnfl  37866  itg2addnclem2  37873  fdc  37946  prdstotbnd  37995  isdrngo1  38157  ispridl  38235  ismaxidl  38241  impor  38282  selconj  38301  tradd  38306  scott0f  38370  r2alan  38447  inxpss3  38513  idinxpssinxp2  38517  idinxpssinxp3  38518  dfrel5  38539  ineleq  38547  moantr  38557  dfxrn2  38570  inxpxrn  38603  rnxrnres  38607  dfsuccl4  38648  coss1cnvres  38680  1cossres  38692  cocossss  38699  cossssid4  38733  cossssid5  38734  cosscnvssid5  38741  cossid  38743  dfssr2  38752  cnvrefrelcoss2  38790  cosselcnvrefrels2  38791  eqvrelcoss  38874  eqvrelcoss2  38876  dfcoeleqvrel  38879  refrelredund4  38892  cnvepresdmqs  38912  dfcomember  38931  dfdisjALTV  38972  dfeldisj3  38978  dfeldisj4  38979  dfeldisj5  38980  disjres  39003  prter1  39139  islshp  39239  islshpat  39277  lcvbr2  39282  lcvnbtwn2  39287  cvrnbtwn3  39536  isatl  39559  ishlat1  39612  ishlat2  39613  cvrat4  39703  pmapglbx  40029  lhpexle3  40272  dib1dim  41425  diblsmopel  41431  lcfls1lem  41794  prjsperref  42849  prjspeclsp  42855  euabsn2w  42922  rexrabdioph  43036  dford4  43271  onsupuni  43471  dflim6  43506  tfsconcatlem  43578  naddgeoa  43636  ifpdfor2  43702  ifpdfan2  43704  ifpdfor  43706  ifpdfan  43707  ifpnot23b  43723  ifpnot23c  43725  ifpnot23d  43726  ifpim123g  43741  ifpbibib  43751  clss2lem  43852  imaiun1  43892  coiun1  43893  brfvrcld2  43933  iunrelexp0  43943  brtrclfv2  43968  snhesn  44027  dffrege76  44180  frege97  44201  frege98  44202  frege109  44213  frege110  44214  dffrege115  44219  frege131  44235  frege133  44237  ntrneineine1lem  44325  ntrneiel2  44327  ntrneiiso  44332  gneispace3  44374  scotteld  44487  ismnuprim  44535  ismnushort  44542  dfuniv2  44543  pm11.52  44628  pm11.58  44631  pm13.192  44651  impexpdcom  44756  sbc3or  44773  opelopab4  44792  uunT12p1  45040  uunT12p2  45041  uunT12p3  45042  uun2221  45053  uun2221p1  45054  uun2221p2  45055  undif3VD  45122  modelaxreplem3  45221  permaxext  45246  permac8prim  45255  ndisj2  45296  nssrex  45330  rabssf  45363  bothtbothsame  47145  bothfbothsame  47146  aiffbtbat  47154  reuabaiotaiota  47333  2reu8i  47359  2reuimp0  47360  ichn  47702  dfodd2  47882  dfeven5  47912  dfodd7  47913  1nevenALTV  47937  oddprmne2  47961  dfvopnbgr2  48099  isuspgrim0lem  48139  gpg5nbgrvtx03starlem1  48314  gpg5nbgrvtx03starlem2  48315  gpg5nbgrvtx03starlem3  48316  gpg5nbgrvtx13starlem1  48317  gpg5nbgrvtx13starlem2  48318  gpg5nbgrvtx13starlem3  48319  gpg5edgnedg  48376  islindeps2  48729  isldepslvec2  48731  line2xlem  48999  rmotru  49048  reutru  49049  isnrm4  49176  iscnrm4  49199  homf0  49254  fuco2el  49557  isthincd2  49682  thinccic  49716  istermc2  49720  istermc3  49721  dftermc3  49776  setrec1lem3  49934  aacllem  50046