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  821  imor  854  imimorb  953  pm5.6  1004  nbi2  1018  casesifp  1078  3ancoma  1098  3ancomb  1099  3anrev  1101  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  2002  sbrimvw  2091  sbcom2  2173  sb5  2276  nf5  2282  nf6  2283  sbrim  2304  sbnf  2312  sb6x  2469  2sb5rf  2477  2sb6rf  2478  sb4b  2480  sb5f  2503  sbequ8  2506  sbhb  2526  eu6lem  2573  eu1  2610  iseqsetv-cleq  2806  issettru  2819  iseqsetv-clel  2820  issetlem  2821  cleqh  2871  cleqf  2934  sbabel  2938  necon3bii  2993  neor  3034  neorian  3037  rextru  3077  r19.26m  3110  r19.43  3122  r2allem  3142  r19.23t  3255  ralcom4  3286  rexcomOLD  3291  moel  3402  moelOLD  3405  rabid2f  3468  rabid2OLD  3471  eqv  3490  eqvf  3491  ralv  3508  rexv  3509  reuv  3510  rmov  3511  rexcom4b  3513  ceqsex4v  3538  ceqsex8v  3540  ceqsrexv  3655  rexab  3700  ralrab2  3704  rexrab2  3706  reu2  3731  reu3  3733  reueq  3743  2reuswap  3752  2reuswap2  3753  reuind  3759  2reu5lem3  3763  2rmoswap  3767  rmo2  3887  rmoanim  3894  rmoanimALT  3895  dfss3  3972  dfss3f  3975  ssabral  4065  rabss  4072  ssrabeq  4084  uniiunlem  4087  sspsstri  4105  npss  4113  dfdif3OLD  4118  raldifb  4149  uncom  4158  inass  4228  elsymdifxor  4260  nsspssun  4268  dfss4  4269  dfun2  4270  dfin2  4271  indi  4284  reupick3  4330  eq0f  4347  neq0f  4348  eq0  4350  eq0ALT  4351  dfnf5  4382  rabn0  4389  csbab  4440  vss  4446  disj  4450  disj3  4454  undisj1  4462  undisj2  4463  inundif  4479  undif  4482  undifr  4483  rabsssn  4668  exsnrex  4680  euabsn2  4725  euabsn  4726  raldifsni  4795  tppreqb  4805  pwpw0  4813  prssg  4819  ssunsn  4828  prneimg2  4855  preqsn  4862  pwpr  4901  dfuni2  4909  unissb  4939  unissbOLD  4940  elint2  4953  ssint  4964  uniintab  4986  dfiin2g  5032  iunid  5060  iunn0  5067  iunxun  5094  iunxiun  5097  iinpw  5106  disjor  5125  disjxiun  5140  dftr2  5261  dftr5OLD  5264  dftr3  5265  dftr4  5266  axrep6OLD  5289  vnex  5314  inuni  5350  eusv2  5396  reusv2lem4  5401  rexxfr  5416  sspwb  5454  opthneg  5486  pwssun  5575  dfid3  5581  dffr6  5640  dffr2  5646  dffr2ALT  5647  opthprc  5749  elxp3  5751  xpiundir  5757  elvv  5760  reliun  5826  inxpOLD  5843  raliunxp  5850  cnvuni  5897  dmopab2rex  5928  dm0rn0  5935  dfres3  6002  ssdmres  6031  elidinxp  6062  idinxpres  6065  dfima2  6080  args  6110  dffr3  6117  cotrg  6127  cotrgOLD  6128  cotrgOLDOLD  6129  intasym  6135  asymref  6136  intirr  6138  xpnz  6179  xp11  6195  ssrnres  6198  xpimasn  6205  coiun  6276  coass  6285  cnvso  6308  elsnxp  6311  dfpo2  6316  imaindm  6319  dffr4  6341  dfse3  6357  frpoind  6363  wfiOLD  6372  dflim2  6441  orddif  6480  dffun2OLDOLD  6573  dffun6  6574  dffun6f  6579  dffun7  6593  dffun9  6595  funfn  6596  svrelfun  6638  mptfnf  6703  dffn2  6738  dffn3  6748  fint  6787  dffn4  6826  dff1o4  6856  brprcneu  6896  brprcneuALT  6897  eqfnfv3  7053  fnreseql  7068  fsn  7155  ftpg  7176  abrexco  7264  imaiun  7265  dff13  7275  isof1oidb  7344  isof1oopb  7345  isocnv2  7351  eloprabga  7542  mpo2eqb  7565  elovmpo  7678  sorpss  7748  abexex  7996  elxp6  8048  elxp7  8049  releldm2  8068  opiota  8084  fnmpo  8094  frxp  8151  frxp2  8169  soseq  8184  cnvimadfsn  8197  mpoxneldm  8237  dftpos4  8270  frrlem9  8319  wfrlem8OLD  8356  wfrfunOLD  8359  dfrecs3  8412  dfrecs3OLD  8413  tfrlem7  8423  ondif1  8539  oarec  8600  oeeu  8641  brinxper  8774  0er  8783  eroveu  8852  erovlem  8853  elixpconst  8945  domen  9002  brsdom  9015  brdom2  9022  reuen1  9066  sbthlem10  9132  brsdom2  9137  xpf1o  9179  unfi  9211  sbthfilem  9238  onfin2  9268  0sdom1domALT  9275  modom  9280  marypha2lem3  9477  wemapsolem  9590  elom3  9688  dfom5  9690  brttrcl2  9754  ttrcltr  9756  ttrclse  9767  trcl  9768  epfrs  9771  frind  9790  rankf  9834  scottexs  9927  scott0s  9928  cplem1  9929  hta  9937  djuexb  9949  pm54.43lem  10040  alephsuc2  10120  iscard3  10133  aceq0  10158  aceq3lem  10160  dfac3  10161  dfac5lem2  10164  dfac5  10169  dfac7  10173  dfac12a  10189  kmlem12  10202  kmlem14  10204  kmlem15  10205  infmap2  10257  ackbij2  10282  dfacfin7  10439  ituniiun  10462  zorng  10544  brdom7disj  10571  entri2  10598  alephreg  10622  fpwwe2lem11  10681  fpwwe2lem12  10682  pwfseqlem1  10698  grutsk  10862  axgroth4  10872  grothprim  10874  grothtsk  10875  elni2  10917  ltsopi  10928  genpass  11049  psslinpr  11071  ltexprlem4  11079  ltresr  11180  1re  11261  infm3  12227  elnnz  12623  dfz2  12632  2rexuz  12942  nnwos  12957  eluz2b1  12961  qexALT  13006  elxr  13158  dflt2  13190  xrsupss  13351  xrinfmss  13352  elixx1  13396  elioo2  13428  dfrp2  13436  elioopnf  13483  elicopnf  13485  elfz1  13552  fznn  13632  fzp1nel  13651  fznn0  13659  preduz  13690  prinfzo0  13738  injresinj  13827  nn0opthlem1  14307  faclbnd4lem1  14332  hashfxnn0  14376  hashprdifel  14437  hashgt23el  14463  hashfun  14476  hashf1  14496  fz1isolem  14500  f1oun2prg  14956  brtrclfv  15041  shftdm  15110  rediv  15170  imdiv  15177  rexanre  15385  caubnd  15397  climreu  15592  prodmo  15972  dvdslelem  16346  3dvdsdec  16369  3dvds2dec  16370  bitsval  16461  smueqlem  16527  algcvgblem  16614  lcmfunsnlem2  16677  isprm2  16719  isprm3  16720  isprm4  16721  pythagtriplem2  16855  elgz  16969  hashbc0  17043  0ram  17058  isstruct  17189  issect  17797  isfull2  17958  isfth2  17962  fucinv  18021  eldmcoa  18110  isdrs  18347  submacs  18840  isnsg4  19185  isgim  19280  gaorb  19325  oppgid  19375  oppgsubm  19381  oppgcntz  19383  ispgp  19610  efgsdm  19748  efgcpbllema  19772  iscyg2  19900  isrng  20151  isring  20234  isirred2  20421  opprirred  20422  isrnghm  20441  dfrhm2  20474  isnzr2  20518  opprsubrng  20559  opprsubrg  20593  isdomn3  20715  drngid2  20752  issdrg  20789  islmod  20862  lss1d  20961  islmhm  21026  islmim  21061  lbsextlem2  21161  lidlnz  21252  dfprm2  21484  isphl  21646  elocv  21686  iunocv  21699  isobs  21740  islinds  21829  1mavmul  22554  toprntopon  22931  isbasis3g  22956  fctop  23011  cctop  23013  isclo2  23096  restsn  23178  lmbr  23266  ist0-3  23353  2ndcdisj  23464  1stccnp  23470  islocfin  23525  1stckgenlem  23561  txbas  23575  ptbasin  23585  tx2cn  23618  fbfinnfr  23849  fbasrn  23892  filuni  23893  ufinffr  23937  fin1aufil  23940  rnelfmlem  23960  flimrest  23991  alexsubALTlem3  24057  alexsubALTlem4  24058  tgphaus  24125  istlm  24193  iscusp2  24311  metuel2  24578  isngp2  24610  isnlm  24696  isphtpc  25026  phtpcer  25027  om1elbas  25065  isclm  25097  iscvsp  25161  iscph  25204  iscau3  25312  minveclem3b  25462  elovolm  25510  ioombl1lem4  25596  dyaddisj  25631  vitali  25648  itg1climres  25749  itg2seq  25777  itg2monolem1  25785  itg2mono  25788  limcrcl  25909  lhop1  26053  itgsubst  26090  mdegleb  26103  isuc1p  26180  ismon1p  26182  plydivex  26339  ellogdm  26681  1cubr  26885  atandm2  26920  birthdaylem3  26996  dmarea  27000  dchrelbas2  27281  dchrelbas4  27287  elno3  27700  nosgnn0  27703  nosepon  27710  nocvxminlem  27822  scutcut  27846  scutbday  27849  dmscut  27856  scutf  27857  sltrec  27865  made0  27912  addsprop  28009  negsproplem2  28061  negsprop  28067  mulsprop  28156  precsexlem10  28240  elzs2  28385  elnnzs  28387  recut  28428  0reno  28429  axcontlem7  28985  nb3grpr  29399  nb3grpr2  29400  upgrwlkcompim  29661  wlkson  29674  wlkonprop  29676  wksonproplem  29722  wksonproplemOLD  29723  ispth  29741  wwlknon  29877  wwlksnextinj  29919  wspthsnwspthsnon  29936  elwspths2spth  29987  rusgrnumwwlkl1  29988  clwwlkccatlem  30008  erclwwlkref  30039  frgr3v  30294  nmoubi  30791  nmobndseqi  30798  nmobndseqiALT  30799  minvecolem1  30893  isch2  31242  hlimreui  31258  isch3  31260  ocsh  31302  dfch2  31426  spanuni  31563  nonbooli  31670  5oalem7  31679  adjsym  31852  elbdop2  31890  dmadjss  31906  nmopub  31927  nmfnleub  31944  nmop0h  32010  pjssposi  32191  pjordi  32192  cvbr2  32302  cvnbtwn2  32306  mdsl2i  32341  cvmdi  32343  elat2  32359  atom1d  32372  chirredi  32413  cdj3i  32460  or3di  32478  opreu2reu1  32503  mo5f  32508  reuxfrdf  32510  rexunirn  32511  difrab2  32517  rabsspr  32520  rabsstp  32521  iuninc  32573  disjorf  32592  disjunsn  32607  rabfmpunirn  32663  aciunf1  32673  funcnv5mpt  32678  eliccelico  32779  elicoelioo  32780  isomnd  33078  omndmul2  33089  isslmd  33208  islinds5  33395  ismxidl  33490  1arithufdlem4  33575  hasheuni  34086  pwsiga  34131  sigainb  34137  issros  34176  2ndmbfm  34263  omssubaddlem  34301  omssubadd  34302  sitgaddlemb  34350  eulerpartlemgvv  34378  eulerpartlemn  34383  probun  34421  ballotlem2  34491  ballotlemodife  34500  bnj252  34717  bnj253  34718  bnj255  34719  bnj345  34728  bnj133  34741  bnj976  34791  bnj1098  34797  bnj121  34884  bnj130  34888  bnj150  34890  bnj581  34922  bnj607  34930  bnj865  34937  bnj917  34948  bnj934  34949  bnj964  34957  bnj983  34965  bnj996  34970  bnj1021  34980  bnj1033  34983  bnj1047  34987  bnj1049  34988  bnj1090  34993  bnj1128  35004  bnj1175  35018  bnj1189  35023  bnj1253  35031  bnj1312  35072  exdifsn  35093  fineqvrep  35109  fineqvac  35111  erdszelem9  35204  erdszelem10  35205  pconnconn  35236  cvmliftiota  35306  fmlaomn0  35395  fmla0disjsuc  35403  fmlasucdisj  35404  dmopab3rexdif  35410  elmthm  35581  nepss  35718  xpab  35726  dfso2  35755  elrn3  35762  elpotr  35782  dfon2lem5  35788  dfon2lem7  35790  dfon2lem8  35791  elwlim  35824  wzel  35825  brtxp2  35882  brpprod3a  35887  eltrans  35892  dfon3  35893  dffix2  35906  dffun10  35915  elfuns  35916  brsingle  35918  brimg  35938  funpartfun  35944  funpartfv  35946  cgrxfr  36056  segletr  36115  outsideoftr  36130  neifg  36372  filnetlem4  36382  df3nandALT1  36400  weiunlem2  36464  bj-consensusALT  36580  bj-df-ifc  36581  bj-biexal3  36708  bj-nfnnfTEMP  36759  bj-denoteslem  36872  bj-denotesALTV  36873  bj-ralvw  36880  bj-rexvw  36881  bj-rexcom4bv  36883  bj-rexcom4b  36884  bj-sbeq  36902  bj-inrab  36928  bj-rcleqf  37026  bj-dfmpoa  37119  bj-imdirco  37191  topdifinffinlem  37348  topdifinfeq  37351  relowlssretop  37364  relowlpssretop  37365  rdgeqoa  37371  domalom  37405  nlpineqsn  37409  fvineqsneq  37413  wl-ifpimpr  37467  wl-df3xor3  37471  wl-3xorbi  37474  wl-3xorbi2  37475  wl-2xor  37484  wl-2mintru2  37492  wl-dfclab  37597  rabiun  37600  phpreu  37611  fin2solem  37613  matunitlindflem2  37624  ptrest  37626  poimirlem25  37652  poimirlem27  37654  poimirlem30  37657  ismblfin  37668  ovoliunnfl  37669  voliunnfl  37671  volsupnfl  37672  itg2addnclem2  37679  fdc  37752  prdstotbnd  37801  isdrngo1  37963  ispridl  38041  ismaxidl  38047  impor  38088  selconj  38107  tradd  38112  scott0f  38176  r2alan  38250  inxpss3  38315  idinxpssinxp2  38319  idinxpssinxp3  38320  dfrel5  38347  ineleq  38355  moantr  38365  dfxrn2  38377  inxpxrn  38396  rnxrnres  38400  coss1cnvres  38418  1cossres  38430  cocossss  38437  cossssid4  38471  cossssid5  38472  cosscnvssid5  38479  cossid  38481  dfssr2  38500  cnvrefrelcoss2  38538  cosselcnvrefrels2  38539  eqvrelcoss  38618  eqvrelcoss2  38620  dfcoeleqvrel  38623  refrelredund4  38636  cnvepresdmqs  38654  dfcomember  38673  dfdisjALTV  38714  dfeldisj3  38720  dfeldisj4  38721  dfeldisj5  38722  disjres  38745  prter1  38880  islshp  38980  islshpat  39018  lcvbr2  39023  lcvnbtwn2  39028  cvrnbtwn3  39277  isatl  39300  ishlat1  39353  ishlat2  39354  cvrat4  39445  pmapglbx  39771  lhpexle3  40014  dib1dim  41167  diblsmopel  41173  lcfls1lem  41536  prjsperref  42616  prjspeclsp  42622  euabsn2w  42689  rexrabdioph  42805  dford4  43041  onsupuni  43241  dflim6  43277  tfsconcatlem  43349  naddgeoa  43407  ifpdfor2  43474  ifpdfan2  43476  ifpdfor  43478  ifpdfan  43479  ifpnot23b  43495  ifpnot23c  43497  ifpnot23d  43498  ifpim123g  43513  ifpbibib  43523  clss2lem  43624  imaiun1  43664  coiun1  43665  brfvrcld2  43705  iunrelexp0  43715  brtrclfv2  43740  snhesn  43799  dffrege76  43952  frege97  43973  frege98  43974  frege109  43985  frege110  43986  dffrege115  43991  frege131  44007  frege133  44009  ntrneineine1lem  44097  ntrneiel2  44099  ntrneiiso  44104  gneispace3  44146  scotteld  44265  ismnuprim  44313  ismnushort  44320  dfuniv2  44321  pm11.52  44406  pm11.58  44409  pm13.192  44429  impexpdcom  44535  sbc3or  44552  opelopab4  44571  uunT12p1  44820  uunT12p2  44821  uunT12p3  44822  uun2221  44833  uun2221p1  44834  uun2221p2  44835  undif3VD  44902  modelaxreplem3  44997  ndisj2  45056  nssrex  45091  rabssf  45124  bothtbothsame  46911  bothfbothsame  46912  aiffbtbat  46920  reuabaiotaiota  47099  2reu8i  47125  2reuimp0  47126  ichn  47443  dfodd2  47623  dfeven5  47653  dfodd7  47654  1nevenALTV  47678  oddprmne2  47702  dfvopnbgr2  47839  isuspgrim0lem  47871  gpg5nbgrvtx03starlem1  48024  gpg5nbgrvtx03starlem2  48025  gpg5nbgrvtx03starlem3  48026  gpg5nbgrvtx13starlem1  48027  gpg5nbgrvtx13starlem2  48028  gpg5nbgrvtx13starlem3  48029  islindeps2  48400  isldepslvec2  48402  line2xlem  48674  rmotru  48723  reutru  48724  isnrm4  48828  iscnrm4  48851  fuco2el  49007  isthincd2  49086  thinccic  49118  istermc2  49122  istermc3  49123  setrec1lem3  49208  aacllem  49320