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  853  imimorb  952  pm5.6  1003  nbi2  1017  casesifp  1077  3ancoma  1097  3ancomb  1098  3anrev  1100  dfnan2  1490  nannan  1493  nanbi  1496  xorcom  1510  xorneg  1519  xorbi12i  1520  norcom  1526  noran  1528  norasslem1  1530  trunortru  1585  trunorfal  1586  cadan  1605  cadcomb  1609  nic-ax  1669  nic-axALT  1670  nf3  1782  nfnbiOLD  1852  19.43  1879  equsv  1999  sbrimvw  2088  sbcom2  2170  sb5  2273  nf5  2280  nf6  2281  sbrim  2302  sbnf  2310  sb6x  2466  2sb5rf  2474  2sb6rf  2475  sb4b  2477  sb5f  2500  sbequ8  2503  sbhb  2523  eu6lem  2570  eu1  2607  iseqsetv-cleq  2803  issettru  2816  iseqsetv-clel  2817  issetlem  2818  cleqh  2868  cleqf  2931  sbabel  2935  necon3bii  2990  neor  3031  neorian  3034  rextru  3074  r19.26m  3107  r19.43  3119  r2allem  3139  r19.23t  3252  ralcom4  3283  rexcomOLD  3288  moel  3399  moelOLD  3402  rabid2f  3465  rabid2OLD  3468  eqv  3487  eqvf  3488  ralv  3505  rexv  3506  reuv  3507  rmov  3508  rexcom4b  3510  ceqsex4v  3537  ceqsex8v  3539  ceqsrexv  3654  rexab  3702  ralrab2  3706  rexrab2  3708  reu2  3733  reu3  3735  reueq  3745  2reuswap  3754  2reuswap2  3755  reuind  3761  2reu5lem3  3765  2rmoswap  3769  rmo2  3895  rmoanim  3902  rmoanimALT  3903  dfss3  3983  dfss3f  3986  ssabral  4074  rabss  4081  ssrabeq  4093  uniiunlem  4096  sspsstri  4114  npss  4122  dfdif3OLD  4127  raldifb  4158  uncom  4167  inass  4235  elsymdifxor  4265  nsspssun  4273  dfss4  4274  dfun2  4275  dfin2  4276  indi  4289  reupick3  4335  eq0f  4352  neq0f  4353  eq0  4355  eq0ALT  4356  dfnf5  4387  rabn0  4394  csbab  4445  vss  4451  disj  4455  disj3  4459  undisj1  4467  undisj2  4468  inundif  4484  undif  4487  undifr  4488  rabsssn  4672  exsnrex  4684  euabsn2  4729  euabsn  4730  raldifsni  4799  tppreqb  4809  pwpw0  4817  prssg  4823  ssunsn  4832  prneimg2  4859  preqsn  4866  pwpr  4905  dfuni2  4913  unissb  4943  unissbOLD  4944  elint2  4957  ssint  4968  uniintab  4990  dfiin2g  5036  iunid  5064  iunn0  5071  iunxun  5098  iunxiun  5101  iinpw  5110  disjor  5129  disjxiun  5144  dftr2  5266  dftr5OLD  5269  dftr3  5270  dftr4  5271  axrep6OLD  5294  vnex  5319  inuni  5355  eusv2  5401  reusv2lem4  5406  rexxfr  5421  sspwb  5459  opthneg  5491  pwssun  5579  dfid3  5585  dffr6  5643  dffr2  5649  dffr2ALT  5650  opthprc  5752  elxp3  5754  xpiundir  5759  elvv  5762  reliun  5828  inxpOLD  5845  raliunxp  5852  cnvuni  5899  dmopab2rex  5930  dm0rn0  5937  dfres3  6004  ssdmres  6032  elidinxp  6063  idinxpres  6066  dfima2  6081  args  6112  dffr3  6119  cotrg  6129  cotrgOLD  6130  cotrgOLDOLD  6131  intasym  6137  asymref  6138  intirr  6140  xpnz  6180  xp11  6196  ssrnres  6199  xpimasn  6206  coiun  6277  coass  6286  cnvso  6309  elsnxp  6312  dfpo2  6317  imaindm  6320  dffr4  6342  dfse3  6358  frpoind  6364  wfiOLD  6373  dflim2  6442  orddif  6481  dffun2OLDOLD  6574  dffun6  6575  dffun6f  6580  dffun7  6594  dffun9  6596  funfn  6597  svrelfun  6639  mptfnf  6703  dffn2  6738  dffn3  6748  fint  6787  dffn4  6826  dff1o4  6856  brprcneu  6896  brprcneuALT  6897  eqfnfv3  7052  fnreseql  7067  fsn  7154  ftpg  7175  abrexco  7263  imaiun  7264  dff13  7274  isof1oidb  7343  isof1oopb  7344  isocnv2  7350  eloprabga  7540  mpo2eqb  7564  elovmpo  7677  sorpss  7746  abexex  7994  elxp6  8046  elxp7  8047  releldm2  8066  opiota  8082  fnmpo  8092  frxp  8149  frxp2  8167  soseq  8182  cnvimadfsn  8195  mpoxneldm  8235  dftpos4  8268  frrlem9  8317  wfrlem8OLD  8354  wfrfunOLD  8357  dfrecs3  8410  dfrecs3OLD  8411  tfrlem7  8421  ondif1  8537  oarec  8598  oeeu  8639  brinxper  8772  0er  8781  eroveu  8850  erovlem  8851  elixpconst  8943  domen  9000  brsdom  9013  brdom2  9020  reuen1  9064  sbthlem10  9130  brsdom2  9135  xpf1o  9177  unfi  9209  sbthfilem  9235  onfin2  9265  0sdom1domALT  9272  modom  9277  marypha2lem3  9474  wemapsolem  9587  elom3  9685  dfom5  9687  brttrcl2  9751  ttrcltr  9753  ttrclse  9764  trcl  9765  epfrs  9768  frind  9787  rankf  9831  scottexs  9924  scott0s  9925  cplem1  9926  hta  9934  djuexb  9946  pm54.43lem  10037  alephsuc2  10117  iscard3  10130  aceq0  10155  aceq3lem  10157  dfac3  10158  dfac5lem2  10161  dfac5  10166  dfac7  10170  dfac12a  10186  kmlem12  10199  kmlem14  10201  kmlem15  10202  infmap2  10254  ackbij2  10279  dfacfin7  10436  ituniiun  10459  zorng  10541  brdom7disj  10568  entri2  10595  alephreg  10619  fpwwe2lem11  10678  fpwwe2lem12  10679  pwfseqlem1  10695  grutsk  10859  axgroth4  10869  grothprim  10871  grothtsk  10872  elni2  10914  ltsopi  10925  genpass  11046  psslinpr  11068  ltexprlem4  11076  ltresr  11177  1re  11258  infm3  12224  elnnz  12620  dfz2  12629  2rexuz  12939  nnwos  12954  eluz2b1  12958  qexALT  13003  elxr  13155  dflt2  13186  xrsupss  13347  xrinfmss  13348  elixx1  13392  elioo2  13424  dfrp2  13432  elioopnf  13479  elicopnf  13481  elfz1  13548  fznn  13628  fzp1nel  13647  fznn0  13655  preduz  13686  prinfzo0  13734  injresinj  13823  nn0opthlem1  14303  faclbnd4lem1  14328  hashfxnn0  14372  hashprdifel  14433  hashgt23el  14459  hashfun  14472  hashf1  14492  fz1isolem  14496  f1oun2prg  14952  brtrclfv  15037  shftdm  15106  rediv  15166  imdiv  15173  rexanre  15381  caubnd  15393  climreu  15588  prodmo  15968  dvdslelem  16342  3dvdsdec  16365  3dvds2dec  16366  bitsval  16457  smueqlem  16523  algcvgblem  16610  lcmfunsnlem2  16673  isprm2  16715  isprm3  16716  isprm4  16717  pythagtriplem2  16850  elgz  16964  hashbc0  17038  0ram  17053  isstruct  17185  issect  17800  isfull2  17964  isfth2  17968  fucinv  18029  eldmcoa  18118  isdrs  18358  submacs  18852  isnsg4  19197  isgim  19292  gaorb  19337  oppgid  19389  oppgsubm  19395  oppgcntz  19397  ispgp  19624  efgsdm  19762  efgcpbllema  19786  iscyg2  19914  isrng  20171  isring  20254  isirred2  20437  opprirred  20438  isrnghm  20457  dfrhm2  20490  isnzr2  20534  opprsubrng  20575  opprsubrg  20609  isdomn3  20731  drngid2  20768  issdrg  20805  islmod  20878  lss1d  20978  islmhm  21043  islmim  21078  lbsextlem2  21178  lidlnz  21269  dfprm2  21501  isphl  21663  elocv  21703  iunocv  21716  isobs  21757  islinds  21846  1mavmul  22569  toprntopon  22946  isbasis3g  22971  fctop  23026  cctop  23028  isclo2  23111  restsn  23193  lmbr  23281  ist0-3  23368  2ndcdisj  23479  1stccnp  23485  islocfin  23540  1stckgenlem  23576  txbas  23590  ptbasin  23600  tx2cn  23633  fbfinnfr  23864  fbasrn  23907  filuni  23908  ufinffr  23952  fin1aufil  23955  rnelfmlem  23975  flimrest  24006  alexsubALTlem3  24072  alexsubALTlem4  24073  tgphaus  24140  istlm  24208  iscusp2  24326  metuel2  24593  isngp2  24625  isnlm  24711  isphtpc  25039  phtpcer  25040  om1elbas  25078  isclm  25110  iscvsp  25174  iscph  25217  iscau3  25325  minveclem3b  25475  elovolm  25523  ioombl1lem4  25609  dyaddisj  25644  vitali  25661  itg1climres  25763  itg2seq  25791  itg2monolem1  25799  itg2mono  25802  limcrcl  25923  lhop1  26067  itgsubst  26104  mdegleb  26117  isuc1p  26194  ismon1p  26196  plydivex  26353  ellogdm  26695  1cubr  26899  atandm2  26934  birthdaylem3  27010  dmarea  27014  dchrelbas2  27295  dchrelbas4  27301  elno3  27714  nosgnn0  27717  nosepon  27724  nocvxminlem  27836  scutcut  27860  scutbday  27863  dmscut  27870  scutf  27871  sltrec  27879  made0  27926  addsprop  28023  negsproplem2  28075  negsprop  28081  mulsprop  28170  precsexlem10  28254  elzs2  28399  elnnzs  28401  recut  28442  0reno  28443  axcontlem7  28999  nb3grpr  29413  nb3grpr2  29414  upgrwlkcompim  29675  wlkson  29688  wlkonprop  29690  wksonproplem  29736  wksonproplemOLD  29737  ispth  29755  wwlknon  29886  wwlksnextinj  29928  wspthsnwspthsnon  29945  elwspths2spth  29996  rusgrnumwwlkl1  29997  clwwlkccatlem  30017  erclwwlkref  30048  frgr3v  30303  nmoubi  30800  nmobndseqi  30807  nmobndseqiALT  30808  minvecolem1  30902  isch2  31251  hlimreui  31267  isch3  31269  ocsh  31311  dfch2  31435  spanuni  31572  nonbooli  31679  5oalem7  31688  adjsym  31861  elbdop2  31899  dmadjss  31915  nmopub  31936  nmfnleub  31953  nmop0h  32019  pjssposi  32200  pjordi  32201  cvbr2  32311  cvnbtwn2  32315  mdsl2i  32350  cvmdi  32352  elat2  32368  atom1d  32381  chirredi  32422  cdj3i  32469  or3di  32487  opreu2reu1  32511  mo5f  32516  reuxfrdf  32518  rexunirn  32519  difrab2  32525  rabsspr  32528  rabsstp  32529  iuninc  32580  disjorf  32598  disjunsn  32613  rabfmpunirn  32669  aciunf1  32679  funcnv5mpt  32684  eliccelico  32785  elicoelioo  32786  isomnd  33060  omndmul2  33071  isslmd  33190  islinds5  33374  ismxidl  33469  1arithufdlem4  33554  hasheuni  34065  pwsiga  34110  sigainb  34116  issros  34155  2ndmbfm  34242  omssubaddlem  34280  omssubadd  34281  sitgaddlemb  34329  eulerpartlemgvv  34357  eulerpartlemn  34362  probun  34400  ballotlem2  34469  ballotlemodife  34478  bnj252  34695  bnj253  34696  bnj255  34697  bnj345  34706  bnj133  34719  bnj976  34769  bnj1098  34775  bnj121  34862  bnj130  34866  bnj150  34868  bnj581  34900  bnj607  34908  bnj865  34915  bnj917  34926  bnj934  34927  bnj964  34935  bnj983  34943  bnj996  34948  bnj1021  34958  bnj1033  34961  bnj1047  34965  bnj1049  34966  bnj1090  34971  bnj1128  34982  bnj1175  34996  bnj1189  35001  bnj1253  35009  bnj1312  35050  exdifsn  35071  fineqvrep  35087  fineqvac  35089  erdszelem9  35183  erdszelem10  35184  pconnconn  35215  cvmliftiota  35285  fmlaomn0  35374  fmla0disjsuc  35382  fmlasucdisj  35383  dmopab3rexdif  35389  elmthm  35560  nepss  35697  xpab  35705  dfso2  35734  elrn3  35741  elpotr  35762  dfon2lem5  35768  dfon2lem7  35770  dfon2lem8  35771  elwlim  35804  wzel  35805  brtxp2  35862  brpprod3a  35867  eltrans  35872  dfon3  35873  dffix2  35886  dffun10  35895  elfuns  35896  brsingle  35898  brimg  35918  funpartfun  35924  funpartfv  35926  cgrxfr  36036  segletr  36095  outsideoftr  36110  neifg  36353  filnetlem4  36363  df3nandALT1  36381  weiunlem2  36445  bj-consensusALT  36561  bj-df-ifc  36562  bj-biexal3  36689  bj-nfnnfTEMP  36740  bj-denoteslem  36853  bj-denotesALTV  36854  bj-ralvw  36861  bj-rexvw  36862  bj-rexcom4bv  36864  bj-rexcom4b  36865  bj-sbeq  36883  bj-inrab  36909  bj-rcleqf  37007  bj-dfmpoa  37100  bj-imdirco  37172  topdifinffinlem  37329  topdifinfeq  37332  relowlssretop  37345  relowlpssretop  37346  rdgeqoa  37352  domalom  37386  nlpineqsn  37390  fvineqsneq  37394  wl-ifpimpr  37448  wl-df3xor3  37452  wl-3xorbi  37455  wl-3xorbi2  37456  wl-2xor  37465  wl-2mintru2  37473  wl-dfclab  37576  rabiun  37579  phpreu  37590  fin2solem  37592  matunitlindflem2  37603  ptrest  37605  poimirlem25  37631  poimirlem27  37633  poimirlem30  37636  ismblfin  37647  ovoliunnfl  37648  voliunnfl  37650  volsupnfl  37651  itg2addnclem2  37658  fdc  37731  prdstotbnd  37780  isdrngo1  37942  ispridl  38020  ismaxidl  38026  impor  38067  selconj  38086  tradd  38091  scott0f  38155  r2alan  38230  inxpss3  38295  idinxpssinxp2  38299  idinxpssinxp3  38300  dfrel5  38327  ineleq  38335  moantr  38345  dfxrn2  38357  inxpxrn  38376  rnxrnres  38380  coss1cnvres  38398  1cossres  38410  cocossss  38417  cossssid4  38451  cossssid5  38452  cosscnvssid5  38459  cossid  38461  dfssr2  38480  cnvrefrelcoss2  38518  cosselcnvrefrels2  38519  eqvrelcoss  38598  eqvrelcoss2  38600  dfcoeleqvrel  38603  refrelredund4  38616  cnvepresdmqs  38634  dfcomember  38653  dfdisjALTV  38694  dfeldisj3  38700  dfeldisj4  38701  dfeldisj5  38702  disjres  38725  prter1  38860  islshp  38960  islshpat  38998  lcvbr2  39003  lcvnbtwn2  39008  cvrnbtwn3  39257  isatl  39280  ishlat1  39333  ishlat2  39334  cvrat4  39425  pmapglbx  39751  lhpexle3  39994  dib1dim  41147  diblsmopel  41153  lcfls1lem  41516  prjsperref  42592  prjspeclsp  42598  euabsn2w  42665  rexrabdioph  42781  dford4  43017  onsupuni  43217  dflim6  43253  tfsconcatlem  43325  naddgeoa  43383  ifpdfor2  43450  ifpdfan2  43452  ifpdfor  43454  ifpdfan  43455  ifpnot23b  43471  ifpnot23c  43473  ifpnot23d  43474  ifpim123g  43489  ifpbibib  43499  clss2lem  43600  imaiun1  43640  coiun1  43641  brfvrcld2  43681  iunrelexp0  43691  brtrclfv2  43716  snhesn  43775  dffrege76  43928  frege97  43949  frege98  43950  frege109  43961  frege110  43962  dffrege115  43967  frege131  43983  frege133  43985  ntrneineine1lem  44073  ntrneiel2  44075  ntrneiiso  44080  gneispace3  44122  scotteld  44241  ismnuprim  44289  ismnushort  44296  dfuniv2  44297  pm11.52  44382  pm11.58  44385  pm13.192  44405  impexpdcom  44512  sbc3or  44529  opelopab4  44548  uunT12p1  44797  uunT12p2  44798  uunT12p3  44799  uun2221  44810  uun2221p1  44811  uun2221p2  44812  undif3VD  44879  modelaxreplem3  44944  ndisj2  44990  nssrex  45025  rabssf  45058  bothtbothsame  46848  bothfbothsame  46849  aiffbtbat  46857  reuabaiotaiota  47036  2reu8i  47062  2reuimp0  47063  ichn  47380  dfodd2  47560  dfeven5  47590  dfodd7  47591  1nevenALTV  47615  oddprmne2  47639  dfvopnbgr2  47776  isuspgrim0lem  47808  gpg5nbgrvtx03starlem1  47958  gpg5nbgrvtx03starlem2  47959  gpg5nbgrvtx03starlem3  47960  gpg5nbgrvtx13starlem1  47961  gpg5nbgrvtx13starlem2  47962  gpg5nbgrvtx13starlem3  47963  islindeps2  48328  isldepslvec2  48330  line2xlem  48602  rmotru  48651  reutru  48652  isnrm4  48726  iscnrm4  48750  isthincd2  48837  thinccic  48861  setrec1lem3  48919  aacllem  49031