Theorem bitr4i 281

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 227	. 2 ⊢ (𝜓 ↔ 𝜒)
4	1, 3	bitri 278	1 ⊢ (𝜑 ↔ 𝜒)

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3bitr2i  302  3bitr2ri  303  3bitr4i  306  3bitr4ri  307  biluk  390  biancomi  468  dfbi2  480  imdistan  578  pm5.32  584  bianass  655  mpbiran  722  biadaniALT  833  imor  867  imimorb  965  pm5.6  1017  nbi2  1033  ifpdfbi  1086  casesifp  1094  3ancoma  1115  3ancomb  1116  3anrev  1118  4anpull2  1382  dfnan2  1524  nannan  1527  nanbi  1530  xorcom  1544  xorneg  1553  xorbi12i  1554  norcom  1560  noran  1562  norasslem1  1564  trunortru  1619  trunorfal  1620  cadan  1642  cadcomb  1646  nic-ax  1706  nic-axALT  1707  nf3  1819  19.43  1915  equsv  2036  sbrimvwOLD  2129  sbcom2  2209  sb5  2309  nf5  2315  nf6  2316  sbrim  2337  sbnf  2344  sb6x  2493  2sb5rf  2501  2sb6rf  2502  sb4b  2504  sb5f  2527  sbequ8  2530  sbhb  2550  eu6lem  2598  eu1  2635  iseqsetv-cleq  2824  issettru  2838  iseqsetv-clel  2839  issetlem  2840  cleqh  2889  cleqf  2950  sbabel  2954  necon3bii  3007  neor  3047  neorian  3050  rextru  3093  r19.26m  3121  r19.43  3130  3r19.43  3131  r2allem  3150  r19.23t  3258  ralcom4  3288  moel  3385  rabid2f  3442  eqv  3460  eqvf  3461  ralv  3476  rexv  3477  reuv  3478  rmov  3479  rexcom4b  3481  ceqsex4v  3503  ceqsex8v  3505  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  3834  rmoanim  3842  rmoanimALT  3843  dfss3  3920  dfss3f  3923  nssrex  3996  ssabral  4012  rabss  4018  ssrabeq  4032  uniiunlem  4035  sspsstri  4054  npss  4062  raldifb  4096  uncom  4105  inass  4173  elsymdifxor  4206  nsspssun  4214  dfss4  4215  dfun2  4216  dfin2  4217  indi  4230  reupick3  4276  eq0f  4294  neq0f  4295  eq0ALT  4298  inssdif0  4322  dfnf5  4331  rabn0  4339  vss  4358  csbab  4398  disj  4403  disj3  4407  undisj1  4415  undisj2  4416  inundif  4435  undif  4438  undifr  4439  rabsssn  4629  exsnrex  4641  euabsn2  4686  euabsn  4687  raldifsni  4758  tppreqb  4768  pwpw0  4774  prssg  4780  ssunsn  4789  prneimg2  4815  preqsn  4822  pwpr  4861  dfuni2  4869  unissb  4901  elint2  4914  ssint  4924  uniintab  4946  dfiin2g  4989  iunid  5019  iunn0  5025  iunxun  5054  iunxiun  5057  iinpw  5066  disjor  5085  disjxiun  5100  dftr2  5214  dftr3  5217  dftr4  5218  axrep6OLD  5242  vnexOLD  5275  inuni  5314  eusv2  5361  reusv2lem4  5366  rexxfr  5381  sspwb  5424  opthneg  5457  pwssun  5547  dfid3  5553  dffr6  5611  dffr2  5616  dffr2ALT  5617  opthprc  5719  elxp3  5721  xpiundir  5727  elvv  5730  raliunxp  5819  cnvuni  5870  dmopab2rex  5901  dm0rn0OLD  5909  dfres3  5977  ssdmres  6006  elidinxp  6040  idinxpres  6043  dfima2  6058  args  6088  dffr3  6095  cotrg  6105  intasym  6109  asymref  6110  intirr  6112  xpnz  6151  xp11  6168  ssrnres  6171  xpimasn  6178  coiun  6253  coass  6262  cnvso  6286  elsnxp  6289  dfpo2  6294  imaindm  6297  dffr4  6318  dfse3  6334  frpoind  6340  dflim2  6416  orddif  6456  dffun6  6544  dffun6f  6548  dffun7  6560  dffun9  6562  funfn  6563  svrelfun  6605  mptfnf  6667  dffn2  6704  dffn3  6715  fint  6754  dffn4  6795  dff1o4  6826  brprcneu  6868  brprcneuALT  6869  eqfnfv3  7024  fnreseql  7040  fsn  7129  ftpg  7153  abrexco  7241  imaiun  7242  dff13  7251  isof1oidb  7325  isof1oopb  7326  isocnv2  7332  eloprabga  7522  mpo2eqb  7545  elovmpo  7659  sorpss  7729  abexex  7968  elxp6  8020  elxp7  8021  releldm2  8040  opiota  8056  fnmpo  8066  frxp  8124  frxp2  8142  soseq  8157  cnvimadfsn  8170  mpoxneldm  8210  dftpos4  8243  frrlem9  8293  dfrecs3  8361  tfrlem7  8372  ondif1  8488  oarec  8549  oeeu  8591  brinxper  8726  0er  8735  eroveu  8812  erovlem  8813  elixpconst  8912  domen  8967  brsdom  8980  brdom2  8988  reuen1  9032  sbthlem10  9094  brsdom2  9099  xpf1o  9137  unfi  9165  sbthfilem  9192  onfin2  9211  0sdom1domALT  9217  modom  9221  marypha2lem3  9407  wemapsolem  9522  elom3  9627  dfom5  9629  brttrcl2  9693  ttrcltr  9695  ttrclse  9706  trcl  9707  epfrs  9710  frind  9732  rankf  9776  scottexsOLD  9882  scott0bsOLD  9884  cplem1OLD  9890  hta  9901  htaOLD  9902  djuexb  9914  pm54.43lem  10005  alephsuc2  10083  iscard3  10096  aceq0  10121  aceq3lem  10123  dfac3  10124  dfac5lem2  10127  dfac5  10131  dfac7  10135  dfac12a  10151  kmlem12  10164  kmlem14  10166  kmlem15  10167  infmap2  10219  ackbij2  10244  dfacfin7  10401  ituniiun  10424  zorng  10506  brdom7disj  10534  entri2  10566  alephreg  10591  fpwwe2lem11  10650  fpwwe2lem12  10651  pwfseqlem1  10667  grutsk  10831  axgroth4  10841  grothprim  10843  grothtsk  10844  elni2  10886  ltsopi  10897  genpass  11018  psslinpr  11040  ltexprlem4  11048  ltresr  11149  infm3  12198  elnnz  12625  dfz2  12634  2rexuz  12949  nnwos  12964  eluz2b1  12968  qexALT  13013  elxr  13167  dflt2  13199  xrsupss  13361  xrinfmss  13362  elixx1  13407  elioo2  13439  dfrp2  13447  elioopnf  13496  elicopnf  13498  elfz1  13566  fznn  13647  fzp1nel  13666  fznn0  13674  preduz  13705  prinfzo0  13754  injresinj  13847  nn0opthlem1  14332  faclbnd4lem1  14357  hashfxnn0  14401  hashprdifel  14462  hashgt23el  14489  hashfun  14502  hashf1  14522  fz1isolem  14526  f1oun2prg  14988  brtrclfv  15075  shftdm  15144  rediv  15218  imdiv  15225  rexanre  15434  caubnd  15446  climreu  15643  prodmo  16023  dvdslelem  16399  3dvdsdec  16422  3dvds2dec  16423  bitsval  16514  smueqlem  16580  algcvgblem  16667  lcmfunsnlem2  16730  isprm2  16772  isprm3  16773  isprm4  16774  pythagtriplem2  16909  elgz  17023  hashbc0  17097  0ram  17112  isstruct  17244  issect  17842  isfull2  18002  isfth2  18006  fucinv  18065  eldmcoa  18154  isdrs  18389  submacs  18936  isnsg4  19290  isgim  19389  gaorb  19434  oppgid  19483  oppgsubm  19489  oppgcntz  19491  ispgp  19719  efgsdm  19857  efgcpbllema  19881  iscyg2  20009  isomnd  20250  omndmul2  20260  isrng  20289  isring  20376  isirred2  20562  opprirred  20563  isrnghm  20582  dfrhm2  20615  rimval  20641  isnzr2  20678  opprsubrng  20721  opprsubrg  20755  isdomn3  20876  drngid2  20919  issdrg  20954  islmod  21048  lss1d  21147  islmhm  21211  islmim  21246  lbsextlem2  21346  lidlnz  21439  dfprm2  21686  isphl  21841  elocv  21881  iunocv  21894  isobs  21933  islinds  22022  1mavmul  22770  matunitlindflem2  22902  toprntopon  23150  isbasis3g  23174  fctop  23229  cctop  23231  isclo2  23313  restsn  23395  lmbr  23483  ist0-3  23570  2ndcdisj  23682  1stccnp  23688  islocfin  23743  1stckgenlem  23779  txbas  23793  ptbasin  23803  tx2cn  23836  fbfinnfr  24067  fbasrn  24110  filuni  24111  ufinffr  24155  fin1aufil  24158  rnelfmlem  24178  flimrest  24209  alexsubALTlem3  24275  alexsubALTlem4  24276  tgphaus  24343  istlm  24411  iscusp2  24527  metuel2  24791  isngp2  24823  isnlm  24901  isphtpc  25222  phtpcer  25223  om1elbas  25260  isclm  25292  iscvsp  25356  iscph  25398  iscau3  25506  minveclem3b  25656  elovolm  25703  ioombl1lem4  25789  dyaddisj  25824  vitali  25841  itg1climres  25942  itg2seq  25970  itg2monolem1  25978  itg2mono  25981  limcrcl  26101  lhop1  26241  itgsubst  26276  mdegleb  26289  isuc1p  26366  ismon1p  26368  plydivex  26527  ellogdm  26876  1cubr  27079  atandm2  27114  birthdaylem3  27190  dmarea  27194  dchrelbas2  27473  dchrelbas4  27479  elno3  27891  nosgnn0  27894  nosepon  27901  nocvxminlem  28019  cutcuts  28046  cutbday  28049  dmcuts  28056  cutsf  28057  ltsrec  28066  made0  28128  addsprop  28241  negsproplem2  28294  negsprop  28300  mulsprop  28395  precsexlem10  28481  elzs2  28664  elnnzs  28666  bdayfinbndlem1  28732  recut  28759  axcontlem7  29427  nb3grpr  29842  nb3grpr2  29843  upgrwlkcompim  30102  wlkson  30114  wlkonprop  30116  wksonproplem  30166  ispth  30185  wwlknon  30325  wwlksnextinj  30367  wspthsnwspthsnon  30384  elwspths2spth  30438  rusgrnumwwlkl1  30439  clwwlkccatlem  30459  erclwwlkref  30490  frgr3v  30755  nmoubi  31253  nmobndseqi  31260  nmobndseqiALT  31261  minvecolem1  31355  isch2  31704  hlimreui  31720  isch3  31722  ocsh  31764  dfch2  31888  spanuni  32025  nonbooli  32132  5oalem7  32141  adjsym  32314  elbdop2  32352  dmadjss  32368  nmopub  32389  nmfnleub  32406  nmop0h  32472  pjssposi  32653  pjordi  32654  cvbr2  32764  cvnbtwn2  32768  mdsl2i  32803  cvmdi  32805  elat2  32821  atom1d  32834  chirredi  32875  cdj3i  32922  or3di  32936  opreu2reu1  32959  mo5f  32964  reuxfrdf  32966  rexunirn  32967  difrab2  32973  rabsspr  32976  rabsstp  32977  tpssg  33012  iuninc  33034  disjorf  33052  disjunsn  33067  rabfmpunirn  33126  aciunf1  33136  funcnv5mpt  33140  eliccelico  33248  elicoelioo  33249  isslmd  33642  islinds5  33802  ismxidl  33865  1arithufdlem4  33957  hasheuni  34595  pwsiga  34640  sigainb  34647  issros  34686  2ndmbfm  34772  omssubaddlem  34810  omssubadd  34811  sitgaddlemb  34859  eulerpartlemgvv  34887  eulerpartlemn  34892  probun  34930  ballotlem2  35000  ballotlemodife  35009  bnj252  35213  bnj253  35214  bnj255  35215  bnj345  35224  bnj133  35237  bnj976  35287  bnj1098  35293  bnj121  35379  bnj130  35383  bnj150  35385  bnj581  35417  bnj607  35425  bnj865  35432  bnj917  35443  bnj934  35444  bnj964  35452  bnj983  35460  bnj996  35465  bnj1021  35475  bnj1033  35478  bnj1047  35482  bnj1049  35483  bnj1090  35488  bnj1128  35499  bnj1175  35513  bnj1189  35518  bnj1253  35526  bnj1312  35567  exdifsn  35589  scott0bOLD  35634  fineqvrep  35640  fineqvac  35642  kard0  35680  kardexen  35689  onvf1odlem4  35703  vonf1wev  35705  vonf1owevOLD  35707  vonf1osev  35709  erdszelem9  35778  erdszelem10  35779  pconnconn  35810  cvmliftiota  35880  fmlaomn0  35969  fmla0disjsuc  35977  fmlasucdisj  35978  dmopab3rexdif  35984  elmthm  36155  antnestALT  36273  nepss  36297  xpab  36305  dfso2  36334  elrn3  36341  elpotr  36358  dfon2lem5  36364  dfon2lem7  36366  dfon2lem8  36367  elwlim  36400  wzel  36401  brtxp2  36458  brpprod3a  36463  eltrans  36468  dfon3  36469  dffix2  36482  dffun10  36491  elfuns  36492  brsingle  36494  brimg  36514  funpartfun  36522  funpartfv  36524  cgrxfr  36635  segletr  36694  outsideoftr  36709  naddle  36799  neifg  36990  filnetlem4  37000  df3nandALT1  37018  weiunlem  37082  ttcwf3  37145  bj-consensusALT  37280  bj-df-ifc  37281  bj-exexalal  37307  bj-cbvaew  37374  bj-biexal3  37440  bj-alnnf  37470  bj-nfnnfTEMP  37515  bj-denoteslem  37614  bj-denotesALTV  37615  bj-ralvw  37622  bj-rexvw  37623  bj-rexcom4bv  37625  bj-rexcom4b  37626  bj-sbeq  37644  bj-inrab  37671  bj-rcleqf  37769  bj-dfmpoa  37868  bj-imdirco  37942  topdifinffinlem  38101  topdifinfeq  38104  relowlssretop  38117  relowlpssretop  38118  rdgeqoa  38124  domalom  38158  nlpineqsn  38162  fvineqsneq  38166  wl-ifpimpr  38220  wl-df3xor3  38224  wl-3xorbi  38227  wl-3xorbi2  38228  wl-2xor  38237  wl-2mintru2  38245  wl-dfclab  38348  rabiun  38352  phpreu  38358  fin2solem  38360  ptrest  38368  poimirlem25  38394  poimirlem27  38396  poimirlem30  38399  ismblfin  38410  ovoliunnfl  38411  voliunnfl  38413  volsupnfl  38414  itg2addnclem2  38421  fdc  38495  prdstotbnd  38544  isdrngo1  38706  ispridl  38784  ismaxidl  38790  impor  38831  selconj  38848  tradd  38853  r2alan  38999  inxpss3  39068  idinxpssinxp2  39072  idinxpssinxp3  39073  dfrel5  39094  ineleq  39102  ralmo  39108  ralrnmo  39109  ralrmo3  39112  moantr  39120  dfxrn2  39133  inxpxrn  39166  rnxrnres  39170  dfsuccl4  39222  coss1cnvres  39255  1cossres  39267  cocossss  39274  cossssid4  39308  cossssid5  39309  cosscnvssid5  39316  cossid  39318  dfssr2  39327  cnvrefrelcoss2  39365  cosselcnvrefrels2  39366  eqvrelcoss  39449  eqvrelcoss2  39451  dfcoeleqvrel  39454  refrelredund4  39467  cnvepresdmqs  39486  dfcomember  39505  dfdisjALTV  39546  disjimdmqseq  39557  dfeldisj3  39559  dfeldisj4  39560  dfeldisj5  39561  disjres  39592  prter1  39752  islshp  39852  islshpat  39890  lcvbr2  39895  lcvnbtwn2  39900  cvrnbtwn3  40149  isatl  40172  ishlat1  40225  ishlat2  40226  cvrat4  40316  pmapglbx  40642  lhpexle3  40885  dib1dim  42038  diblsmopel  42044  lcfls1lem  42407  prjsperref  43452  prjspeclsp  43458  euabsn2w  43525  rexrabdioph  43635  dford4  43870  onsupuni  44070  dflim6  44105  tfsconcatlem  44177  naddgeoa  44235  ifpdfor2  44301  ifpdfan2  44303  ifpdfor  44305  ifpdfan  44306  ifpnot23b  44322  ifpnot23c  44324  ifpnot23d  44325  ifpim123g  44340  ifpbibib  44350  clss2lem  44451  imaiun1  44491  coiun1  44492  brfvrcld2  44532  iunrelexp0  44542  brtrclfv2  44567  snhesn  44626  dffrege76  44779  frege97  44800  frege98  44801  frege109  44812  frege110  44813  dffrege115  44818  frege131  44834  frege133  44836  ntrneineine1lem  44924  ntrneiel2  44926  ntrneiiso  44931  gneispace3  44973  ismnuprim  45118  ismnushort  45125  dfuniv2  45126  pm11.52  45211  pm11.58  45214  pm13.192  45234  impexpdcom  45338  sbc3or  45355  opelopab4  45374  uunT12p1  45622  uunT12p2  45623  uunT12p3  45624  uun2221  45635  uun2221p1  45636  uun2221p2  45637  undif3VD  45704  modelaxreplem3  45803  permaxext  45828  permac8prim  45837  ndisj2  45885  rabssf  45951  wrddin2  47716  chndin2  47721  chnrin2  47726  bothtbothsame  47787  bothfbothsame  47788  aiffbtbat  47796  reuabaiotaiota  47975  2reu8i  48001  2reuimp0  48002  ichn  48356  dfodd2  48552  dfeven5  48582  dfodd7  48583  1nevenALTV  48607  oddprmne2  48631  dfvopnbgr2  48769  isuspgrim0lem  48809  gpg5nbgrvtx03starlem1  48984  gpg5nbgrvtx03starlem2  48985  gpg5nbgrvtx03starlem3  48986  gpg5nbgrvtx13starlem1  48987  gpg5nbgrvtx13starlem2  48988  gpg5nbgrvtx13starlem3  48989  gpg5edgnedg  49046  dfidom2  49258  islindeps2  49413  isldepslvec2  49415  line2xlem  49683  rmotru  49731  reutru  49732  isnrm4  49857  iscnrm4  49880  homf0  49935  fuco2el  50238  isthincd2  50363  thinccic  50397  istermc2  50401  istermc3  50402  dftermc3  50457  setrec1lem3  50615  dfrals2  50719  dfralseu2  50752  aacllem  50772