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  820  imor  853  imimorb  952  pm5.6  1003  nbi2  1017  casesifp  1077  3ancoma  1097  3ancomb  1098  3anrev  1100  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  2003  sbrimvw  2092  sbcom2  2174  sb5  2276  nf5  2282  nf6  2283  sbrim  2304  sbnf  2311  sb6x  2462  2sb5rf  2470  2sb6rf  2471  sb4b  2473  sb5f  2496  sbequ8  2499  sbhb  2519  eu6lem  2566  eu1  2603  iseqsetv-cleq  2793  issettru  2806  iseqsetv-clel  2807  issetlem  2808  cleqh  2857  cleqf  2920  sbabel  2924  necon3bii  2977  neor  3017  neorian  3020  rextru  3060  r19.26m  3090  r19.43  3101  3r19.43  3102  r2allem  3121  r19.23t  3233  ralcom4  3263  moel  3376  rabid2f  3437  eqv  3457  eqvf  3458  ralv  3474  rexv  3475  reuv  3476  rmov  3477  rexcom4b  3479  ceqsex4v  3504  ceqsex8v  3506  ceqsrexv  3621  rexab  3666  ralrab2  3669  rexrab2  3671  reu2  3696  reu3  3698  reueq  3708  2reuswap  3717  2reuswap2  3718  reuind  3724  2reu5lem3  3728  2rmoswap  3732  rmo2  3850  rmoanim  3857  rmoanimALT  3858  dfss3  3935  dfss3f  3938  ssabral  4028  rabss  4035  ssrabeq  4047  uniiunlem  4050  sspsstri  4068  npss  4076  dfdif3OLD  4081  raldifb  4112  uncom  4121  inass  4191  elsymdifxor  4223  nsspssun  4231  dfss4  4232  dfun2  4233  dfin2  4234  indi  4247  reupick3  4293  eq0f  4310  neq0f  4311  eq0  4313  eq0ALT  4314  dfnf5  4345  rabn0  4352  csbab  4403  vss  4409  disj  4413  disj3  4417  undisj1  4425  undisj2  4426  inundif  4442  undif  4445  undifr  4446  rabsssn  4632  exsnrex  4644  euabsn2  4689  euabsn  4690  raldifsni  4759  tppreqb  4769  pwpw0  4777  prssg  4783  ssunsn  4792  prneimg2  4819  preqsn  4826  pwpr  4865  dfuni2  4873  unissb  4903  unissbOLD  4904  elint2  4917  ssint  4928  uniintab  4950  dfiin2g  4996  iunid  5024  iunn0  5031  iunxun  5058  iunxiun  5061  iinpw  5070  disjor  5089  disjxiun  5104  dftr2  5216  dftr5OLD  5219  dftr3  5220  dftr4  5221  axrep6OLD  5244  vnex  5269  inuni  5305  eusv2  5351  reusv2lem4  5356  rexxfr  5371  sspwb  5409  opthneg  5441  pwssun  5530  dfid3  5536  dffr6  5594  dffr2  5599  dffr2ALT  5600  opthprc  5702  elxp3  5704  xpiundir  5710  elvv  5713  reliun  5779  inxpOLD  5796  raliunxp  5803  cnvuni  5850  dmopab2rex  5881  dm0rn0  5888  dfres3  5955  ssdmres  5984  elidinxp  6015  idinxpres  6018  dfima2  6033  args  6063  dffr3  6070  cotrg  6080  cotrgOLD  6081  cotrgOLDOLD  6082  intasym  6088  asymref  6089  intirr  6091  xpnz  6132  xp11  6148  ssrnres  6151  xpimasn  6158  coiun  6229  coass  6238  cnvso  6261  elsnxp  6264  dfpo2  6269  imaindm  6272  dffr4  6293  dfse3  6309  frpoind  6315  dflim2  6390  orddif  6430  dffun2OLDOLD  6523  dffun6  6524  dffun6f  6529  dffun7  6543  dffun9  6545  funfn  6546  svrelfun  6588  mptfnf  6653  dffn2  6690  dffn3  6700  fint  6739  dffn4  6778  dff1o4  6808  brprcneu  6848  brprcneuALT  6849  eqfnfv3  7005  fnreseql  7020  fsn  7107  ftpg  7128  abrexco  7218  imaiun  7219  dff13  7229  isof1oidb  7299  isof1oopb  7300  isocnv2  7306  eloprabga  7498  mpo2eqb  7521  elovmpo  7634  sorpss  7704  abexex  7950  elxp6  8002  elxp7  8003  releldm2  8022  opiota  8038  fnmpo  8048  frxp  8105  frxp2  8123  soseq  8138  cnvimadfsn  8151  mpoxneldm  8191  dftpos4  8224  frrlem9  8273  dfrecs3  8341  tfrlem7  8351  ondif1  8465  oarec  8526  oeeu  8567  brinxper  8700  0er  8709  eroveu  8785  erovlem  8786  elixpconst  8878  domen  8933  brsdom  8946  brdom2  8953  reuen1  8997  sbthlem10  9060  brsdom2  9065  xpf1o  9103  unfi  9135  sbthfilem  9162  onfin2  9180  0sdom1domALT  9186  modom  9191  marypha2lem3  9388  wemapsolem  9503  elom3  9601  dfom5  9603  brttrcl2  9667  ttrcltr  9669  ttrclse  9680  trcl  9681  epfrs  9684  frind  9703  rankf  9747  scottexs  9840  scott0s  9841  cplem1  9842  hta  9850  djuexb  9862  pm54.43lem  9953  alephsuc2  10033  iscard3  10046  aceq0  10071  aceq3lem  10073  dfac3  10074  dfac5lem2  10077  dfac5  10082  dfac7  10086  dfac12a  10102  kmlem12  10115  kmlem14  10117  kmlem15  10118  infmap2  10170  ackbij2  10195  dfacfin7  10352  ituniiun  10375  zorng  10457  brdom7disj  10484  entri2  10511  alephreg  10535  fpwwe2lem11  10594  fpwwe2lem12  10595  pwfseqlem1  10611  grutsk  10775  axgroth4  10785  grothprim  10787  grothtsk  10788  elni2  10830  ltsopi  10841  genpass  10962  psslinpr  10984  ltexprlem4  10992  ltresr  11093  infm3  12142  elnnz  12539  dfz2  12548  2rexuz  12859  nnwos  12874  eluz2b1  12878  qexALT  12923  elxr  13076  dflt2  13108  xrsupss  13269  xrinfmss  13270  elixx1  13315  elioo2  13347  dfrp2  13355  elioopnf  13404  elicopnf  13406  elfz1  13473  fznn  13553  fzp1nel  13572  fznn0  13580  preduz  13611  prinfzo0  13659  injresinj  13749  nn0opthlem1  14233  faclbnd4lem1  14258  hashfxnn0  14302  hashprdifel  14363  hashgt23el  14389  hashfun  14402  hashf1  14422  fz1isolem  14426  f1oun2prg  14883  brtrclfv  14968  shftdm  15037  rediv  15097  imdiv  15104  rexanre  15313  caubnd  15325  climreu  15522  prodmo  15902  dvdslelem  16279  3dvdsdec  16302  3dvds2dec  16303  bitsval  16394  smueqlem  16460  algcvgblem  16547  lcmfunsnlem2  16610  isprm2  16652  isprm3  16653  isprm4  16654  pythagtriplem2  16788  elgz  16902  hashbc0  16976  0ram  16991  isstruct  17122  issect  17715  isfull2  17875  isfth2  17879  fucinv  17938  eldmcoa  18027  isdrs  18262  submacs  18754  isnsg4  19099  isgim  19194  gaorb  19239  oppgid  19288  oppgsubm  19294  oppgcntz  19296  ispgp  19522  efgsdm  19660  efgcpbllema  19684  iscyg2  19812  isrng  20063  isring  20146  isirred2  20330  opprirred  20331  isrnghm  20350  dfrhm2  20383  isnzr2  20427  opprsubrng  20468  opprsubrg  20502  isdomn3  20624  drngid2  20661  issdrg  20697  islmod  20770  lss1d  20869  islmhm  20934  islmim  20969  lbsextlem2  21069  lidlnz  21152  dfprm2  21383  isphl  21537  elocv  21577  iunocv  21590  isobs  21629  islinds  21718  1mavmul  22435  toprntopon  22812  isbasis3g  22836  fctop  22891  cctop  22893  isclo2  22975  restsn  23057  lmbr  23145  ist0-3  23232  2ndcdisj  23343  1stccnp  23349  islocfin  23404  1stckgenlem  23440  txbas  23454  ptbasin  23464  tx2cn  23497  fbfinnfr  23728  fbasrn  23771  filuni  23772  ufinffr  23816  fin1aufil  23819  rnelfmlem  23839  flimrest  23870  alexsubALTlem3  23936  alexsubALTlem4  23937  tgphaus  24004  istlm  24072  iscusp2  24189  metuel2  24453  isngp2  24485  isnlm  24563  isphtpc  24893  phtpcer  24894  om1elbas  24932  isclm  24964  iscvsp  25028  iscph  25070  iscau3  25178  minveclem3b  25328  elovolm  25376  ioombl1lem4  25462  dyaddisj  25497  vitali  25514  itg1climres  25615  itg2seq  25643  itg2monolem1  25651  itg2mono  25654  limcrcl  25775  lhop1  25919  itgsubst  25956  mdegleb  25969  isuc1p  26046  ismon1p  26048  plydivex  26205  ellogdm  26548  1cubr  26752  atandm2  26787  birthdaylem3  26863  dmarea  26867  dchrelbas2  27148  dchrelbas4  27154  elno3  27567  nosgnn0  27570  nosepon  27577  nocvxminlem  27689  scutcut  27713  scutbday  27716  dmscut  27723  scutf  27724  sltrec  27732  made0  27785  addsprop  27883  negsproplem2  27935  negsprop  27941  mulsprop  28033  precsexlem10  28118  elzs2  28287  elnnzs  28289  recut  28347  0reno  28348  axcontlem7  28897  nb3grpr  29309  nb3grpr2  29310  upgrwlkcompim  29571  wlkson  29584  wlkonprop  29586  wksonproplem  29632  wksonproplemOLD  29633  ispth  29651  wwlknon  29787  wwlksnextinj  29829  wspthsnwspthsnon  29846  elwspths2spth  29897  rusgrnumwwlkl1  29898  clwwlkccatlem  29918  erclwwlkref  29949  frgr3v  30204  nmoubi  30701  nmobndseqi  30708  nmobndseqiALT  30709  minvecolem1  30803  isch2  31152  hlimreui  31168  isch3  31170  ocsh  31212  dfch2  31336  spanuni  31473  nonbooli  31580  5oalem7  31589  adjsym  31762  elbdop2  31800  dmadjss  31816  nmopub  31837  nmfnleub  31854  nmop0h  31920  pjssposi  32101  pjordi  32102  cvbr2  32212  cvnbtwn2  32216  mdsl2i  32251  cvmdi  32253  elat2  32269  atom1d  32282  chirredi  32323  cdj3i  32370  or3di  32388  opreu2reu1  32413  mo5f  32418  reuxfrdf  32420  rexunirn  32421  difrab2  32427  rabsspr  32430  rabsstp  32431  tpssg  32466  iuninc  32489  disjorf  32508  disjunsn  32523  rabfmpunirn  32577  aciunf1  32587  funcnv5mpt  32592  eliccelico  32700  elicoelioo  32701  isomnd  33015  omndmul2  33026  isslmd  33155  islinds5  33338  ismxidl  33433  1arithufdlem4  33518  hasheuni  34075  pwsiga  34120  sigainb  34126  issros  34165  2ndmbfm  34252  omssubaddlem  34290  omssubadd  34291  sitgaddlemb  34339  eulerpartlemgvv  34367  eulerpartlemn  34372  probun  34410  ballotlem2  34480  ballotlemodife  34489  bnj252  34693  bnj253  34694  bnj255  34695  bnj345  34704  bnj133  34717  bnj976  34767  bnj1098  34773  bnj121  34860  bnj130  34864  bnj150  34866  bnj581  34898  bnj607  34906  bnj865  34913  bnj917  34924  bnj934  34925  bnj964  34933  bnj983  34941  bnj996  34946  bnj1021  34956  bnj1033  34959  bnj1047  34963  bnj1049  34964  bnj1090  34969  bnj1128  34980  bnj1175  34994  bnj1189  34999  bnj1253  35007  bnj1312  35048  exdifsn  35069  fineqvrep  35085  fineqvac  35087  onvf1odlem4  35093  vonf1owev  35095  erdszelem9  35186  erdszelem10  35187  pconnconn  35218  cvmliftiota  35288  fmlaomn0  35377  fmla0disjsuc  35385  fmlasucdisj  35386  dmopab3rexdif  35392  elmthm  35563  antnestALT  35681  nepss  35705  xpab  35713  dfso2  35742  elrn3  35749  elpotr  35769  dfon2lem5  35775  dfon2lem7  35777  dfon2lem8  35778  elwlim  35811  wzel  35812  brtxp2  35869  brpprod3a  35874  eltrans  35879  dfon3  35880  dffix2  35893  dffun10  35902  elfuns  35903  brsingle  35905  brimg  35925  funpartfun  35931  funpartfv  35933  cgrxfr  36043  segletr  36102  outsideoftr  36117  neifg  36359  filnetlem4  36369  df3nandALT1  36387  weiunlem2  36451  bj-consensusALT  36567  bj-df-ifc  36568  bj-biexal3  36695  bj-nfnnfTEMP  36746  bj-denoteslem  36859  bj-denotesALTV  36860  bj-ralvw  36867  bj-rexvw  36868  bj-rexcom4bv  36870  bj-rexcom4b  36871  bj-sbeq  36889  bj-inrab  36915  bj-rcleqf  37013  bj-dfmpoa  37106  bj-imdirco  37178  topdifinffinlem  37335  topdifinfeq  37338  relowlssretop  37351  relowlpssretop  37352  rdgeqoa  37358  domalom  37392  nlpineqsn  37396  fvineqsneq  37400  wl-ifpimpr  37454  wl-df3xor3  37458  wl-3xorbi  37461  wl-3xorbi2  37462  wl-2xor  37471  wl-2mintru2  37479  wl-dfclab  37584  rabiun  37587  phpreu  37598  fin2solem  37600  matunitlindflem2  37611  ptrest  37613  poimirlem25  37639  poimirlem27  37641  poimirlem30  37644  ismblfin  37655  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  itg2addnclem2  37666  fdc  37739  prdstotbnd  37788  isdrngo1  37950  ispridl  38028  ismaxidl  38034  impor  38075  selconj  38094  tradd  38099  scott0f  38163  r2alan  38238  inxpss3  38302  idinxpssinxp2  38306  idinxpssinxp3  38307  dfrel5  38328  ineleq  38336  moantr  38346  dfxrn2  38358  inxpxrn  38381  rnxrnres  38385  coss1cnvres  38408  1cossres  38420  cocossss  38427  cossssid4  38461  cossssid5  38462  cosscnvssid5  38469  cossid  38471  dfssr2  38490  cnvrefrelcoss2  38528  cosselcnvrefrels2  38529  eqvrelcoss  38608  eqvrelcoss2  38610  dfcoeleqvrel  38613  refrelredund4  38626  cnvepresdmqs  38645  dfcomember  38664  dfdisjALTV  38705  dfeldisj3  38711  dfeldisj4  38712  dfeldisj5  38713  disjres  38736  prter1  38872  islshp  38972  islshpat  39010  lcvbr2  39015  lcvnbtwn2  39020  cvrnbtwn3  39269  isatl  39292  ishlat1  39345  ishlat2  39346  cvrat4  39437  pmapglbx  39763  lhpexle3  40006  dib1dim  41159  diblsmopel  41165  lcfls1lem  41528  prjsperref  42594  prjspeclsp  42600  euabsn2w  42667  rexrabdioph  42782  dford4  43018  onsupuni  43218  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  44235  ismnuprim  44283  ismnushort  44290  dfuniv2  44291  pm11.52  44376  pm11.58  44379  pm13.192  44399  impexpdcom  44505  sbc3or  44522  opelopab4  44541  uunT12p1  44789  uunT12p2  44790  uunT12p3  44791  uun2221  44802  uun2221p1  44803  uun2221p2  44804  undif3VD  44871  modelaxreplem3  44970  permaxext  44995  permac8prim  45004  ndisj2  45045  nssrex  45080  rabssf  45113  bothtbothsame  46900  bothfbothsame  46901  aiffbtbat  46909  reuabaiotaiota  47088  2reu8i  47114  2reuimp0  47115  ichn  47457  dfodd2  47637  dfeven5  47667  dfodd7  47668  1nevenALTV  47692  oddprmne2  47716  dfvopnbgr2  47853  isuspgrim0lem  47893  gpg5nbgrvtx03starlem1  48059  gpg5nbgrvtx03starlem2  48060  gpg5nbgrvtx03starlem3  48061  gpg5nbgrvtx13starlem1  48062  gpg5nbgrvtx13starlem2  48063  gpg5nbgrvtx13starlem3  48064  islindeps2  48472  isldepslvec2  48474  line2xlem  48742  rmotru  48791  reutru  48792  isnrm4  48919  iscnrm4  48942  homf0  48998  fuco2el  49301  isthincd2  49426  thinccic  49460  istermc2  49464  istermc3  49465  dftermc3  49520  setrec1lem3  49678  aacllem  49790