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  1383  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  1917  equsv  2038  sbrimvwOLD  2131  sbcom2  2212  sb5  2313  nf5  2319  nf6  2320  sbrim  2341  sbnf  2348  sb6x  2496  2sb5rf  2504  2sb6rf  2505  sb4b  2507  sb5f  2530  sbequ8  2533  sbhb  2553  eu6lem  2601  eu1  2638  iseqsetv-cleq  2827  abbib  2832  issettru  2842  iseqsetv-clel  2843  issetlem  2844  cleqh  2893  cleqf  2954  sbabel  2958  necon3bii  3011  neor  3051  neorian  3054  rextru  3097  r19.26m  3125  r19.43  3134  3r19.43  3135  r2allem  3154  r19.23t  3262  ralcom4  3292  moel  3389  rabid2f  3446  eqv  3464  eqvf  3465  ralv  3480  rexv  3481  reuv  3482  rmov  3483  rexcom4b  3485  ceqsex4v  3507  ceqsex8v  3509  ceqsrexv  3612  rexab  3656  ralrab2  3659  rexrab2  3661  reu2  3686  reu3  3688  reueq  3698  2reuswap  3707  2reuswap2  3708  reuind  3714  2reu5lem3  3718  2rmoswap  3722  rmo2  3838  rmoanim  3846  rmoanimALT  3847  dfss3  3902  dfss3f  3905  nssrex  3978  ssabral  3992  rabss  3998  ssrabeq  4012  uniiunlem  4015  sspsstri  4036  npss  4044  raldifb  4088  inass  4127  uncom  4160  elsymdifxor  4208  nsspssun  4216  dfss4  4217  dfun2  4218  dfin2  4219  indi  4232  reupick3  4278  eq0f  4297  neq0f  4298  eq0ALT  4301  inssdif0  4325  dfnf5  4334  rabn0  4342  vss  4361  csbab  4401  disj  4406  disj3  4410  undisj1  4418  undisj2  4419  inundif  4438  undif  4441  undifr  4442  rabsssn  4629  exsnrex  4641  euabsn2  4686  euabsn  4687  raldifsni  4758  tppreqb  4768  prssg  4778  ssunsn  4787  prneimg2  4813  preqsn  4820  pwpr  4831  pwpw0  4834  dfuni2  4872  unissb  4904  elint2  4917  ssint  4927  uniintab  4949  dfiin2g  4992  iunid  5022  iunn0  5028  iunxun  5057  iunxiun  5060  iinpw  5069  disjor  5088  disjxiun  5103  dftr2  5218  dftr3  5221  dftr4  5222  vnexOLD  5276  inuni  5316  eusv2  5363  reusv2lem4  5368  rexxfr  5383  sspwb  5422  opthneg  5455  pwssun  5548  dfid3  5554  dffr6  5612  dffr2  5617  dffr2ALT  5618  opthprc  5720  elxp3  5722  xpiundir  5728  elvvOLD  5732  raliunxp  5824  cnvuni  5878  dmopab2rex  5909  dm0rn0OLD  5917  dfres3  5989  ssdmres  6019  elidinxp  6052  idinxpres  6055  dfima2  6074  args  6106  dffr3  6113  cotrg  6121  intasym  6125  asymref  6126  intirr  6128  xpnz  6166  xp11  6183  ssrnres  6186  xpimasn  6193  coiun  6275  coassOLD  6289  cnvso  6313  elsnxp  6318  dfpo2  6323  imaindm  6326  dffr4  6347  dfse3  6363  frpoind  6369  dflim2  6445  orddif  6485  dffun6  6575  dffun6f  6579  dffun7  6593  dffun9  6595  funfn  6596  svrelfun  6640  mptfnf  6702  dffn2  6739  dffn3  6750  fint  6789  dffn4  6830  dff1o4  6861  brprcneu  6904  brprcneuALT  6905  eqfnfv3  7060  fnreseql  7076  fsn  7166  ftpg  7190  abrexco  7277  imaiun  7278  dff13  7287  isof1oidb  7361  isof1oopb  7362  isocnv2  7368  eloprabga  7558  mpo2eqb  7581  elovmpo  7696  mpt3eqdv  7716  funmpt3  7717  mpt3fvd  7718  sorpss  7774  abexex  8015  elxp6  8067  elxp7  8068  releldm2  8086  opiota  8103  fnmpo  8113  frxp  8173  frxp2  8196  soseq  8211  cnvimadfsn  8225  mpoxneldm  8265  dftpos4  8298  frrlem9  8348  dfrecs3  8416  tfrlem7  8427  ondif1  8545  oarec  8606  oeeu  8648  brinxper  8783  0er  8792  eroveu  8869  erovlem  8870  elixpconst  8969  domen  9024  brsdom  9037  brdom2  9045  reuen1  9089  sbthlem10  9151  brsdom2  9156  xpf1o  9194  unfi  9222  sbthfilem  9249  onfin2  9268  0sdom1domALT  9274  modom  9278  marypha2lem3  9464  wemapsolem  9579  elom3  9684  dfom5  9686  brttrcl2  9750  ttrcltr  9752  ttrclse  9763  trcl  9764  epfrs  9767  frind  9789  rankf  9837  elhf3  9948  scottexsOLD  9978  scott0bsOLD  9980  cplem1OLD  9986  hta  9997  htaOLD  9998  setrec1lem3  10004  djuexb  10025  pm54.43lem  10118  alephsuc2  10196  iscard3  10209  aceq0  10234  aceq3lem  10236  dfac3  10237  dfac5lem2  10240  dfac5  10244  dfac7  10248  dfac12a  10264  kmlem12  10277  kmlem14  10279  kmlem15  10280  infmap2  10332  ackbij2  10357  dfacfin7  10514  ituniiun  10537  zorng  10619  brdom7disj  10647  entri2  10679  alephreg  10704  fpwwe2lem11  10763  fpwwe2lem12  10764  pwfseqlem1  10780  grutsk  10944  axgroth4  10954  grothprim  10956  grothtsk  10957  elni2  10999  ltsopi  11010  genpass  11131  psslinpr  11153  ltexprlem4  11161  ltresr  11262  infm3  12314  elnnz  12741  dfz2  12750  2rexuz  13065  nnwos  13080  eluz2b1  13084  qexALT  13129  elxr  13283  dflt2  13315  xrsupss  13477  xrinfmss  13478  elixx1  13523  elioo2  13555  dfrp2  13563  elioopnf  13612  elicopnf  13614  elfz1  13682  fznn  13764  fzp1nel  13783  fznn0  13791  preduz  13822  prinfzo0  13871  injresinj  13964  nn0opthlem1  14451  faclbnd4lem1  14476  hashfxnn0  14520  hashprdifel  14581  hashgt23el  14608  hashfun  14621  hashf1  14641  fz1isolem  14645  f1oun2prg  15109  brtrclfv  15196  shftdm  15265  rediv  15339  imdiv  15346  rexanre  15555  caubnd  15567  climreu  15764  prodmo  16144  dvdslelem  16520  3dvdsdec  16543  3dvds2dec  16544  bitsval  16635  smueqlem  16701  algcvgblem  16793  lcmfunsnlem2  16856  isprm2  16898  isprm3  16899  isprm4  16900  pythagtriplem2  17036  elgz  17150  hashbc0  17224  0ram  17239  isstruct  17371  issect  17969  isfull2  18129  isfth2  18133  fucinv  18192  eldmcoa  18281  isdrs  18516  submacs  19064  isnsg4  19418  isgim  19517  gaorb  19563  oppgid  19612  oppgsubm  19618  oppgcntz  19620  ispgp  19848  efgsdm  19986  efgcpbllema  20010  iscyg2  20138  isomnd  20379  omndmul2  20389  isrng  20418  isring  20505  isirred2  20693  opprirred  20694  isrnghm  20713  dfrhm2  20746  rimval  20772  isnzr2  20810  opprsubrng  20853  opprsubrg  20887  isdomn3  21008  drngid2  21052  issdrg  21087  islmod  21181  lss1d  21280  islmhm  21344  islmim  21379  lbsextlem2  21479  lidlnz  21572  dfprm2  21823  isphl  21978  elocv  22018  iunocv  22031  isobs  22070  islinds  22159  1mavmul  22907  matunitlindflem2  23039  toprntopon  23287  isbasis3g  23311  fctop  23366  cctop  23368  isclo2  23450  restsn  23532  lmbr  23620  ist0-3  23707  2ndcdisj  23819  1stccnp  23825  islocfin  23880  1stckgenlem  23916  txbas  23930  ptbasin  23940  tx2cn  23973  fbfinnfr  24204  fbasrn  24247  filuni  24248  ufinffr  24292  fin1aufil  24295  rnelfmlem  24315  flimrest  24346  alexsubALTlem3  24412  alexsubALTlem4  24413  tgphaus  24480  istlm  24548  iscusp2  24664  metuel2  24928  isngp2  24960  isnlm  25038  isphtpc  25359  phtpcer  25360  om1elbas  25397  isclm  25429  iscvsp  25493  iscph  25535  iscau3  25643  minveclem3b  25793  elovolm  25840  ioombl1lem4  25926  dyaddisj  25961  vitali  25978  itg1climres  26079  itg2seq  26107  itg2monolem1  26115  itg2mono  26118  limcrcl  26238  lhop1  26378  itgsubst  26413  mdegleb  26426  isuc1p  26503  ismon1p  26505  plydivex  26662  ellogdm  27013  1cubr  27216  atandm2  27251  birthdaylem3  27327  dmarea  27331  dchrelbas2  27610  dchrelbas4  27616  elno3  28058  nosgnn0  28061  nosepon  28068  nocvxminlem  28186  cutcuts  28213  cutbday  28216  dmcuts  28223  cutsf  28224  ltsrec  28233  made0  28295  addsprop  28408  negsproplem2  28461  negsprop  28467  mulsprop  28562  precsexlem10  28648  elzs2  28831  elnnzs  28833  bdayfinbndlem1  28899  recut  28926  axcontlem7  29594  nb3grpr  30009  nb3grpr2  30010  upgrwlkcompim  30269  wlkson  30281  wlkonprop  30283  wksonproplem  30333  ispth  30352  wwlknon  30492  wwlksnextinj  30534  wspthsnwspthsnon  30551  elwspths2spth  30605  rusgrnumwwlkl1  30606  clwwlkccatlem  30626  erclwwlkref  30657  frgr3v  30922  nmoubi  31420  nmobndseqi  31427  nmobndseqiALT  31428  minvecolem1  31522  isch2  31871  hlimreui  31887  isch3  31889  ocsh  31931  dfch2  32055  spanuni  32192  nonbooli  32299  5oalem7  32308  adjsym  32481  elbdop2  32519  dmadjss  32535  nmopub  32556  nmfnleub  32573  nmop0h  32639  pjssposi  32820  pjordi  32821  cvbr2  32931  cvnbtwn2  32935  mdsl2i  32970  cvmdi  32972  elat2  32988  atom1d  33001  chirredi  33042  cdj3i  33089  or3di  33145  opreu2reu1  33168  mo5f  33173  reuxfrdf  33175  rexunirn  33176  difrab2  33182  rabsspr  33185  rabsstp  33186  tpssg  33221  iuninc  33243  disjorf  33261  disjunsn  33276  rabfmpunirn  33335  aciunf1  33345  funcnv5mpt  33349  eliccelico  33455  elicoelioo  33456  isslmd  33852  islinds5  34020  ismxidl  34084  1arithufdlem4  34176  hasheuni  34821  pwsiga  34866  sigainb  34873  issros  34912  2ndmbfm  34997  omssubaddlem  35035  omssubadd  35036  sitgaddlemb  35084  eulerpartlemgvv  35112  eulerpartlemn  35117  probun  35155  ballotlem2  35225  ballotlemodife  35234  bnj252  35438  bnj253  35439  bnj255  35440  bnj345  35449  bnj133  35462  bnj976  35512  bnj1098  35518  bnj121  35604  bnj130  35608  bnj150  35610  bnj581  35642  bnj607  35650  bnj865  35657  bnj917  35668  bnj934  35669  bnj964  35677  bnj983  35685  bnj996  35690  bnj1021  35700  bnj1033  35703  bnj1047  35707  bnj1049  35708  bnj1090  35713  bnj1128  35724  bnj1175  35738  bnj1189  35743  bnj1253  35751  bnj1312  35792  rmo6  35814  exdifsn  35817  scott0bOLD  35869  fineqvrep  35916  fineqvac  35918  kard0  35956  kardexen  35965  onvf1odlem4  36068  vonf1wev  36070  vonf1owevOLD  36072  vonf1osev  36074  onprcf1acwevdlem1  36079  erdszelem9  36165  erdszelem10  36166  pconnconn  36197  cvmliftiota  36267  fmlaomn0  36356  fmla0disjsuc  36364  fmlasucdisj  36365  dmopab3rexdif  36371  elmthm  36542  antnestALT  36660  mirimanofffr  36663  nepss  36691  xpab  36699  dfso2  36728  elrn3  36735  elpotr  36751  dfon2lem5  36757  dfon2lem7  36759  dfon2lem8  36760  elwlim  36793  wzel  36794  brtxp2  36851  brpprod3a  36856  eltrans  36861  dfon3  36862  dffix2  36875  dffun10  36884  elfuns  36885  brsingle  36887  brimg  36907  funpartfun  36915  funpartfv  36917  cgrxfr  37028  segletr  37087  outsideoftr  37102  naddle  37176  neifg  37367  filnetlem4  37377  df3nandALT1  37395  weiunlem  37459  ttcwf3  37522  bj-consensusALT  37657  bj-df-ifc  37658  bj-exexalal  37684  bj-cbvaew  37751  bj-biexal3  37817  bj-alnnf  37847  bj-nfnnfTEMP  37892  bj-denoteslem  37991  bj-denotesALTV  37992  bj-ralvw  37999  bj-rexvw  38000  bj-rexcom4bv  38002  bj-rexcom4b  38003  bj-sbeq  38021  bj-inrab  38048  bj-rcleqf  38146  bj-resssxp  38176  bj-dfrel3  38180  bj-dfrel2  38184  relssresb  38188  bj-coi1  38196  bj-dfmpoa  38303  bj-imdirco  38372  topdifinffinlem  38531  topdifinfeq  38534  relowlssretop  38547  relowlpssretop  38548  rdgeqoa  38554  domalom  38588  nlpineqsn  38592  fvineqsneq  38596  wl-ifpimpr  38650  wl-df3xor3  38654  wl-3xorbi  38657  wl-3xorbi2  38658  wl-2xor  38667  wl-2mintru2  38675  wl-dfclab  38778  rabiun  38782  phpreu  38788  fin2solem  38790  ptrest  38798  poimirlem25  38824  poimirlem27  38826  poimirlem30  38829  ismblfin  38840  ovoliunnfl  38841  voliunnfl  38843  volsupnfl  38844  itg2addnclem2  38851  dfprop1  38906  fdc  38938  prdstotbnd  38987  isdrngo1  39149  ispridl  39227  ismaxidl  39233  impor  39274  selconj  39291  tradd  39296  r2alan  39442  inxpss3  39511  idinxpssinxp2  39515  idinxpssinxp3  39516  dfrel5  39537  ineleq  39545  ralmo  39551  ralrnmo  39552  ralrmo3  39555  moantr  39563  dfxrn2  39576  inxpxrn  39609  rnxrnres  39613  dfsuccl4  39665  coss1cnvres  39698  1cossres  39710  cocossss  39717  cossssid4  39751  cossssid5  39752  cosscnvssid5  39759  cossid  39761  dfssr2  39770  cnvrefrelcoss2  39808  cosselcnvrefrels2  39809  eqvrelcoss  39892  eqvrelcoss2  39894  dfcoeleqvrel  39897  refrelredund4  39910  cnvepresdmqs  39929  dfcomember  39948  dfdisjALTV  39989  disjimdmqseq  40000  dfeldisj3  40002  dfeldisj4  40003  dfeldisj5  40004  disjres  40035  prter1  40195  islshp  40295  islshpat  40333  lcvbr2  40338  lcvnbtwn2  40343  cvrnbtwn3  40592  isatl  40615  ishlat1  40668  ishlat2  40669  cvrat4  40759  pmapglbx  41085  lhpexle3  41328  dib1dim  42481  diblsmopel  42487  lcfls1lem  42850  prjsperref  43894  prjspeclsp  43900  euabsn2w  43950  rexrabdioph  44061  dford4  44296  onsupuni  44486  dflim6  44521  tfsconcatlem  44593  naddgeoa  44651  ifpdfor2  44717  ifpdfan2  44719  ifpdfor  44721  ifpdfan  44722  ifpnot23b  44738  ifpnot23c  44740  ifpnot23d  44741  ifpim123g  44756  ifpbibib  44766  clss2lem  44866  imaiun1  44906  coiun1  44907  brfvrcld2  44947  iunrelexp0  44957  brtrclfv2  44982  snhesn  45041  dffrege76  45194  frege97  45215  frege98  45216  frege109  45227  frege110  45228  dffrege115  45233  frege131  45249  frege133  45251  ntrneineine1lem  45339  ntrneiel2  45341  ntrneiiso  45346  gneispace3  45388  ismnuprim  45533  ismnushort  45540  dfuniv2  45541  pm11.52  45626  pm11.58  45629  pm13.192  45649  impexpdcom  45752  sbc3or  45769  opelopab4  45788  uunT12p1  46036  uunT12p2  46037  uunT12p3  46038  uun2221  46049  uun2221p1  46050  uun2221p2  46051  undif3VD  46118  modelaxreplem3  46228  permaxext  46253  permac8prim  46262  ndisj2  46336  rabssf  46401  wrddin2  48165  chndin2  48170  chnrin2  48175  bothtbothsame  48236  bothfbothsame  48237  aiffbtbat  48245  reuabaiotaiota  48424  2reu8i  48451  2reuimp0  48452  ichn  48805  dfodd2  49001  dfeven5  49031  dfodd7  49032  1nevenALTV  49056  oddprmne2  49080  dfvopnbgr2  49218  isuspgrim0lem  49258  gpg5nbgrvtx03starlem1  49433  gpg5nbgrvtx03starlem2  49434  gpg5nbgrvtx03starlem3  49435  gpg5nbgrvtx13starlem1  49436  gpg5nbgrvtx13starlem2  49437  gpg5nbgrvtx13starlem3  49438  gpg5edgnedg  49495  dfidom2  49765  islindeps2  49920  isldepslvec2  49922  line2xlem  50190  rmotru  50238  reutru  50239  elif0  50247  isnrm4  50370  iscnrm4  50393  homf0  50448  fuco2el  50759  isthincd2  50897  thinccic  50931  istermc2  50935  istermc3  50936  dftermc3  50991  dfrals2  51308  dfralseu2  51341  aacllem  51361