Theorem bitr4i 277

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

Syntax hints:   ↔ wb 205

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 206

This theorem is referenced by:  3bitr2i  298  3bitr2ri  299  3bitr4i  302  3bitr4ri  303  biluk  384  biancomi  461  dfbi2  473  imdistan  566  pm5.32  572  bianass  640  mpbiran  707  biadaniALT  819  imor  851  imimorb  948  pm5.6  999  nbi2  1013  casesifp  1075  3ancoma  1095  3ancomb  1096  3anrev  1098  dfnan2  1488  nannan  1491  nanbi  1494  xorcom  1508  xorneg  1517  xorbi12i  1518  norcom  1524  noran  1526  norasslem1  1528  trunortru  1583  trunorfal  1584  cadan  1603  cadcomb  1607  nic-ax  1668  nic-axALT  1669  nf3  1781  nfnbiOLD  1851  19.43  1878  equsv  1999  sbrimvw  2087  sbcom2  2163  sb5  2263  nf5  2272  nf6  2273  sbrim  2294  sbnf  2302  sb6x  2458  2sb5rf  2466  2sb6rf  2467  sb4b  2469  sb5f  2492  sbequ8  2495  sbhb  2515  eu6lem  2562  eu1  2599  issetlem  2806  cleqh  2856  clelabOLD  2873  cleqf  2924  sbabel  2928  necon3bii  2983  neor  3024  neorian  3027  rextru  3067  r19.26m  3100  r19.43  3112  r2allem  3132  r19.23t  3243  ralcom4  3274  rexcomOLD  3279  moel  3386  moelOLD  3389  rabid2f  3451  rabid2OLD  3454  eqv  3472  eqvf  3473  ralv  3489  rexv  3490  reuv  3491  rmov  3492  rexcom4b  3494  ceqsex4v  3524  ceqsex8v  3526  ceqsrexv  3640  rexab  3688  ralrab2  3692  rexrab2  3694  reu2  3719  reu3  3721  reueq  3731  2reuswap  3740  2reuswap2  3741  reuind  3747  2reu5lem3  3751  2rmoswap  3755  rmo2  3880  rmoanim  3887  rmoanimALT  3888  dfss3  3968  dfss3f  3971  ssabral  4059  rabss  4068  ssrabeq  4081  uniiunlem  4083  sspsstri  4101  npss  4109  dfdif3  4113  raldifb  4144  uncom  4153  inass  4221  elsymdifxor  4251  nsspssun  4259  dfss4  4260  dfun2  4261  dfin2  4262  indi  4275  indifdirOLD  4287  reupick3  4322  eq0f  4343  neq0f  4344  eq0  4346  eq0ALT  4347  dfnf5  4382  rabn0  4390  csbab  4442  vss  4448  disj  4452  disjOLD  4453  disj3  4458  undisj1  4466  undisj2  4467  inundif  4483  undif  4486  undifr  4487  rabsssn  4675  exsnrex  4689  euabsn2  4734  euabsn  4735  raldifsni  4804  tppreqb  4814  pwpw0  4822  prssg  4828  ssunsn  4837  preqsn  4868  pwpr  4907  dfuni2  4915  unissb  4947  unissbOLD  4948  elint2  4961  ssint  4972  uniintab  4996  dfiin2g  5040  iunid  5068  iunn0  5075  iunxun  5102  iunxiun  5105  iinpw  5114  disjor  5133  disjxiun  5150  dftr2  5272  dftr5OLD  5275  dftr3  5276  dftr4  5277  axrep6  5297  vnex  5319  inuni  5350  eusv2  5400  reusv2lem4  5405  rexxfr  5420  sspwb  5455  opthneg  5487  pwssun  5577  dfid3  5583  dffr6  5640  dffr2  5646  dffr2ALT  5647  opthprc  5746  elxp3  5748  xpiundir  5753  elvv  5756  reliun  5822  inxpOLD  5839  raliunxp  5846  cnvuni  5893  dmopab2rex  5924  dm0rn0  5931  dfres3  5994  ssdmres  6022  elidinxp  6053  idinxpres  6056  dfima2  6071  args  6102  dffr3  6109  cotrg  6119  cotrgOLD  6120  cotrgOLDOLD  6121  intasym  6127  asymref  6128  intirr  6130  xpnz  6170  xp11  6186  ssrnres  6189  xpimasn  6196  coiun  6267  coass  6276  cnvso  6299  elsnxp  6302  dfpo2  6307  imaindm  6310  dffr4  6332  dfse3  6349  frpoind  6355  wfiOLD  6364  dflim2  6433  orddif  6472  dffun2OLDOLD  6566  dffun6  6567  dffun6f  6572  dffun7  6586  dffun9  6588  funfn  6589  svrelfun  6631  mptfnf  6696  dffn2  6730  dffn3  6740  fint  6781  dffn4  6821  dff1o4  6851  brprcneu  6891  brprcneuALT  6892  eqfnfv3  7046  fnreseql  7061  fsn  7149  ftpg  7170  abrexco  7259  imaiun  7260  dff13  7270  isof1oidb  7336  isof1oopb  7337  isocnv2  7343  eloprabga  7533  mpo2eqb  7558  elovmpo  7671  sorpss  7739  abexex  7985  elxp6  8037  elxp7  8038  releldm2  8057  opiota  8073  fnmpo  8083  frxp  8140  frxp2  8158  soseq  8173  cnvimadfsn  8186  mpoxneldm  8227  dftpos4  8260  frrlem9  8309  wfrlem8OLD  8346  wfrfunOLD  8349  dfrecs3  8402  dfrecs3OLD  8403  tfrlem7  8413  ondif1  8531  oarec  8592  oeeu  8633  brinxper  8763  0er  8772  eroveu  8841  erovlem  8842  elixpconst  8934  domen  8992  brsdom  9006  brdom2  9013  reuen1  9061  sbthlem10  9130  brsdom2  9135  xpf1o  9177  unfi  9210  sbthfilem  9235  onfin2  9265  0sdom1domALT  9273  modom  9278  unfiOLD  9347  marypha2lem3  9480  wemapsolem  9593  elom3  9691  dfom5  9693  brttrcl2  9757  ttrcltr  9759  ttrclse  9770  trcl  9771  epfrs  9774  frind  9793  rankf  9837  scottexs  9930  scott0s  9931  cplem1  9932  hta  9940  djuexb  9952  pm54.43lem  10043  alephsuc2  10123  iscard3  10136  aceq0  10161  aceq3lem  10163  dfac3  10164  dfac5lem2  10167  dfac5  10171  dfac7  10175  dfac12a  10191  kmlem12  10204  kmlem14  10206  kmlem15  10207  infmap2  10261  ackbij2  10286  dfacfin7  10442  ituniiun  10465  zorng  10547  brdom7disj  10574  entri2  10601  alephreg  10625  fpwwe2lem11  10684  fpwwe2lem12  10685  pwfseqlem1  10701  grutsk  10865  axgroth4  10875  grothprim  10877  grothtsk  10878  elni2  10920  ltsopi  10931  genpass  11052  psslinpr  11074  ltexprlem4  11082  ltresr  11183  1re  11264  infm3  12225  elnnz  12620  dfz2  12629  2rexuz  12936  nnwos  12951  eluz2b1  12955  qexALT  13000  elxr  13150  dflt2  13181  xrsupss  13342  xrinfmss  13343  elixx1  13387  elioo2  13419  dfrp2  13427  elioopnf  13474  elicopnf  13476  elfz1  13543  fznn  13623  fzp1nel  13639  fznn0  13647  preduz  13677  prinfzo0  13725  injresinj  13808  nn0opthlem1  14285  faclbnd4lem1  14310  hashfxnn0  14354  hashprdifel  14415  hashgt23el  14441  hashfun  14454  hashf1  14476  fz1isolem  14480  f1oun2prg  14926  brtrclfv  15007  shftdm  15076  rediv  15136  imdiv  15143  rexanre  15351  caubnd  15363  climreu  15558  prodmo  15938  dvdslelem  16311  3dvdsdec  16334  3dvds2dec  16335  bitsval  16424  smueqlem  16490  algcvgblem  16578  lcmfunsnlem2  16641  isprm2  16683  isprm3  16684  isprm4  16685  pythagtriplem2  16819  elgz  16933  hashbc0  17007  0ram  17022  isstruct  17154  issect  17769  isfull2  17933  isfth2  17937  fucinv  17998  eldmcoa  18087  isdrs  18326  submacs  18817  isnsg4  19161  isgim  19256  gaorb  19301  oppgid  19353  oppgsubm  19359  oppgcntz  19361  ispgp  19590  efgsdm  19728  efgcpbllema  19752  iscyg2  19880  isrng  20137  isring  20220  isirred2  20403  opprirred  20404  isrnghm  20423  dfrhm2  20456  isnzr2  20500  opprsubrng  20541  opprsubrg  20577  isdomn3  20693  drngid2  20730  issdrg  20767  islmod  20840  lss1d  20940  islmhm  21005  islmim  21040  lbsextlem2  21140  lidlnz  21231  dfprm2  21463  isphl  21624  elocv  21664  iunocv  21677  isobs  21718  islinds  21807  1mavmul  22541  toprntopon  22918  isbasis3g  22943  fctop  22998  cctop  23000  isclo2  23083  restsn  23165  lmbr  23253  ist0-3  23340  2ndcdisj  23451  1stccnp  23457  islocfin  23512  1stckgenlem  23548  txbas  23562  ptbasin  23572  tx2cn  23605  fbfinnfr  23836  fbasrn  23879  filuni  23880  ufinffr  23924  fin1aufil  23927  rnelfmlem  23947  flimrest  23978  alexsubALTlem3  24044  alexsubALTlem4  24045  tgphaus  24112  istlm  24180  iscusp2  24298  metuel2  24565  isngp2  24597  isnlm  24683  isphtpc  25011  phtpcer  25012  om1elbas  25050  isclm  25082  iscvsp  25146  iscph  25189  iscau3  25297  minveclem3b  25447  elovolm  25495  ioombl1lem4  25581  dyaddisj  25616  vitali  25633  itg1climres  25735  itg2seq  25763  itg2monolem1  25771  itg2mono  25774  limcrcl  25894  lhop1  26038  itgsubst  26075  mdegleb  26091  isuc1p  26168  ismon1p  26170  plydivex  26325  ellogdm  26666  1cubr  26870  atandm2  26905  birthdaylem3  26981  dmarea  26985  dchrelbas2  27266  dchrelbas4  27272  elno3  27685  nosgnn0  27688  nosepon  27695  nocvxminlem  27807  scutcut  27831  scutbday  27834  dmscut  27841  scutf  27842  sltrec  27850  made0  27897  addsprop  27990  negsproplem2  28038  negsprop  28044  mulsprop  28131  precsexlem10  28215  recut  28347  0reno  28348  axcontlem7  28904  nb3grpr  29318  nb3grpr2  29319  upgrwlkcompim  29580  wlkson  29593  wlkonprop  29595  wksonproplem  29641  wksonproplemOLD  29642  ispth  29660  wwlknon  29791  wwlksnextinj  29833  wspthsnwspthsnon  29850  elwspths2spth  29901  rusgrnumwwlkl1  29902  clwwlkccatlem  29922  erclwwlkref  29953  frgr3v  30208  nmoubi  30705  nmobndseqi  30712  nmobndseqiALT  30713  minvecolem1  30807  isch2  31156  hlimreui  31172  isch3  31174  ocsh  31216  dfch2  31340  spanuni  31477  nonbooli  31584  5oalem7  31593  adjsym  31766  elbdop2  31804  dmadjss  31820  nmopub  31841  nmfnleub  31858  nmop0h  31924  pjssposi  32105  pjordi  32106  cvbr2  32216  cvnbtwn2  32220  mdsl2i  32255  cvmdi  32257  elat2  32273  atom1d  32286  chirredi  32327  cdj3i  32374  or3di  32389  opreu2reu1  32412  mo5f  32417  reuxfrdf  32419  rexunirn  32420  difrab2  32426  iuninc  32481  disjorf  32499  disjunsn  32514  rabfmpunirn  32570  aciunf1  32580  funcnv5mpt  32585  eliccelico  32679  elicoelioo  32680  isomnd  32936  omndmul2  32947  isslmd  33066  islinds5  33242  ismxidl  33337  1arithufdlem4  33422  hasheuni  33918  pwsiga  33963  sigainb  33969  issros  34008  2ndmbfm  34095  omssubaddlem  34133  omssubadd  34134  sitgaddlemb  34182  eulerpartlemgvv  34210  eulerpartlemn  34215  probun  34253  ballotlem2  34322  ballotlemodife  34331  bnj252  34548  bnj253  34549  bnj255  34550  bnj345  34559  bnj133  34572  bnj976  34622  bnj1098  34628  bnj121  34715  bnj130  34719  bnj150  34721  bnj581  34753  bnj607  34761  bnj865  34768  bnj917  34779  bnj934  34780  bnj964  34788  bnj983  34796  bnj996  34801  bnj1021  34811  bnj1033  34814  bnj1047  34818  bnj1049  34819  bnj1090  34824  bnj1128  34835  bnj1175  34849  bnj1189  34854  bnj1253  34862  bnj1312  34903  exdifsn  34918  fineqvrep  34931  fineqvac  34933  erdszelem9  35027  erdszelem10  35028  pconnconn  35059  cvmliftiota  35129  fmlaomn0  35218  fmla0disjsuc  35226  fmlasucdisj  35227  dmopab3rexdif  35233  elmthm  35404  nepss  35540  xpab  35548  dfso2  35577  elrn3  35584  elpotr  35605  dfon2lem5  35611  dfon2lem7  35613  dfon2lem8  35614  elwlim  35647  wzel  35648  brtxp2  35705  brpprod3a  35710  eltrans  35715  dfon3  35716  dffix2  35729  dffun10  35738  elfuns  35739  brsingle  35741  brimg  35761  funpartfun  35767  funpartfv  35769  cgrxfr  35879  segletr  35938  outsideoftr  35953  neifg  36083  filnetlem4  36093  df3nandALT1  36111  bj-consensusALT  36283  bj-df-ifc  36284  bj-biexal3  36412  bj-nfnnfTEMP  36463  bj-denoteslem  36576  bj-denotes  36577  bj-ralvw  36585  bj-rexvw  36586  bj-rexcom4bv  36588  bj-rexcom4b  36589  bj-sbeq  36607  bj-inrab  36633  bj-rcleqf  36732  bj-dfmpoa  36825  bj-imdirco  36897  topdifinffinlem  37054  topdifinfeq  37057  relowlssretop  37070  relowlpssretop  37071  rdgeqoa  37077  domalom  37111  nlpineqsn  37115  fvineqsneq  37119  wl-ifpimpr  37173  wl-df3xor3  37177  wl-3xorbi  37180  wl-3xorbi2  37181  wl-2xor  37190  wl-2mintru2  37198  wl-dfclab  37291  rabiun  37294  phpreu  37305  fin2solem  37307  matunitlindflem2  37318  ptrest  37320  poimirlem25  37346  poimirlem27  37348  poimirlem30  37351  ismblfin  37362  ovoliunnfl  37363  voliunnfl  37365  volsupnfl  37366  itg2addnclem2  37373  fdc  37446  prdstotbnd  37495  isdrngo1  37657  ispridl  37735  ismaxidl  37741  impor  37782  selconj  37801  tradd  37806  scott0f  37870  r2alan  37947  inxpss3  38012  idinxpssinxp2  38016  idinxpssinxp3  38017  dfrel5  38044  ineleq  38052  moantr  38062  dfxrn2  38074  inxpxrn  38093  rnxrnres  38097  coss1cnvres  38115  1cossres  38127  cocossss  38134  cossssid4  38168  cossssid5  38169  cosscnvssid5  38176  cossid  38178  dfssr2  38197  cnvrefrelcoss2  38235  cosselcnvrefrels2  38236  eqvrelcoss  38315  eqvrelcoss2  38317  dfcoeleqvrel  38320  refrelredund4  38333  cnvepresdmqs  38351  dfcomember  38370  dfdisjALTV  38411  dfeldisj3  38417  dfeldisj4  38418  dfeldisj5  38419  disjres  38442  prter1  38577  islshp  38677  islshpat  38715  lcvbr2  38720  lcvnbtwn2  38725  cvrnbtwn3  38974  isatl  38997  ishlat1  39050  ishlat2  39051  cvrat4  39142  pmapglbx  39468  lhpexle3  39711  dib1dim  40864  diblsmopel  40870  lcfls1lem  41233  prjsperref  42260  prjspeclsp  42266  euabsn2w  42334  rexrabdioph  42451  dford4  42687  onsupuni  42894  dflim6  42930  tfsconcatlem  43002  naddgeoa  43061  ifpdfor2  43128  ifpdfan2  43130  ifpdfor  43132  ifpdfan  43133  ifpnot23b  43149  ifpnot23c  43151  ifpnot23d  43152  ifpim123g  43167  ifpbibib  43177  clss2lem  43278  imaiun1  43318  coiun1  43319  brfvrcld2  43359  iunrelexp0  43369  brtrclfv2  43394  snhesn  43453  dffrege76  43606  frege97  43627  frege98  43628  frege109  43639  frege110  43640  dffrege115  43645  frege131  43661  frege133  43663  ntrneineine1lem  43751  ntrneiel2  43753  ntrneiiso  43758  gneispace3  43800  scotteld  43920  ismnuprim  43968  ismnushort  43975  dfuniv2  43976  pm11.52  44061  pm11.58  44064  pm13.192  44084  impexpdcom  44191  sbc3or  44208  opelopab4  44227  uunT12p1  44476  uunT12p2  44477  uunT12p3  44478  uun2221  44489  uun2221p1  44490  uun2221p2  44491  undif3VD  44558  ndisj2  44652  nssrex  44687  rabssf  44720  bothtbothsame  46514  bothfbothsame  46515  aiffbtbat  46523  reuabaiotaiota  46700  2reu8i  46726  2reuimp0  46727  ichn  47028  dfodd2  47208  dfeven5  47238  dfodd7  47239  1nevenALTV  47263  oddprmne2  47287  dfvopnbgr2  47420  isuspgrim0lem  47450  gricer  47472  islindeps2  47866  isldepslvec2  47868  line2xlem  48141  rmotru  48190  reutru  48191  isnrm4  48264  iscnrm4  48288  isthincd2  48359  thinccic  48382  setrec1lem3  48435  aacllem  48549