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 223	. 2 ⊢ (𝜓 ↔ 𝜒)
4	1, 3	bitri 275	1 ⊢ (𝜑 ↔ 𝜒)

Syntax hints:   ↔ wb 205

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 206

This theorem is referenced by:  3bitr2i  299  3bitr2ri  300  3bitr4i  303  3bitr4ri  304  biluk  387  biancomi  464  dfbi2  476  imdistan  569  pm5.32  575  bianass  640  mpbiran  707  biadaniALT  819  imor  851  imimorb  949  pm5.6  1000  nbi2  1014  casesifp  1077  3ancoma  1098  3ancomb  1099  3anrev  1101  an3andi  1482  dfnan2  1490  nannan  1493  nanbi  1496  xorcom  1510  xorneg  1520  xorbi12i  1521  norcom  1528  noran  1531  norasslem1  1533  trunortru  1588  trunorfal  1589  cadan  1608  cadcomb  1612  nic-ax  1673  nic-axALT  1674  nf3  1786  nfnbiOLD  1856  19.43  1883  equsv  2004  sbrimvw  2092  sbcom2  2159  sb5  2266  nf5  2277  nf6  2278  sbrim  2299  sb6x  2462  2sb5rf  2470  2sb6rf  2471  sb4b  2473  sb4bOLD  2474  sb5f  2500  sbequ8  2503  sbhb  2523  eu6lem  2571  eu1  2610  elisset  2818  cleqh  2860  clelabOLD  2882  cleqf  2936  sbabel  2939  necon3bii  2994  neor  3034  neorian  3037  r19.26m  3110  r19.26-3  3112  r19.43  3122  r2allem  3136  r19.23t  3235  ralcom4  3266  rexcomOLD  3271  rabid2f  3325  rabid2OLD  3327  moelOLD  3371  eqv  3446  eqvf  3447  isset  3450  ralv  3461  rexv  3462  reuv  3463  rmov  3464  rexcom4b  3466  ceqsex4v  3490  ceqsex8v  3492  ceqsrexv  3590  rexab  3636  ralrab2  3640  rexrab2  3642  reu2  3665  reu3  3667  reueq  3677  2reuswap  3686  2reuswap2  3687  reuind  3693  2reu5lem3  3697  2rmoswap  3701  sbc3an  3791  rmo2  3825  rmoanim  3832  rmoanimALT  3833  dfss2  3912  dfss2OLD  3913  dfss3  3914  dfss3f  3917  ssabral  4001  rabss  4011  ssrabeq  4023  uniiunlem  4025  sspsstri  4043  npss  4051  dfdif3  4055  raldifb  4085  uncom  4093  inass  4159  elsymdifxor  4189  nsspssun  4197  dfss4  4198  dfun2  4199  dfin2  4200  indi  4213  indifdirOLD  4225  difin2  4231  reupick3  4259  eq0f  4280  neq0f  4281  eq0  4283  eq0ALT  4284  dfnf5  4317  rabn0  4325  csbab  4377  vss  4383  disj  4387  disjOLD  4388  disj3  4393  undisj1  4401  undisj2  4402  inundif  4418  undif  4421  absn  4583  rabsssn  4607  exsnrex  4620  euabsn2  4665  euabsn  4666  raldifsni  4734  tppreqb  4744  pwpw0  4752  prssg  4758  ssunsn  4767  preqsn  4798  pwpr  4838  dfuni2  4846  unissb  4879  unissbOLD  4880  elint2  4893  ssint  4902  uniintab  4926  dfiin2g  4969  iunn0  5003  iunxun  5030  iunxiun  5033  iinpw  5042  disjor  5061  disjxiun  5078  dftr2  5200  dftr5OLD  5203  dftr3  5204  dftr4  5205  axrep6  5225  vnex  5247  inuni  5276  eusv2  5328  reusv2lem4  5333  rexxfr  5348  snelpw  5374  sspwb  5378  opthneg  5409  pwssun  5497  dfid3  5503  dffr6  5558  dffr2  5564  dffr2ALT  5565  opthprc  5662  elxp3  5664  xpiundir  5669  elvv  5672  reliun  5738  inxp  5754  raliunxp  5761  cnvuni  5808  dmopab2rex  5839  dm0rn0  5846  dfres3  5908  ssdmres  5926  elidinxp  5963  idinxpres  5966  dfima2  5981  args  6010  dffr3  6017  cotrg  6027  cotrgOLD  6028  cotrgOLDOLD  6029  intasym  6035  asymref  6036  intirr  6038  xpnz  6077  xp11  6093  ssrnres  6096  xpimasn  6103  coiun  6174  coass  6183  cnvso  6206  elsnxp  6209  dfpo2  6214  dffr4  6237  dfse3  6254  frpoind  6260  wfiOLD  6269  dflim2  6337  orddif  6376  dffun2OLDOLD  6470  dffun6  6471  dffun6f  6476  dffun7  6490  dffun9  6492  funfn  6493  svrelfun  6535  mptfnf  6598  dffn2  6632  dffn3  6643  fint  6683  dffn4  6724  dff1o4  6754  brprcneu  6794  brprcneuALT  6795  eqfnfv3  6943  fnreseql  6957  fsn  7039  ftpg  7060  abrexco  7149  imaiun  7150  dff13  7160  isof1oidb  7227  isof1oopb  7228  isocnv2  7234  eloprabga  7414  mpo2eqb  7438  elovmpo  7546  sorpss  7613  abexex  7846  elxp6  7897  elxp7  7898  releldm2  7916  opiota  7931  fnmpo  7941  frxp  7998  cnvimadfsn  8019  mpoxneldm  8059  dftpos4  8092  frrlem9  8141  wfrlem8OLD  8178  wfrfunOLD  8181  dfrecs3  8234  dfrecs3OLD  8235  tfrlem7  8245  ondif1  8362  oarec  8424  oeeu  8465  0er  8566  eroveu  8632  erovlem  8633  elixpconst  8724  domen  8782  brsdom  8796  brdom2  8803  reuen1  8850  sbthlem10  8917  brsdom2  8922  xpf1o  8964  unfi  8993  sbthfilem  9022  onfin2  9052  0sdom1domOLD  9060  modom  9065  unfiOLD  9125  marypha2lem3  9240  wemapsolem  9353  elom3  9450  dfom5  9452  brttrcl2  9516  ttrcltr  9518  ttrclse  9529  trcl  9530  epfrs  9533  frind  9552  rankf  9596  scottexs  9689  scott0s  9690  cplem1  9691  karden  9697  hta  9699  djuexb  9711  pm54.43lem  9802  alephsuc2  9882  iscard3  9895  aceq0  9920  aceq3lem  9922  dfac3  9923  dfac5lem2  9926  dfac5  9930  dfac7  9934  dfac12a  9950  kmlem12  9963  kmlem14  9965  kmlem15  9966  infmap2  10020  ackbij2  10045  dfacfin7  10201  ituniiun  10224  zorng  10306  brdom7disj  10333  entri2  10360  alephreg  10384  fpwwe2lem11  10443  fpwwe2lem12  10444  pwfseqlem1  10460  grutsk  10624  axgroth4  10634  grothprim  10636  grothtsk  10637  elni2  10679  ltsopi  10690  genpass  10811  psslinpr  10833  ltexprlem4  10841  ltresr  10942  1re  11021  infm3  11980  elnnz  12375  dfz2  12384  2rexuz  12686  nnwos  12701  eluz2b1  12705  qexALT  12750  elxr  12898  dflt2  12928  xrsupss  13089  xrinfmss  13090  elixx1  13134  elioo2  13166  dfrp2  13174  elioopnf  13221  elicopnf  13223  elfz1  13290  fznn  13370  fzp1nel  13386  fznn0  13394  preduz  13424  prinfzo0  13472  injresinj  13554  nn0opthlem1  14028  faclbnd4lem1  14053  hashfxnn0  14097  hashprdifel  14158  hashgt23el  14184  hashfun  14197  hashf1  14216  fz1isolem  14220  f1oun2prg  14675  brtrclfv  14758  shftdm  14827  rediv  14887  imdiv  14894  rexanre  15103  caubnd  15115  climreu  15310  prodmo  15691  dvdslelem  16063  3dvdsdec  16086  3dvds2dec  16087  bitsval  16176  smueqlem  16242  algcvgblem  16327  lcmfunsnlem2  16390  isprm2  16432  isprm3  16433  isprm4  16434  pythagtriplem2  16563  elgz  16677  hashbc0  16751  0ram  16766  isstruct  16898  issect  17510  isfull2  17672  isfth2  17676  fucinv  17736  eldmcoa  17825  isdrs  18064  submacs  18510  isnsg4  18840  isgim  18923  gaorb  18958  oppgid  19008  oppgsubm  19014  oppgcntz  19016  ispgp  19242  efgsdm  19381  efgcpbllema  19405  iscyg2  19527  isring  19832  isirred2  19988  opprirred  19989  dfrhm2  20006  drngid2  20052  opprsubrg  20090  issdrg  20108  islmod  20172  lss1d  20270  islmhm  20334  islmim  20369  lbsextlem2  20466  lidlnz  20544  isnzr2  20579  dfprm2  20740  isphl  20878  elocv  20918  iunocv  20931  isobs  20972  islinds  21061  isassa  21108  1mavmul  21742  toprntopon  22119  isbasis3g  22144  fctop  22199  cctop  22201  isclo2  22284  restsn  22366  lmbr  22454  ist0-3  22541  2ndcdisj  22652  1stccnp  22658  islocfin  22713  1stckgenlem  22749  txbas  22763  ptbasin  22773  tx2cn  22806  fbfinnfr  23037  fbasrn  23080  filuni  23081  ufinffr  23125  fin1aufil  23128  rnelfmlem  23148  flimrest  23179  alexsubALTlem3  23245  alexsubALTlem4  23246  tgphaus  23313  istlm  23381  iscusp2  23499  metuel2  23766  isngp2  23798  isnlm  23884  isphtpc  24202  phtpcer  24203  om1elbas  24240  isclm  24272  iscvsp  24336  iscph  24379  iscau3  24487  minveclem3b  24637  elovolm  24684  ioombl1lem4  24770  dyaddisj  24805  vitali  24822  itg1climres  24924  itg2seq  24952  itg2monolem1  24960  itg2mono  24963  limcrcl  25083  lhop1  25223  itgsubst  25258  mdegleb  25274  isuc1p  25350  ismon1p  25352  plydivex  25502  ellogdm  25839  1cubr  26037  atandm2  26072  birthdaylem3  26148  dmarea  26152  dchrelbas2  26430  dchrelbas4  26436  axcontlem7  27383  nb3grpr  27794  nb3grpr2  27795  upgrwlkcompim  28055  wlkson  28069  wlkonprop  28071  wksonproplem  28117  wksonproplemOLD  28118  ispth  28136  wwlknon  28267  wwlksnextinj  28309  wspthsnwspthsnon  28326  elwspths2spth  28377  rusgrnumwwlkl1  28378  clwwlkccatlem  28398  erclwwlkref  28429  frgr3v  28684  nmoubi  29179  nmobndseqi  29186  nmobndseqiALT  29187  minvecolem1  29281  isch2  29630  hlimreui  29646  isch3  29648  ocsh  29690  dfch2  29814  spanuni  29951  nonbooli  30058  5oalem7  30067  adjsym  30240  elbdop2  30278  dmadjss  30294  nmopub  30315  nmfnleub  30332  nmop0h  30398  pjssposi  30579  pjordi  30580  cvbr2  30690  cvnbtwn2  30694  mdsl2i  30729  cvmdi  30731  elat2  30747  atom1d  30760  chirredi  30801  cdj3i  30848  or3di  30855  opreu2reu1  30877  mo5f  30882  reuxfrdf  30884  rexunirn  30885  difrab2  30890  iuninc  30945  disjorf  30963  disjunsn  30978  rabfmpunirn  31035  aciunf1  31045  funcnv5mpt  31050  eliccelico  31143  elicoelioo  31144  isomnd  31372  omndmul2  31383  isslmd  31500  islinds5  31608  ismxidl  31679  hasheuni  32098  pwsiga  32143  sigainb  32149  issros  32188  2ndmbfm  32273  omssubaddlem  32311  omssubadd  32312  sitgaddlemb  32360  eulerpartlemgvv  32388  eulerpartlemn  32393  probun  32431  ballotlem2  32500  ballotlemodife  32509  bnj252  32727  bnj253  32728  bnj255  32729  bnj345  32738  bnj133  32751  bnj976  32802  bnj1098  32808  bnj121  32895  bnj130  32899  bnj150  32901  bnj581  32933  bnj607  32941  bnj865  32948  bnj917  32959  bnj934  32960  bnj964  32968  bnj983  32976  bnj996  32981  bnj1021  32991  bnj1033  32994  bnj1047  32998  bnj1049  32999  bnj1090  33004  bnj1128  33015  bnj1175  33029  bnj1189  33034  bnj1253  33042  bnj1312  33083  exdifsn  33098  fineqvrep  33109  fineqvac  33111  erdszelem9  33206  erdszelem10  33207  pconnconn  33238  cvmliftiota  33308  fmlaomn0  33397  fmla0disjsuc  33405  fmlasucdisj  33406  dmopab3rexdif  33412  elmthm  33583  nepss  33707  xpab  33722  dfso2  33767  elrn3  33774  imaindm  33798  elpotr  33802  dfon2lem5  33808  dfon2lem7  33810  dfon2lem8  33811  frxp2  33836  poxp3  33841  soseq  33848  elwlim  33862  wzel  33863  elno3  33903  nosgnn0  33906  nosepon  33913  nocvxminlem  34017  scutcut  34040  scutbday  34043  dmscut  34050  scutf  34051  sltrec  34059  made0  34102  brtxp2  34228  brpprod3a  34233  eltrans  34238  dfon3  34239  dffix2  34252  dffun10  34261  elfuns  34262  brsingle  34264  brimg  34284  funpartfun  34290  funpartfv  34292  cgrxfr  34402  segletr  34461  outsideoftr  34476  neifg  34605  filnetlem4  34615  df3nandALT1  34633  bj-consensusALT  34805  bj-df-ifc  34806  bj-biexal3  34934  bj-nfnnfTEMP  34985  bj-denoteslem  35099  bj-denotes  35100  bj-ralvw  35108  bj-rexvw  35109  bj-rexcom4bv  35111  bj-rexcom4b  35112  bj-sbeq  35130  bj-inrab  35159  bj-rcleqf  35259  bj-dfmpoa  35333  bj-imdirco  35405  topdifinffinlem  35562  topdifinfeq  35565  relowlssretop  35578  relowlpssretop  35579  rdgeqoa  35585  domalom  35619  nlpineqsn  35623  fvineqsneq  35627  wl-ifpimpr  35681  wl-df3xor3  35685  wl-3xorbi  35688  wl-3xorbi2  35689  wl-2xor  35698  wl-2mintru2  35706  wl-dfclab  35791  rabiun  35794  phpreu  35805  fin2solem  35807  matunitlindflem2  35818  ptrest  35820  poimirlem25  35846  poimirlem27  35848  poimirlem30  35851  ismblfin  35862  ovoliunnfl  35863  voliunnfl  35865  volsupnfl  35866  itg2addnclem2  35873  fdc  35947  prdstotbnd  35996  isdrngo1  36158  ispridl  36236  ismaxidl  36242  impor  36283  selconj  36302  tradd  36307  scott0f  36371  inxpss3  36491  idinxpssinxp2  36495  idinxpssinxp3  36496  dfrel5  36523  ineleq  36528  moantr  36536  dfxrn2  36548  inxpxrn  36563  rnxrnres  36567  1cossres  36594  cocossss  36601  cossssid4  36630  cossssid5  36631  cosscnvssid5  36638  cossid  36640  dfssr2  36659  cnvrefrelcoss2  36693  cosselcnvrefrels2  36694  eqvrelcoss  36772  eqvrelcoss2  36774  dfcoeleqvrel  36777  refrelredund4  36790  cnvepresdmqs  36807  dfmember  36826  dfdisjALTV  36866  dfeldisj3  36872  dfeldisj4  36873  dfeldisj5  36874  prter1  36935  islshp  37035  islshpat  37073  lcvbr2  37078  lcvnbtwn2  37083  cvrnbtwn3  37332  isatl  37355  ishlat1  37408  ishlat2  37409  cvrat4  37499  pmapglbx  37825  lhpexle3  38068  dib1dim  39221  diblsmopel  39227  lcfls1lem  39590  prjsperref  40482  prjspeclsp  40488  rexrabdioph  40653  dford4  40889  isdomn3  41067  ifpdfor2  41106  ifpdfan2  41108  ifpdfor  41110  ifpdfan  41111  ifpnot23b  41127  ifpnot23c  41129  ifpnot23d  41130  ifpim123g  41145  ifpbibib  41155  clss2lem  41257  imaiun1  41297  coiun1  41298  brfvrcld2  41338  iunrelexp0  41348  brtrclfv2  41373  snhesn  41432  dffrege76  41585  frege97  41606  frege98  41607  frege109  41618  frege110  41619  dffrege115  41624  frege131  41640  frege133  41642  ntrneineine1lem  41732  ntrneiel2  41734  ntrneiiso  41739  gneispace3  41781  scotteld  41902  ismnuprim  41950  ismnushort  41957  dfuniv2  41958  pm11.52  42043  pm11.58  42046  pm13.192  42066  impexpdcom  42173  sbc3or  42190  opelopab4  42209  uunT12p1  42458  uunT12p2  42459  uunT12p3  42460  uun2221  42471  uun2221p1  42472  uun2221p2  42473  undif3VD  42540  ndisj2  42637  nssrex  42674  rabssf  42706  bothtbothsame  44452  bothfbothsame  44453  aiffbtbat  44461  reuabaiotaiota  44637  2reu8i  44663  2reuimp0  44664  ichn  44966  dfodd2  45146  dfeven5  45176  dfodd7  45177  1nevenALTV  45201  oddprmne2  45225  isrng  45492  isrnghm  45508  islindeps2  45882  isldepslvec2  45884  line2xlem  46157  rextru  46207  rmotru  46208  reutru  46209  isnrm4  46282  iscnrm4  46306  isthincd2  46377  thinccic  46400  setrec1lem3  46453  aacllem  46563