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 ⊢ (𝜑 ↔ 𝜒)

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  3bitr2i  302  3bitr2ri  303  3bitr4i  306  3bitr4ri  307  biluk  389  biancomi  467  dfbi2  479  imdistan  577  pm5.32  583  bianass  654  mpbiran  721  biadaniALT  832  imor  866  imimorb  965  pm5.6  1017  nbi2  1031  ifpdfbi  1084  casesifp  1092  3ancoma  1113  3ancomb  1114  3anrev  1116  4anpull2  1380  dfnan2  1521  nannan  1524  nanbi  1527  xorcom  1541  xorneg  1550  xorbi12i  1551  norcom  1557  noran  1559  norasslem1  1561  trunortru  1616  trunorfal  1617  cadan  1636  cadcomb  1640  nic-ax  1700  nic-axALT  1701  nf3  1813  19.43  1909  equsv  2030  sbrimvwOLD  2132  sbcom2  2213  sb5  2317  nf5  2323  nf6  2324  sbrim  2345  sbnf  2352  sb6x  2502  2sb5rf  2510  2sb6rf  2511  sb4b  2513  sb5f  2536  sbequ8  2539  sbhb  2559  eu6lem  2607  eu1  2644  iseqsetv-cleq  2833  issettru  2847  iseqsetv-clel  2848  issetlem  2849  cleqh  2898  cleqf  2959  sbabel  2963  necon3bii  3016  neor  3056  neorian  3059  rextru  3102  r19.26m  3130  r19.43  3139  3r19.43  3140  r2allem  3159  r19.23t  3267  ralcom4  3297  moel  3396  rabid2f  3454  eqv  3473  eqvf  3474  ralv  3489  rexv  3490  reuv  3491  rmov  3492  rexcom4b  3494  ceqsex4v  3516  ceqsex8v  3518  ceqsrexv  3623  rexab  3667  ralrab2  3670  rexrab2  3672  reu2  3697  reu3  3699  reueq  3709  2reuswap  3718  2reuswap2  3719  reuind  3725  2reu5lem3  3729  2rmoswap  3733  rmo2  3849  rmoanim  3856  rmoanimALT  3857  dfss3  3934  dfss3f  3937  nssrex  4010  ssabral  4026  rabss  4032  ssrabeq  4046  uniiunlem  4049  sspsstri  4068  npss  4076  dfdif3OLD  4081  raldifb  4111  uncom  4120  inass  4188  elsymdifxor  4221  nsspssun  4229  dfss4  4230  dfun2  4231  dfin2  4232  indi  4245  reupick3  4291  eq0f  4308  neq0f  4309  eq0ALT  4312  dfnf5  4344  rabn0  4352  csbab  4403  vss  4409  disj  4413  disj3  4417  undisj1  4425  undisj2  4426  inundif  4442  undif  4445  undifr  4446  rabsssn  4636  exsnrex  4648  euabsn2  4693  euabsn  4694  raldifsni  4764  tppreqb  4774  pwpw0  4780  prssg  4786  ssunsn  4795  prneimg2  4821  preqsn  4828  pwpr  4867  dfuni2  4875  unissb  4907  elint2  4920  ssint  4930  uniintab  4952  dfiin2g  4996  iunid  5026  iunn0  5032  iunxun  5061  iunxiun  5064  iinpw  5073  disjor  5092  disjxiun  5107  dftr2  5221  dftr3  5224  dftr4  5225  axrep6OLD  5249  vnexOLD  5280  inuni  5318  eusv2  5365  reusv2lem4  5370  rexxfr  5385  sspwb  5428  opthneg  5461  pwssun  5551  dfid3  5557  dffr6  5615  dffr2  5620  dffr2ALT  5621  opthprc  5723  elxp3  5725  xpiundir  5731  elvv  5734  raliunxp  5823  cnvuni  5874  dmopab2rex  5905  dm0rn0OLD  5913  dfres3  5981  ssdmres  6010  elidinxp  6044  idinxpres  6047  dfima2  6062  args  6092  dffr3  6099  cotrg  6109  intasym  6113  asymref  6114  intirr  6116  xpnz  6155  xp11  6172  ssrnres  6175  xpimasn  6182  coiun  6255  coass  6264  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  6668  dffn2  6705  dffn3  6716  fint  6755  dffn4  6796  dff1o4  6827  brprcneu  6869  brprcneuALT  6870  eqfnfv3  7025  fnreseql  7041  fsn  7129  ftpg  7151  abrexco  7240  imaiun  7241  dff13  7250  isof1oidb  7320  isof1oopb  7321  isocnv2  7327  eloprabga  7517  mpo2eqb  7540  elovmpo  7653  sorpss  7723  abexex  7964  elxp6  8016  elxp7  8017  releldm2  8036  opiota  8052  fnmpo  8062  frxp  8118  frxp2  8136  soseq  8151  cnvimadfsn  8164  mpoxneldm  8204  dftpos4  8237  frrlem9  8287  dfrecs3  8355  tfrlem7  8366  ondif1  8482  oarec  8543  oeeu  8585  brinxper  8720  0er  8729  eroveu  8806  erovlem  8807  elixpconst  8899  domen  8954  brsdom  8967  brdom2  8975  reuen1  9019  sbthlem10  9080  brsdom2  9085  xpf1o  9123  unfi  9151  sbthfilem  9178  onfin2  9197  0sdom1domALT  9203  modom  9207  marypha2lem3  9393  wemapsolem  9508  elom3  9613  dfom5  9615  brttrcl2  9679  ttrcltr  9681  ttrclse  9692  trcl  9693  epfrs  9696  frind  9718  rankf  9762  scottexs  9857  scott0s  9858  scotteld  9868  cplem1  9871  hta  9879  djuexb  9891  pm54.43lem  9982  alephsuc2  10060  iscard3  10073  aceq0  10098  aceq3lem  10100  dfac3  10101  dfac5lem2  10104  dfac5  10108  dfac7  10112  dfac12a  10128  kmlem12  10141  kmlem14  10143  kmlem15  10144  infmap2  10196  ackbij2  10221  dfacfin7  10379  ituniiun  10402  zorng  10484  brdom7disj  10511  entri2  10538  alephreg  10563  fpwwe2lem11  10622  fpwwe2lem12  10623  pwfseqlem1  10639  grutsk  10803  axgroth4  10813  grothprim  10815  grothtsk  10816  elni2  10858  ltsopi  10869  genpass  10990  psslinpr  11012  ltexprlem4  11020  ltresr  11121  infm3  12170  elnnz  12597  dfz2  12606  2rexuz  12920  nnwos  12935  eluz2b1  12939  qexALT  12984  elxr  13137  dflt2  13169  xrsupss  13331  xrinfmss  13332  elixx1  13377  elioo2  13409  dfrp2  13417  elioopnf  13466  elicopnf  13468  elfz1  13536  fznn  13616  fzp1nel  13635  fznn0  13643  preduz  13674  prinfzo0  13723  injresinj  13816  nn0opthlem1  14300  faclbnd4lem1  14325  hashfxnn0  14369  hashprdifel  14430  hashgt23el  14457  hashfun  14470  hashf1  14490  fz1isolem  14494  f1oun2prg  14950  brtrclfv  15035  shftdm  15104  rediv  15178  imdiv  15185  rexanre  15394  caubnd  15406  climreu  15603  prodmo  15986  dvdslelem  16363  3dvdsdec  16386  3dvds2dec  16387  bitsval  16478  smueqlem  16544  algcvgblem  16631  lcmfunsnlem2  16694  isprm2  16736  isprm3  16737  isprm4  16738  pythagtriplem2  16873  elgz  16987  hashbc0  17061  0ram  17076  isstruct  17208  issect  17806  isfull2  17966  isfth2  17970  fucinv  18029  eldmcoa  18118  isdrs  18353  submacs  18882  isnsg4  19229  isgim  19328  gaorb  19373  oppgid  19422  oppgsubm  19428  oppgcntz  19430  ispgp  19658  efgsdm  19796  efgcpbllema  19820  iscyg2  19948  isomnd  20189  omndmul2  20199  isrng  20228  isring  20315  isirred2  20499  opprirred  20500  isrnghm  20519  dfrhm2  20552  isnzr2  20597  opprsubrng  20640  opprsubrg  20674  isdomn3  20795  drngid2  20831  issdrg  20865  islmod  20959  lss1d  21058  islmhm  21122  islmim  21157  lbsextlem2  21257  lidlnz  21346  dfprm2  21588  isphl  21743  elocv  21783  iunocv  21796  isobs  21835  islinds  21924  1mavmul  22670  toprntopon  23047  isbasis3g  23071  fctop  23126  cctop  23128  isclo2  23210  restsn  23292  lmbr  23380  ist0-3  23467  2ndcdisj  23578  1stccnp  23584  islocfin  23639  1stckgenlem  23675  txbas  23689  ptbasin  23699  tx2cn  23732  fbfinnfr  23963  fbasrn  24006  filuni  24007  ufinffr  24051  fin1aufil  24054  rnelfmlem  24074  flimrest  24105  alexsubALTlem3  24171  alexsubALTlem4  24172  tgphaus  24239  istlm  24307  iscusp2  24423  metuel2  24687  isngp2  24719  isnlm  24797  isphtpc  25118  phtpcer  25119  om1elbas  25156  isclm  25188  iscvsp  25252  iscph  25294  iscau3  25402  minveclem3b  25552  elovolm  25599  ioombl1lem4  25685  dyaddisj  25720  vitali  25737  itg1climres  25838  itg2seq  25866  itg2monolem1  25874  itg2mono  25877  limcrcl  25998  lhop1  26138  itgsubst  26173  mdegleb  26186  isuc1p  26263  ismon1p  26265  plydivex  26423  ellogdm  26766  1cubr  26969  atandm2  27004  birthdaylem3  27080  dmarea  27084  dchrelbas2  27363  dchrelbas4  27369  elno3  27781  nosgnn0  27784  nosepon  27791  nocvxminlem  27909  cutcuts  27936  cutbday  27939  dmcuts  27946  cutsf  27947  ltsrec  27956  made0  28018  addsprop  28131  negsproplem2  28184  negsprop  28190  mulsprop  28285  precsexlem10  28371  elzs2  28554  elnnzs  28556  bdayfinbndlem1  28622  recut  28649  axcontlem7  29257  nb3grpr  29669  nb3grpr2  29670  upgrwlkcompim  29929  wlkson  29941  wlkonprop  29943  wksonproplem  29989  ispth  30007  wwlknon  30143  wwlksnextinj  30185  wspthsnwspthsnon  30202  elwspths2spth  30256  rusgrnumwwlkl1  30257  clwwlkccatlem  30277  erclwwlkref  30308  frgr3v  30563  nmoubi  31061  nmobndseqi  31068  nmobndseqiALT  31069  minvecolem1  31163  isch2  31512  hlimreui  31528  isch3  31530  ocsh  31572  dfch2  31696  spanuni  31833  nonbooli  31940  5oalem7  31949  adjsym  32122  elbdop2  32160  dmadjss  32176  nmopub  32197  nmfnleub  32214  nmop0h  32280  pjssposi  32461  pjordi  32462  cvbr2  32572  cvnbtwn2  32576  mdsl2i  32611  cvmdi  32613  elat2  32629  atom1d  32642  chirredi  32683  cdj3i  32730  or3di  32744  opreu2reu1  32767  mo5f  32772  reuxfrdf  32774  rexunirn  32775  difrab2  32781  rabsspr  32784  rabsstp  32785  tpssg  32820  iuninc  32842  disjorf  32861  disjunsn  32876  rabfmpunirn  32935  aciunf1  32945  funcnv5mpt  32949  eliccelico  33059  elicoelioo  33060  isslmd  33459  islinds5  33621  ismxidl  33686  1arithufdlem4  33778  hasheuni  34416  pwsiga  34461  sigainb  34467  issros  34506  2ndmbfm  34592  omssubaddlem  34630  omssubadd  34631  sitgaddlemb  34679  eulerpartlemgvv  34707  eulerpartlemn  34712  probun  34750  ballotlem2  34820  ballotlemodife  34829  bnj252  35033  bnj253  35034  bnj255  35035  bnj345  35044  bnj133  35057  bnj976  35107  bnj1098  35113  bnj121  35199  bnj130  35203  bnj150  35205  bnj581  35237  bnj607  35245  bnj865  35252  bnj917  35263  bnj934  35264  bnj964  35272  bnj983  35280  bnj996  35285  bnj1021  35295  bnj1033  35298  bnj1047  35302  bnj1049  35303  bnj1090  35308  bnj1128  35319  bnj1175  35333  bnj1189  35338  bnj1253  35346  bnj1312  35387  exdifsn  35408  fineqvrep  35446  fineqvac  35448  onvf1odlem4  35485  vonf1wev  35487  vonf1owevOLD  35489  vonf1osev  35491  erdszelem9  35586  erdszelem10  35587  pconnconn  35618  cvmliftiota  35688  fmlaomn0  35777  fmla0disjsuc  35785  fmlasucdisj  35786  dmopab3rexdif  35792  elmthm  35963  antnestALT  36081  nepss  36105  xpab  36113  dfso2  36142  elrn3  36149  elpotr  36166  dfon2lem5  36172  dfon2lem7  36174  dfon2lem8  36175  elwlim  36208  wzel  36209  brtxp2  36266  brpprod3a  36271  eltrans  36276  dfon3  36277  dffix2  36290  dffun10  36299  elfuns  36300  brsingle  36302  brimg  36322  funpartfun  36330  funpartfv  36332  cgrxfr  36442  segletr  36501  outsideoftr  36516  neifg  36767  filnetlem4  36777  df3nandALT1  36795  weiunlem  36859  ttcwf3  36922  bj-consensusALT  37057  bj-df-ifc  37058  bj-exexalal  37084  bj-cbvaew  37151  bj-biexal3  37217  bj-alnnf  37247  bj-nfnnfTEMP  37292  bj-denoteslem  37391  bj-denotesALTV  37392  bj-ralvw  37399  bj-rexvw  37400  bj-rexcom4bv  37402  bj-rexcom4b  37403  bj-sbeq  37421  bj-inrab  37447  bj-rcleqf  37545  bj-dfmpoa  37643  bj-imdirco  37717  topdifinffinlem  37876  topdifinfeq  37879  relowlssretop  37892  relowlpssretop  37893  rdgeqoa  37899  domalom  37933  nlpineqsn  37937  fvineqsneq  37941  wl-ifpimpr  37995  wl-df3xor3  37999  wl-3xorbi  38002  wl-3xorbi2  38003  wl-2xor  38012  wl-2mintru2  38020  wl-dfclab  38123  rabiun  38127  phpreu  38138  fin2solem  38140  matunitlindflem2  38151  ptrest  38153  poimirlem25  38179  poimirlem27  38181  poimirlem30  38184  ismblfin  38195  ovoliunnfl  38196  voliunnfl  38198  volsupnfl  38199  itg2addnclem2  38206  fdc  38279  prdstotbnd  38328  isdrngo1  38490  ispridl  38568  ismaxidl  38574  impor  38615  selconj  38634  tradd  38639  scott0f  38703  r2alan  38785  inxpss3  38854  idinxpssinxp2  38858  idinxpssinxp3  38859  dfrel5  38880  ineleq  38888  ralmo  38894  ralrnmo  38895  ralrmo3  38898  moantr  38906  dfxrn2  38919  inxpxrn  38952  rnxrnres  38956  dfsuccl4  39008  coss1cnvres  39041  1cossres  39053  cocossss  39060  cossssid4  39094  cossssid5  39095  cosscnvssid5  39102  cossid  39104  dfssr2  39113  cnvrefrelcoss2  39151  cosselcnvrefrels2  39152  eqvrelcoss  39235  eqvrelcoss2  39237  dfcoeleqvrel  39240  refrelredund4  39253  cnvepresdmqs  39272  dfcomember  39291  dfdisjALTV  39332  disjimdmqseq  39343  dfeldisj3  39345  dfeldisj4  39346  dfeldisj5  39347  disjres  39378  prter1  39538  islshp  39638  islshpat  39676  lcvbr2  39681  lcvnbtwn2  39686  cvrnbtwn3  39935  isatl  39958  ishlat1  40011  ishlat2  40012  cvrat4  40102  pmapglbx  40428  lhpexle3  40671  dib1dim  41824  diblsmopel  41830  lcfls1lem  42193  prjsperref  43223  prjspeclsp  43229  euabsn2w  43296  rexrabdioph  43406  dford4  43641  onsupuni  43841  dflim6  43876  tfsconcatlem  43948  naddgeoa  44006  ifpdfor2  44072  ifpdfan2  44074  ifpdfor  44076  ifpdfan  44077  ifpnot23b  44093  ifpnot23c  44095  ifpnot23d  44096  ifpim123g  44111  ifpbibib  44121  clss2lem  44222  imaiun1  44262  coiun1  44263  brfvrcld2  44303  iunrelexp0  44313  brtrclfv2  44338  snhesn  44397  dffrege76  44550  frege97  44571  frege98  44572  frege109  44583  frege110  44584  dffrege115  44589  frege131  44605  frege133  44607  ntrneineine1lem  44695  ntrneiel2  44697  ntrneiiso  44702  gneispace3  44744  ismnuprim  44889  ismnushort  44896  dfuniv2  44897  pm11.52  44982  pm11.58  44985  pm13.192  45005  impexpdcom  45109  sbc3or  45126  opelopab4  45145  uunT12p1  45393  uunT12p2  45394  uunT12p3  45395  uun2221  45406  uun2221p1  45407  uun2221p2  45408  undif3VD  45475  modelaxreplem3  45574  permaxext  45599  permac8prim  45608  ndisj2  45656  rabssf  45722  bothtbothsame  47518  bothfbothsame  47519  aiffbtbat  47527  reuabaiotaiota  47706  2reu8i  47732  2reuimp0  47733  ichn  48087  dfodd2  48283  dfeven5  48313  dfodd7  48314  1nevenALTV  48338  oddprmne2  48362  dfvopnbgr2  48500  isuspgrim0lem  48540  gpg5nbgrvtx03starlem1  48715  gpg5nbgrvtx03starlem2  48716  gpg5nbgrvtx03starlem3  48717  gpg5nbgrvtx13starlem1  48718  gpg5nbgrvtx13starlem2  48719  gpg5nbgrvtx13starlem3  48720  gpg5edgnedg  48777  dfidom2  48990  islindeps2  49141  isldepslvec2  49143  line2xlem  49411  rmotru  49459  reutru  49460  isnrm4  49587  iscnrm4  49610  homf0  49665  fuco2el  49968  isthincd2  50093  thinccic  50127  istermc2  50131  istermc3  50132  dftermc3  50187  setrec1lem3  50345  aacllem  50457