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  643  mpbiran  710  biadaniALT  821  imor  854  imimorb  953  pm5.6  1004  nbi2  1018  casesifp  1078  3ancoma  1098  3ancomb  1099  3anrev  1101  dfnan2  1496  nannan  1499  nanbi  1502  xorcom  1516  xorneg  1525  xorbi12i  1526  norcom  1532  noran  1534  norasslem1  1536  trunortru  1591  trunorfal  1592  cadan  1611  cadcomb  1615  nic-ax  1675  nic-axALT  1676  nf3  1788  19.43  1884  equsv  2005  sbrimvw  2097  sbcom2  2179  sb5  2283  nf5  2289  nf6  2290  sbrim  2311  sbnf  2318  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  3068  r19.26m  3096  r19.43  3105  3r19.43  3106  r2allem  3125  r19.23t  3233  ralcom4  3263  moel  3362  rabid2f  3420  eqv  3439  eqvf  3440  ralv  3456  rexv  3457  reuv  3458  rmov  3459  rexcom4b  3461  ceqsex4v  3484  ceqsex8v  3486  ceqsrexv  3597  rexab  3641  ralrab2  3644  rexrab2  3646  reu2  3671  reu3  3673  reueq  3683  2reuswap  3692  2reuswap2  3693  reuind  3699  2reu5lem3  3703  2rmoswap  3707  rmo2  3825  rmoanim  3832  rmoanimALT  3833  dfss3  3910  dfss3f  3913  ssabral  4004  rabss  4010  ssrabeq  4024  uniiunlem  4027  sspsstri  4045  npss  4053  dfdif3OLD  4058  raldifb  4089  uncom  4098  inass  4168  elsymdifxor  4200  nsspssun  4208  dfss4  4209  dfun2  4210  dfin2  4211  indi  4224  reupick3  4270  eq0f  4287  neq0f  4288  eq0ALT  4291  dfnf5  4322  rabn0  4329  csbab  4380  vss  4386  disj  4390  disj3  4394  undisj1  4402  undisj2  4403  inundif  4419  undif  4422  undifr  4423  rabsssn  4612  exsnrex  4624  euabsn2  4669  euabsn  4670  raldifsni  4740  tppreqb  4750  pwpw0  4756  prssg  4762  ssunsn  4771  prneimg2  4798  preqsn  4805  pwpr  4844  dfuni2  4852  unissb  4883  elint2  4896  ssint  4906  uniintab  4928  dfiin2g  4973  iunid  5003  iunn0  5009  iunxun  5036  iunxiun  5039  iinpw  5048  disjor  5067  disjxiun  5082  dftr2  5194  dftr3  5197  dftr4  5198  axrep6OLD  5222  vnexOLD  5253  inuni  5291  eusv2  5338  reusv2lem4  5343  rexxfr  5358  sspwb  5401  opthneg  5434  pwssun  5523  dfid3  5529  dffr6  5587  dffr2  5592  dffr2ALT  5593  opthprc  5695  elxp3  5697  xpiundir  5703  elvv  5706  raliunxp  5794  cnvuni  5841  dmopab2rex  5872  dm0rn0OLD  5880  dfres3  5949  ssdmres  5978  elidinxp  6009  idinxpres  6012  dfima2  6027  args  6057  dffr3  6064  cotrg  6074  intasym  6078  asymref  6079  intirr  6081  xpnz  6123  xp11  6139  ssrnres  6142  xpimasn  6149  coiun  6221  coass  6230  cnvso  6252  elsnxp  6255  dfpo2  6260  imaindm  6263  dffr4  6284  dfse3  6300  frpoind  6306  dflim2  6381  orddif  6421  dffun6  6509  dffun6f  6513  dffun7  6525  dffun9  6527  funfn  6528  svrelfun  6570  mptfnf  6633  dffn2  6670  dffn3  6680  fint  6719  dffn4  6758  dff1o4  6788  brprcneu  6830  brprcneuALT  6831  eqfnfv3  6985  fnreseql  7000  fsn  7088  ftpg  7110  abrexco  7199  imaiun  7200  dff13  7209  isof1oidb  7279  isof1oopb  7280  isocnv2  7286  eloprabga  7476  mpo2eqb  7499  elovmpo  7612  sorpss  7682  abexex  7924  elxp6  7976  elxp7  7977  releldm2  7996  opiota  8012  fnmpo  8022  frxp  8076  frxp2  8094  soseq  8109  cnvimadfsn  8122  mpoxneldm  8162  dftpos4  8195  frrlem9  8244  dfrecs3  8312  tfrlem7  8322  ondif1  8436  oarec  8497  oeeu  8539  brinxper  8673  0er  8682  eroveu  8759  erovlem  8760  elixpconst  8853  domen  8908  brsdom  8921  brdom2  8929  reuen1  8973  sbthlem10  9034  brsdom2  9039  xpf1o  9077  unfi  9105  sbthfilem  9132  onfin2  9151  0sdom1domALT  9157  modom  9161  marypha2lem3  9350  wemapsolem  9465  elom3  9569  dfom5  9571  brttrcl2  9635  ttrcltr  9637  ttrclse  9648  trcl  9649  epfrs  9652  frind  9674  rankf  9718  scottexs  9811  scott0s  9812  cplem1  9813  hta  9821  djuexb  9833  pm54.43lem  9924  alephsuc2  10002  iscard3  10015  aceq0  10040  aceq3lem  10042  dfac3  10043  dfac5lem2  10046  dfac5  10051  dfac7  10055  dfac12a  10071  kmlem12  10084  kmlem14  10086  kmlem15  10087  infmap2  10139  ackbij2  10164  dfacfin7  10321  ituniiun  10344  zorng  10426  brdom7disj  10453  entri2  10480  alephreg  10505  fpwwe2lem11  10564  fpwwe2lem12  10565  pwfseqlem1  10581  grutsk  10745  axgroth4  10755  grothprim  10757  grothtsk  10758  elni2  10800  ltsopi  10811  genpass  10932  psslinpr  10954  ltexprlem4  10962  ltresr  11063  infm3  12115  elnnz  12534  dfz2  12543  2rexuz  12850  nnwos  12865  eluz2b1  12869  qexALT  12914  elxr  13067  dflt2  13099  xrsupss  13261  xrinfmss  13262  elixx1  13307  elioo2  13339  dfrp2  13347  elioopnf  13396  elicopnf  13398  elfz1  13466  fznn  13546  fzp1nel  13565  fznn0  13573  preduz  13604  prinfzo0  13653  injresinj  13746  nn0opthlem1  14230  faclbnd4lem1  14255  hashfxnn0  14299  hashprdifel  14360  hashgt23el  14386  hashfun  14399  hashf1  14419  fz1isolem  14423  f1oun2prg  14879  brtrclfv  14964  shftdm  15033  rediv  15093  imdiv  15100  rexanre  15309  caubnd  15321  climreu  15518  prodmo  15901  dvdslelem  16278  3dvdsdec  16301  3dvds2dec  16302  bitsval  16393  smueqlem  16459  algcvgblem  16546  lcmfunsnlem2  16609  isprm2  16651  isprm3  16652  isprm4  16653  pythagtriplem2  16788  elgz  16902  hashbc0  16976  0ram  16991  isstruct  17122  issect  17720  isfull2  17880  isfth2  17884  fucinv  17943  eldmcoa  18032  isdrs  18267  submacs  18795  isnsg4  19142  isgim  19237  gaorb  19282  oppgid  19331  oppgsubm  19337  oppgcntz  19339  ispgp  19567  efgsdm  19705  efgcpbllema  19729  iscyg2  19857  isomnd  20098  omndmul2  20108  isrng  20135  isring  20218  isirred2  20401  opprirred  20402  isrnghm  20421  dfrhm2  20454  isnzr2  20495  opprsubrng  20536  opprsubrg  20570  isdomn3  20692  drngid2  20729  issdrg  20765  islmod  20859  lss1d  20958  islmhm  21022  islmim  21057  lbsextlem2  21157  lidlnz  21240  dfprm2  21453  isphl  21608  elocv  21648  iunocv  21661  isobs  21700  islinds  21789  1mavmul  22513  toprntopon  22890  isbasis3g  22914  fctop  22969  cctop  22971  isclo2  23053  restsn  23135  lmbr  23223  ist0-3  23310  2ndcdisj  23421  1stccnp  23427  islocfin  23482  1stckgenlem  23518  txbas  23532  ptbasin  23542  tx2cn  23575  fbfinnfr  23806  fbasrn  23849  filuni  23850  ufinffr  23894  fin1aufil  23897  rnelfmlem  23917  flimrest  23948  alexsubALTlem3  24014  alexsubALTlem4  24015  tgphaus  24082  istlm  24150  iscusp2  24266  metuel2  24530  isngp2  24562  isnlm  24640  isphtpc  24961  phtpcer  24962  om1elbas  24999  isclm  25031  iscvsp  25095  iscph  25137  iscau3  25245  minveclem3b  25395  elovolm  25442  ioombl1lem4  25528  dyaddisj  25563  vitali  25580  itg1climres  25681  itg2seq  25709  itg2monolem1  25717  itg2mono  25720  limcrcl  25841  lhop1  25981  itgsubst  26016  mdegleb  26029  isuc1p  26106  ismon1p  26108  plydivex  26263  ellogdm  26603  1cubr  26806  atandm2  26841  birthdaylem3  26917  dmarea  26921  dchrelbas2  27200  dchrelbas4  27206  elno3  27619  nosgnn0  27622  nosepon  27629  nocvxminlem  27746  cutcuts  27773  cutbday  27776  dmcuts  27783  cutsf  27784  ltsrec  27793  made0  27855  addsprop  27968  negsproplem2  28021  negsprop  28027  mulsprop  28122  precsexlem10  28208  elzs2  28391  elnnzs  28393  bdayfinbndlem1  28459  recut  28486  axcontlem7  29039  nb3grpr  29451  nb3grpr2  29452  upgrwlkcompim  29711  wlkson  29723  wlkonprop  29725  wksonproplem  29771  ispth  29789  wwlknon  29925  wwlksnextinj  29967  wspthsnwspthsnon  29984  elwspths2spth  30038  rusgrnumwwlkl1  30039  clwwlkccatlem  30059  erclwwlkref  30090  frgr3v  30345  nmoubi  30843  nmobndseqi  30850  nmobndseqiALT  30851  minvecolem1  30945  isch2  31294  hlimreui  31310  isch3  31312  ocsh  31354  dfch2  31478  spanuni  31615  nonbooli  31722  5oalem7  31731  adjsym  31904  elbdop2  31942  dmadjss  31958  nmopub  31979  nmfnleub  31996  nmop0h  32062  pjssposi  32243  pjordi  32244  cvbr2  32354  cvnbtwn2  32358  mdsl2i  32393  cvmdi  32395  elat2  32411  atom1d  32424  chirredi  32465  cdj3i  32512  or3di  32528  opreu2reu1  32553  mo5f  32558  reuxfrdf  32560  rexunirn  32561  difrab2  32567  rabsspr  32571  rabsstp  32572  tpssg  32607  iuninc  32630  disjorf  32649  disjunsn  32664  rabfmpunirn  32726  aciunf1  32736  funcnv5mpt  32740  eliccelico  32850  elicoelioo  32851  isslmd  33263  islinds5  33427  ismxidl  33522  1arithufdlem4  33607  hasheuni  34229  pwsiga  34274  sigainb  34280  issros  34319  2ndmbfm  34405  omssubaddlem  34443  omssubadd  34444  sitgaddlemb  34492  eulerpartlemgvv  34520  eulerpartlemn  34525  probun  34563  ballotlem2  34633  ballotlemodife  34642  bnj252  34846  bnj253  34847  bnj255  34848  bnj345  34857  bnj133  34870  bnj976  34920  bnj1098  34926  bnj121  35012  bnj130  35016  bnj150  35018  bnj581  35050  bnj607  35058  bnj865  35065  bnj917  35076  bnj934  35077  bnj964  35085  bnj983  35093  bnj996  35098  bnj1021  35108  bnj1033  35111  bnj1047  35115  bnj1049  35116  bnj1090  35121  bnj1128  35132  bnj1175  35146  bnj1189  35151  bnj1253  35159  bnj1312  35200  exdifsn  35221  fineqvrep  35258  fineqvac  35260  onvf1odlem4  35288  vonf1owev  35290  erdszelem9  35381  erdszelem10  35382  pconnconn  35413  cvmliftiota  35483  fmlaomn0  35572  fmla0disjsuc  35580  fmlasucdisj  35581  dmopab3rexdif  35587  elmthm  35758  antnestALT  35876  nepss  35900  xpab  35908  dfso2  35937  elrn3  35944  elpotr  35961  dfon2lem5  35967  dfon2lem7  35969  dfon2lem8  35970  elwlim  36003  wzel  36004  brtxp2  36061  brpprod3a  36066  eltrans  36071  dfon3  36072  dffix2  36085  dffun10  36094  elfuns  36095  brsingle  36097  brimg  36117  funpartfun  36125  funpartfv  36127  cgrxfr  36237  segletr  36296  outsideoftr  36311  neifg  36553  filnetlem4  36563  df3nandALT1  36581  weiunlem  36645  ttcwf3  36708  bj-consensusALT  36844  bj-df-ifc  36845  bj-exexalal  36871  bj-cbvaew  36938  bj-biexal3  37004  bj-alnnf  37034  bj-nfnnfTEMP  37079  bj-denoteslem  37178  bj-denotesALTV  37179  bj-ralvw  37186  bj-rexvw  37187  bj-rexcom4bv  37189  bj-rexcom4b  37190  bj-sbeq  37208  bj-inrab  37234  bj-rcleqf  37332  bj-dfmpoa  37430  bj-imdirco  37504  topdifinffinlem  37663  topdifinfeq  37666  relowlssretop  37679  relowlpssretop  37680  rdgeqoa  37686  domalom  37720  nlpineqsn  37724  fvineqsneq  37728  wl-ifpimpr  37782  wl-df3xor3  37786  wl-3xorbi  37789  wl-3xorbi2  37790  wl-2xor  37799  wl-2mintru2  37807  wl-dfclab  37910  rabiun  37914  phpreu  37925  fin2solem  37927  matunitlindflem2  37938  ptrest  37940  poimirlem25  37966  poimirlem27  37968  poimirlem30  37971  ismblfin  37982  ovoliunnfl  37983  voliunnfl  37985  volsupnfl  37986  itg2addnclem2  37993  fdc  38066  prdstotbnd  38115  isdrngo1  38277  ispridl  38355  ismaxidl  38361  impor  38402  selconj  38421  tradd  38426  scott0f  38490  r2alan  38572  inxpss3  38641  idinxpssinxp2  38645  idinxpssinxp3  38646  dfrel5  38667  ineleq  38675  ralmo  38681  ralrnmo  38682  ralrmo3  38685  moantr  38693  dfxrn2  38706  inxpxrn  38739  rnxrnres  38743  dfsuccl4  38795  coss1cnvres  38828  1cossres  38840  cocossss  38847  cossssid4  38881  cossssid5  38882  cosscnvssid5  38889  cossid  38891  dfssr2  38900  cnvrefrelcoss2  38938  cosselcnvrefrels2  38939  eqvrelcoss  39022  eqvrelcoss2  39024  dfcoeleqvrel  39027  refrelredund4  39040  cnvepresdmqs  39059  dfcomember  39078  dfdisjALTV  39119  disjimdmqseq  39130  dfeldisj3  39132  dfeldisj4  39133  dfeldisj5  39134  disjres  39165  prter1  39325  islshp  39425  islshpat  39463  lcvbr2  39468  lcvnbtwn2  39473  cvrnbtwn3  39722  isatl  39745  ishlat1  39798  ishlat2  39799  cvrat4  39889  pmapglbx  40215  lhpexle3  40458  dib1dim  41611  diblsmopel  41617  lcfls1lem  41980  prjsperref  43039  prjspeclsp  43045  euabsn2w  43112  rexrabdioph  43222  dford4  43457  onsupuni  43657  dflim6  43692  tfsconcatlem  43764  naddgeoa  43822  ifpdfor2  43888  ifpdfan2  43890  ifpdfor  43892  ifpdfan  43893  ifpnot23b  43909  ifpnot23c  43911  ifpnot23d  43912  ifpim123g  43927  ifpbibib  43937  clss2lem  44038  imaiun1  44078  coiun1  44079  brfvrcld2  44119  iunrelexp0  44129  brtrclfv2  44154  snhesn  44213  dffrege76  44366  frege97  44387  frege98  44388  frege109  44399  frege110  44400  dffrege115  44405  frege131  44421  frege133  44423  ntrneineine1lem  44511  ntrneiel2  44513  ntrneiiso  44518  gneispace3  44560  scotteld  44673  ismnuprim  44721  ismnushort  44728  dfuniv2  44729  pm11.52  44814  pm11.58  44817  pm13.192  44837  impexpdcom  44942  sbc3or  44959  opelopab4  44978  uunT12p1  45226  uunT12p2  45227  uunT12p3  45228  uun2221  45239  uun2221p1  45240  uun2221p2  45241  undif3VD  45308  modelaxreplem3  45407  permaxext  45432  permac8prim  45441  ndisj2  45482  nssrex  45516  rabssf  45549  bothtbothsame  47347  bothfbothsame  47348  aiffbtbat  47356  reuabaiotaiota  47535  2reu8i  47561  2reuimp0  47562  ichn  47916  dfodd2  48112  dfeven5  48142  dfodd7  48143  1nevenALTV  48167  oddprmne2  48191  dfvopnbgr2  48329  isuspgrim0lem  48369  gpg5nbgrvtx03starlem1  48544  gpg5nbgrvtx03starlem2  48545  gpg5nbgrvtx03starlem3  48546  gpg5nbgrvtx13starlem1  48547  gpg5nbgrvtx13starlem2  48548  gpg5nbgrvtx13starlem3  48549  gpg5edgnedg  48606  islindeps2  48959  isldepslvec2  48961  line2xlem  49229  rmotru  49278  reutru  49279  isnrm4  49406  iscnrm4  49429  homf0  49484  fuco2el  49787  isthincd2  49912  thinccic  49946  istermc2  49950  istermc3  49951  dftermc3  50006  setrec1lem3  50164  aacllem  50276