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  643  mpbiran  710  biadaniALT  821  imor  854  imimorb  953  pm5.6  1004  nbi2  1018  casesifp  1078  3ancoma  1098  3ancomb  1099  3anrev  1101  dfnan2  1496  nannan  1499  nanbi  1502  xorcom  1516  xorneg  1525  xorbi12i  1526  norcom  1532  noran  1534  norasslem1  1536  trunortru  1591  trunorfal  1592  cadan  1611  cadcomb  1615  nic-ax  1675  nic-axALT  1676  nf3  1788  19.43  1884  equsv  2005  sbrimvw  2097  sbcom2  2179  sb5  2283  nf5  2289  nf6  2290  sbrim  2311  sbnf  2318  sb6x  2469  2sb5rf  2477  2sb6rf  2478  sb4b  2480  sb5f  2503  sbequ8  2506  sbhb  2526  eu6lem  2574  eu1  2611  iseqsetv-cleq  2801  issettru  2815  iseqsetv-clel  2816  issetlem  2817  cleqh  2866  cleqf  2928  sbabel  2932  necon3bii  2985  neor  3025  neorian  3028  rextru  3069  r19.26m  3097  r19.43  3106  3r19.43  3107  r2allem  3126  r19.23t  3234  ralcom4  3264  moel  3363  rabid2f  3421  eqv  3440  eqvf  3441  ralv  3457  rexv  3458  reuv  3459  rmov  3460  rexcom4b  3462  ceqsex4v  3485  ceqsex8v  3487  ceqsrexv  3598  rexab  3642  ralrab2  3645  rexrab2  3647  reu2  3672  reu3  3674  reueq  3684  2reuswap  3693  2reuswap2  3694  reuind  3700  2reu5lem3  3704  2rmoswap  3708  rmo2  3826  rmoanim  3833  rmoanimALT  3834  dfss3  3911  dfss3f  3914  ssabral  4005  rabss  4011  ssrabeq  4025  uniiunlem  4028  sspsstri  4046  npss  4054  dfdif3OLD  4059  raldifb  4090  uncom  4099  inass  4169  elsymdifxor  4201  nsspssun  4209  dfss4  4210  dfun2  4211  dfin2  4212  indi  4225  reupick3  4271  eq0f  4288  neq0f  4289  eq0ALT  4292  dfnf5  4323  rabn0  4330  csbab  4381  vss  4387  disj  4391  disj3  4395  undisj1  4403  undisj2  4404  inundif  4420  undif  4423  undifr  4424  rabsssn  4613  exsnrex  4625  euabsn2  4670  euabsn  4671  raldifsni  4739  tppreqb  4749  pwpw0  4757  prssg  4763  ssunsn  4772  prneimg2  4799  preqsn  4806  pwpr  4845  dfuni2  4853  unissb  4884  elint2  4897  ssint  4907  uniintab  4929  dfiin2g  4974  iunid  5004  iunn0  5010  iunxun  5037  iunxiun  5040  iinpw  5049  disjor  5068  disjxiun  5083  dftr2  5195  dftr3  5198  dftr4  5199  axrep6OLD  5222  vnex  5251  inuni  5287  eusv2  5333  reusv2lem4  5338  rexxfr  5353  sspwb  5396  opthneg  5429  pwssun  5516  dfid3  5522  dffr6  5580  dffr2  5585  dffr2ALT  5586  opthprc  5688  elxp3  5690  xpiundir  5696  elvv  5699  inxpOLD  5781  raliunxp  5788  cnvuni  5835  dmopab2rex  5866  dm0rn0OLD  5874  dfres3  5943  ssdmres  5972  elidinxp  6003  idinxpres  6006  dfima2  6021  args  6051  dffr3  6058  cotrg  6068  intasym  6072  asymref  6073  intirr  6075  xpnz  6117  xp11  6133  ssrnres  6136  xpimasn  6143  coiun  6215  coass  6224  cnvso  6246  elsnxp  6249  dfpo2  6254  imaindm  6257  dffr4  6278  dfse3  6294  frpoind  6300  dflim2  6375  orddif  6415  dffun6  6503  dffun6f  6507  dffun7  6519  dffun9  6521  funfn  6522  svrelfun  6564  mptfnf  6627  dffn2  6664  dffn3  6674  fint  6713  dffn4  6752  dff1o4  6782  brprcneu  6824  brprcneuALT  6825  eqfnfv3  6979  fnreseql  6994  fsn  7082  ftpg  7103  abrexco  7192  imaiun  7193  dff13  7202  isof1oidb  7272  isof1oopb  7273  isocnv2  7279  eloprabga  7469  mpo2eqb  7492  elovmpo  7605  sorpss  7675  abexex  7917  elxp6  7969  elxp7  7970  releldm2  7989  opiota  8005  fnmpo  8015  frxp  8069  frxp2  8087  soseq  8102  cnvimadfsn  8115  mpoxneldm  8155  dftpos4  8188  frrlem9  8237  dfrecs3  8305  tfrlem7  8315  ondif1  8429  oarec  8490  oeeu  8532  brinxper  8666  0er  8675  eroveu  8752  erovlem  8753  elixpconst  8846  domen  8901  brsdom  8914  brdom2  8922  reuen1  8966  sbthlem10  9027  brsdom2  9032  xpf1o  9070  unfi  9098  sbthfilem  9125  onfin2  9144  0sdom1domALT  9150  modom  9154  marypha2lem3  9343  wemapsolem  9458  elom3  9560  dfom5  9562  brttrcl2  9626  ttrcltr  9628  ttrclse  9639  trcl  9640  epfrs  9643  frind  9665  rankf  9709  scottexs  9802  scott0s  9803  cplem1  9804  hta  9812  djuexb  9824  pm54.43lem  9915  alephsuc2  9993  iscard3  10006  aceq0  10031  aceq3lem  10033  dfac3  10034  dfac5lem2  10037  dfac5  10042  dfac7  10046  dfac12a  10062  kmlem12  10075  kmlem14  10077  kmlem15  10078  infmap2  10130  ackbij2  10155  dfacfin7  10312  ituniiun  10335  zorng  10417  brdom7disj  10444  entri2  10471  alephreg  10496  fpwwe2lem11  10555  fpwwe2lem12  10556  pwfseqlem1  10572  grutsk  10736  axgroth4  10746  grothprim  10748  grothtsk  10749  elni2  10791  ltsopi  10802  genpass  10923  psslinpr  10945  ltexprlem4  10953  ltresr  11054  infm3  12106  elnnz  12525  dfz2  12534  2rexuz  12841  nnwos  12856  eluz2b1  12860  qexALT  12905  elxr  13058  dflt2  13090  xrsupss  13252  xrinfmss  13253  elixx1  13298  elioo2  13330  dfrp2  13338  elioopnf  13387  elicopnf  13389  elfz1  13457  fznn  13537  fzp1nel  13556  fznn0  13564  preduz  13595  prinfzo0  13644  injresinj  13737  nn0opthlem1  14221  faclbnd4lem1  14246  hashfxnn0  14290  hashprdifel  14351  hashgt23el  14377  hashfun  14390  hashf1  14410  fz1isolem  14414  f1oun2prg  14870  brtrclfv  14955  shftdm  15024  rediv  15084  imdiv  15091  rexanre  15300  caubnd  15312  climreu  15509  prodmo  15892  dvdslelem  16269  3dvdsdec  16292  3dvds2dec  16293  bitsval  16384  smueqlem  16450  algcvgblem  16537  lcmfunsnlem2  16600  isprm2  16642  isprm3  16643  isprm4  16644  pythagtriplem2  16779  elgz  16893  hashbc0  16967  0ram  16982  isstruct  17113  issect  17711  isfull2  17871  isfth2  17875  fucinv  17934  eldmcoa  18023  isdrs  18258  submacs  18786  isnsg4  19133  isgim  19228  gaorb  19273  oppgid  19322  oppgsubm  19328  oppgcntz  19330  ispgp  19558  efgsdm  19696  efgcpbllema  19720  iscyg2  19848  isomnd  20089  omndmul2  20099  isrng  20126  isring  20209  isirred2  20392  opprirred  20393  isrnghm  20412  dfrhm2  20445  isnzr2  20486  opprsubrng  20527  opprsubrg  20561  isdomn3  20683  drngid2  20720  issdrg  20756  islmod  20850  lss1d  20949  islmhm  21014  islmim  21049  lbsextlem2  21149  lidlnz  21232  dfprm2  21463  isphl  21618  elocv  21658  iunocv  21671  isobs  21710  islinds  21799  1mavmul  22523  toprntopon  22900  isbasis3g  22924  fctop  22979  cctop  22981  isclo2  23063  restsn  23145  lmbr  23233  ist0-3  23320  2ndcdisj  23431  1stccnp  23437  islocfin  23492  1stckgenlem  23528  txbas  23542  ptbasin  23552  tx2cn  23585  fbfinnfr  23816  fbasrn  23859  filuni  23860  ufinffr  23904  fin1aufil  23907  rnelfmlem  23927  flimrest  23958  alexsubALTlem3  24024  alexsubALTlem4  24025  tgphaus  24092  istlm  24160  iscusp2  24276  metuel2  24540  isngp2  24572  isnlm  24650  isphtpc  24971  phtpcer  24972  om1elbas  25009  isclm  25041  iscvsp  25105  iscph  25147  iscau3  25255  minveclem3b  25405  elovolm  25452  ioombl1lem4  25538  dyaddisj  25573  vitali  25590  itg1climres  25691  itg2seq  25719  itg2monolem1  25727  itg2mono  25730  limcrcl  25851  lhop1  25991  itgsubst  26026  mdegleb  26039  isuc1p  26116  ismon1p  26118  plydivex  26274  ellogdm  26616  1cubr  26819  atandm2  26854  birthdaylem3  26930  dmarea  26934  dchrelbas2  27214  dchrelbas4  27220  elno3  27633  nosgnn0  27636  nosepon  27643  nocvxminlem  27760  cutcuts  27787  cutbday  27790  dmcuts  27797  cutsf  27798  ltsrec  27807  made0  27869  addsprop  27982  negsproplem2  28035  negsprop  28041  mulsprop  28136  precsexlem10  28222  elzs2  28405  elnnzs  28407  bdayfinbndlem1  28473  recut  28500  axcontlem7  29053  nb3grpr  29465  nb3grpr2  29466  upgrwlkcompim  29726  wlkson  29738  wlkonprop  29740  wksonproplem  29786  ispth  29804  wwlknon  29940  wwlksnextinj  29982  wspthsnwspthsnon  29999  elwspths2spth  30053  rusgrnumwwlkl1  30054  clwwlkccatlem  30074  erclwwlkref  30105  frgr3v  30360  nmoubi  30858  nmobndseqi  30865  nmobndseqiALT  30866  minvecolem1  30960  isch2  31309  hlimreui  31325  isch3  31327  ocsh  31369  dfch2  31493  spanuni  31630  nonbooli  31737  5oalem7  31746  adjsym  31919  elbdop2  31957  dmadjss  31973  nmopub  31994  nmfnleub  32011  nmop0h  32077  pjssposi  32258  pjordi  32259  cvbr2  32369  cvnbtwn2  32373  mdsl2i  32408  cvmdi  32410  elat2  32426  atom1d  32439  chirredi  32480  cdj3i  32527  or3di  32543  opreu2reu1  32568  mo5f  32573  reuxfrdf  32575  rexunirn  32576  difrab2  32582  rabsspr  32586  rabsstp  32587  tpssg  32622  iuninc  32645  disjorf  32664  disjunsn  32679  rabfmpunirn  32741  aciunf1  32751  funcnv5mpt  32755  eliccelico  32865  elicoelioo  32866  isslmd  33278  islinds5  33442  ismxidl  33537  1arithufdlem4  33622  hasheuni  34245  pwsiga  34290  sigainb  34296  issros  34335  2ndmbfm  34421  omssubaddlem  34459  omssubadd  34460  sitgaddlemb  34508  eulerpartlemgvv  34536  eulerpartlemn  34541  probun  34579  ballotlem2  34649  ballotlemodife  34658  bnj252  34862  bnj253  34863  bnj255  34864  bnj345  34873  bnj133  34886  bnj976  34936  bnj1098  34942  bnj121  35028  bnj130  35032  bnj150  35034  bnj581  35066  bnj607  35074  bnj865  35081  bnj917  35092  bnj934  35093  bnj964  35101  bnj983  35109  bnj996  35114  bnj1021  35124  bnj1033  35127  bnj1047  35131  bnj1049  35132  bnj1090  35137  bnj1128  35148  bnj1175  35162  bnj1189  35167  bnj1253  35175  bnj1312  35216  exdifsn  35237  fineqvrep  35274  fineqvac  35276  onvf1odlem4  35304  vonf1owev  35306  erdszelem9  35397  erdszelem10  35398  pconnconn  35429  cvmliftiota  35499  fmlaomn0  35588  fmla0disjsuc  35596  fmlasucdisj  35597  dmopab3rexdif  35603  elmthm  35774  antnestALT  35892  nepss  35916  xpab  35924  dfso2  35953  elrn3  35960  elpotr  35977  dfon2lem5  35983  dfon2lem7  35985  dfon2lem8  35986  elwlim  36019  wzel  36020  brtxp2  36077  brpprod3a  36082  eltrans  36087  dfon3  36088  dffix2  36101  dffun10  36110  elfuns  36111  brsingle  36113  brimg  36133  funpartfun  36141  funpartfv  36143  cgrxfr  36253  segletr  36312  outsideoftr  36327  neifg  36569  filnetlem4  36579  df3nandALT1  36597  weiunlem  36661  ttcwf3  36724  bj-consensusALT  36860  bj-df-ifc  36861  bj-exexalal  36887  bj-cbvaew  36954  bj-biexal3  37020  bj-alnnf  37050  bj-nfnnfTEMP  37095  bj-denoteslem  37194  bj-denotesALTV  37195  bj-ralvw  37202  bj-rexvw  37203  bj-rexcom4bv  37205  bj-rexcom4b  37206  bj-sbeq  37224  bj-inrab  37250  bj-rcleqf  37348  bj-dfmpoa  37446  bj-imdirco  37520  topdifinffinlem  37677  topdifinfeq  37680  relowlssretop  37693  relowlpssretop  37694  rdgeqoa  37700  domalom  37734  nlpineqsn  37738  fvineqsneq  37742  wl-ifpimpr  37796  wl-df3xor3  37800  wl-3xorbi  37803  wl-3xorbi2  37804  wl-2xor  37813  wl-2mintru2  37821  wl-dfclab  37924  rabiun  37928  phpreu  37939  fin2solem  37941  matunitlindflem2  37952  ptrest  37954  poimirlem25  37980  poimirlem27  37982  poimirlem30  37985  ismblfin  37996  ovoliunnfl  37997  voliunnfl  37999  volsupnfl  38000  itg2addnclem2  38007  fdc  38080  prdstotbnd  38129  isdrngo1  38291  ispridl  38369  ismaxidl  38375  impor  38416  selconj  38435  tradd  38440  scott0f  38504  r2alan  38586  inxpss3  38655  idinxpssinxp2  38659  idinxpssinxp3  38660  dfrel5  38681  ineleq  38689  ralmo  38695  ralrnmo  38696  ralrmo3  38699  moantr  38707  dfxrn2  38720  inxpxrn  38753  rnxrnres  38757  dfsuccl4  38809  coss1cnvres  38842  1cossres  38854  cocossss  38861  cossssid4  38895  cossssid5  38896  cosscnvssid5  38903  cossid  38905  dfssr2  38914  cnvrefrelcoss2  38952  cosselcnvrefrels2  38953  eqvrelcoss  39036  eqvrelcoss2  39038  dfcoeleqvrel  39041  refrelredund4  39054  cnvepresdmqs  39073  dfcomember  39092  dfdisjALTV  39133  disjimdmqseq  39144  dfeldisj3  39146  dfeldisj4  39147  dfeldisj5  39148  disjres  39179  prter1  39339  islshp  39439  islshpat  39477  lcvbr2  39482  lcvnbtwn2  39487  cvrnbtwn3  39736  isatl  39759  ishlat1  39812  ishlat2  39813  cvrat4  39903  pmapglbx  40229  lhpexle3  40472  dib1dim  41625  diblsmopel  41631  lcfls1lem  41994  prjsperref  43053  prjspeclsp  43059  euabsn2w  43126  rexrabdioph  43240  dford4  43475  onsupuni  43675  dflim6  43710  tfsconcatlem  43782  naddgeoa  43840  ifpdfor2  43906  ifpdfan2  43908  ifpdfor  43910  ifpdfan  43911  ifpnot23b  43927  ifpnot23c  43929  ifpnot23d  43930  ifpim123g  43945  ifpbibib  43955  clss2lem  44056  imaiun1  44096  coiun1  44097  brfvrcld2  44137  iunrelexp0  44147  brtrclfv2  44172  snhesn  44231  dffrege76  44384  frege97  44405  frege98  44406  frege109  44417  frege110  44418  dffrege115  44423  frege131  44439  frege133  44441  ntrneineine1lem  44529  ntrneiel2  44531  ntrneiiso  44536  gneispace3  44578  scotteld  44691  ismnuprim  44739  ismnushort  44746  dfuniv2  44747  pm11.52  44832  pm11.58  44835  pm13.192  44855  impexpdcom  44960  sbc3or  44977  opelopab4  44996  uunT12p1  45244  uunT12p2  45245  uunT12p3  45246  uun2221  45257  uun2221p1  45258  uun2221p2  45259  undif3VD  45326  modelaxreplem3  45425  permaxext  45450  permac8prim  45459  ndisj2  45500  nssrex  45534  rabssf  45567  bothtbothsame  47359  bothfbothsame  47360  aiffbtbat  47368  reuabaiotaiota  47547  2reu8i  47573  2reuimp0  47574  ichn  47928  dfodd2  48124  dfeven5  48154  dfodd7  48155  1nevenALTV  48179  oddprmne2  48203  dfvopnbgr2  48341  isuspgrim0lem  48381  gpg5nbgrvtx03starlem1  48556  gpg5nbgrvtx03starlem2  48557  gpg5nbgrvtx03starlem3  48558  gpg5nbgrvtx13starlem1  48559  gpg5nbgrvtx13starlem2  48560  gpg5nbgrvtx13starlem3  48561  gpg5edgnedg  48618  islindeps2  48971  isldepslvec2  48973  line2xlem  49241  rmotru  49290  reutru  49291  isnrm4  49418  iscnrm4  49441  homf0  49496  fuco2el  49799  isthincd2  49924  thinccic  49958  istermc2  49962  istermc3  49963  dftermc3  50018  setrec1lem3  50176  aacllem  50288