Theorem bitr4i 277

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 274	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  298  3bitr2ri  299  3bitr4i  302  3bitr4ri  303  biluk  386  biancomi  462  dfbi2  474  imdistan  567  pm5.32  573  bianass  638  mpbiran  705  biadaniALT  817  imor  849  imimorb  947  pm5.6  998  nbi2  1012  casesifp  1075  3ancoma  1096  3ancomb  1097  3anrev  1099  an3andi  1480  dfnan2  1488  nannan  1491  nanbi  1494  xorcom  1508  xorneg  1518  xorbi12i  1519  norcom  1526  noran  1530  norasslem1  1534  norassOLD  1538  trunortru  1590  trunorfal  1592  cadan  1614  cadcomb  1618  nic-ax  1679  nic-axALT  1680  nf3  1792  nfnbiOLD  1861  19.43  1888  equsv  2009  sbrimvw  2097  sbcom2  2164  sb5  2271  nf5  2282  nf6  2283  sbrim  2304  sb6x  2465  2sb5rf  2473  2sb6rf  2474  sb4b  2476  sb4bOLD  2477  sb5f  2503  sbequ8  2506  sbhb  2526  eu6lem  2574  eu1  2613  elisset  2821  cleqh  2863  clelabOLD  2885  cleqf  2939  sbabel  2942  necon3bii  2997  neor  3037  neorian  3040  r19.26-3  3098  r19.26m  3099  r2allem  3125  ralcom4  3163  r19.23t  3243  r19.43  3279  rexcom  3283  rabid2f  3311  rabid2OLD  3313  moelOLD  3357  eqv  3439  eqvf  3440  isset  3443  ralv  3454  rexv  3455  reuv  3456  rmov  3457  rexcom4b  3459  ceqsex4v  3483  ceqsex8v  3485  ceqsrexv  3586  rexab  3632  ralrab2  3637  rexrab2  3640  reu2  3663  reu3  3665  reueq  3675  2reuswap  3684  2reuswap2  3685  reuind  3691  2reu5lem3  3695  2rmoswap  3699  sbc3an  3790  rmo2  3824  rmoanim  3831  rmoanimALT  3832  dfss2  3911  dfss2OLD  3912  dfss3  3913  dfss3f  3916  ssabral  4000  rabss  4009  ssrabeq  4021  uniiunlem  4023  sspsstri  4041  npss  4049  dfdif3  4053  raldifb  4083  uncom  4091  inass  4158  elsymdifxor  4188  nsspssun  4196  dfss4  4197  dfun2  4198  dfin2  4199  indi  4212  indifdirOLD  4224  difin2  4230  reupick3  4258  eq0f  4279  neq0f  4280  eq0  4282  eq0ALT  4283  dfnf5  4316  rabn0  4324  csbab  4376  vss  4382  disj  4386  disjOLD  4387  disj3  4392  undisj1  4400  undisj2  4401  inundif  4417  undif  4420  absn  4584  rabsssn  4608  exsnrex  4621  euabsn2  4666  euabsn  4667  raldifsni  4733  tppreqb  4743  pwpw0  4751  prssg  4757  ssunsn  4766  preqsn  4797  pwpr  4838  dfuni2  4846  unissb  4878  elint2  4891  ssint  4900  uniintab  4924  dfiin2g  4966  iunn0  5000  iunxun  5027  iunxiun  5030  iinpw  5039  disjor  5058  disjxiun  5075  dftr2  5197  dftr5  5198  dftr3  5199  dftr4  5200  axrep6  5220  vnex  5241  inuni  5270  eusv2  5322  reusv2lem4  5327  rexxfr  5342  snelpw  5363  sspwb  5367  opthneg  5398  pwssun  5484  dfid3  5491  dffr6  5546  dffr2  5552  dffr2ALT  5553  opthprc  5650  elxp3  5652  xpiundir  5657  elvv  5660  reliun  5723  inxp  5738  raliunxp  5745  cnvuni  5792  dmopab2rex  5823  dm0rn0  5831  dfres3  5893  ssdmres  5911  elidinxp  5948  idinxpres  5951  dfima2  5968  args  5997  dffr3  6004  cotrg  6013  intasym  6017  asymref  6018  intirr  6020  xpnz  6059  xp11  6075  ssrnres  6078  xpimasn  6085  coiun  6157  coass  6166  cnvso  6188  elsnxp  6191  dfpo2  6196  dffr4  6219  dfse3  6236  frpoind  6242  wfiOLD  6251  dflim2  6319  orddif  6356  dffun2  6440  dffun6f  6444  dffun7  6457  dffun9  6459  funfn  6460  svrelfun  6502  mptfnf  6564  dffn2  6598  dffn3  6609  fint  6649  dffn4  6690  dff1o4  6720  brprcneu  6759  fvprc  6760  eqfnfv3  6905  fnreseql  6919  fsn  7001  ftpg  7022  abrexco  7111  imaiun  7112  dff13  7122  isof1oidb  7188  isof1oopb  7189  isocnv2  7195  eloprabga  7373  mpo2eqb  7397  elovmpo  7505  sorpss  7572  abexex  7800  elxp6  7851  elxp7  7852  releldm2  7870  opiota  7885  fnmpo  7895  frxp  7951  cnvimadfsn  7972  mpoxneldm  8012  dftpos4  8045  frrlem9  8094  wfrlem8OLD  8131  wfrfunOLD  8134  dfrecs3  8187  dfrecs3OLD  8188  tfrlem7  8198  ondif1  8307  oarec  8369  oeeu  8410  0er  8509  eroveu  8575  erovlem  8576  elixpconst  8667  domen  8722  brsdom  8734  brdom2  8741  reuen1  8785  sbthlem10  8848  brsdom2  8853  xpf1o  8891  unfi  8920  sbthfilem  8949  onfin2  8977  0sdom1dom  8982  modom  8985  unfiOLD  9042  marypha2lem3  9157  wemapsolem  9270  elom3  9367  dfom5  9369  brttrcl2  9433  ttrcltr  9435  ttrclse  9446  trcl  9469  epfrs  9472  frind  9492  rankf  9536  scottexs  9629  scott0s  9630  cplem1  9631  karden  9637  hta  9639  djuexb  9651  pm54.43lem  9742  alephsuc2  9820  iscard3  9833  aceq0  9858  aceq3lem  9860  dfac3  9861  dfac5lem2  9864  dfac5  9868  dfac7  9872  dfac12a  9888  kmlem12  9901  kmlem14  9903  kmlem15  9904  infmap2  9958  ackbij2  9983  dfacfin7  10139  ituniiun  10162  zorng  10244  brdom7disj  10271  entri2  10298  alephreg  10322  fpwwe2lem11  10381  fpwwe2lem12  10382  pwfseqlem1  10398  grutsk  10562  axgroth4  10572  grothprim  10574  grothtsk  10575  elni2  10617  ltsopi  10628  genpass  10749  psslinpr  10771  ltexprlem4  10779  ltresr  10880  1re  10959  infm3  11917  elnnz  12312  dfz2  12321  2rexuz  12622  nnwos  12637  eluz2b1  12641  qexALT  12686  elxr  12834  dflt2  12864  xrsupss  13025  xrinfmss  13026  elixx1  13070  elioo2  13102  dfrp2  13110  elioopnf  13157  elicopnf  13159  elfz1  13226  fznn  13306  fzp1nel  13322  fznn0  13330  preduz  13360  prinfzo0  13407  injresinj  13489  nn0opthlem1  13963  faclbnd4lem1  13988  hashfxnn0  14032  hashprdifel  14094  hashgt23el  14120  hashfun  14133  hashf1  14152  fz1isolem  14156  f1oun2prg  14611  brtrclfv  14694  shftdm  14763  rediv  14823  imdiv  14830  rexanre  15039  caubnd  15051  climreu  15246  prodmo  15627  dvdslelem  15999  3dvdsdec  16022  3dvds2dec  16023  bitsval  16112  smueqlem  16178  algcvgblem  16263  lcmfunsnlem2  16326  isprm2  16368  isprm3  16369  isprm4  16370  pythagtriplem2  16499  elgz  16613  hashbc0  16687  0ram  16702  isstruct  16834  issect  17446  isfull2  17608  isfth2  17612  fucinv  17672  eldmcoa  17761  isdrs  18000  submacs  18446  isnsg4  18776  isgim  18859  gaorb  18894  oppgid  18944  oppgsubm  18950  oppgcntz  18952  ispgp  19178  efgsdm  19317  efgcpbllema  19341  iscyg2  19463  isring  19768  isirred2  19924  opprirred  19925  dfrhm2  19942  drngid2  19988  opprsubrg  20026  issdrg  20044  islmod  20108  lss1d  20206  islmhm  20270  islmim  20305  lbsextlem2  20402  lidlnz  20480  isnzr2  20515  dfprm2  20676  isphl  20814  elocv  20854  iunocv  20867  isobs  20908  islinds  20997  isassa  21044  1mavmul  21678  toprntopon  22055  isbasis3g  22080  fctop  22135  cctop  22137  isclo2  22220  restsn  22302  lmbr  22390  ist0-3  22477  2ndcdisj  22588  1stccnp  22594  islocfin  22649  1stckgenlem  22685  txbas  22699  ptbasin  22709  tx2cn  22742  fbfinnfr  22973  fbasrn  23016  filuni  23017  ufinffr  23061  fin1aufil  23064  rnelfmlem  23084  flimrest  23115  alexsubALTlem3  23181  alexsubALTlem4  23182  tgphaus  23249  istlm  23317  iscusp2  23435  metuel2  23702  isngp2  23734  isnlm  23820  isphtpc  24138  phtpcer  24139  om1elbas  24176  isclm  24208  iscvsp  24272  iscph  24315  iscau3  24423  minveclem3b  24573  elovolm  24620  ioombl1lem4  24706  dyaddisj  24741  vitali  24758  itg1climres  24860  itg2seq  24888  itg2monolem1  24896  itg2mono  24899  limcrcl  25019  lhop1  25159  itgsubst  25194  mdegleb  25210  isuc1p  25286  ismon1p  25288  plydivex  25438  ellogdm  25775  1cubr  25973  atandm2  26008  birthdaylem3  26084  dmarea  26088  dchrelbas2  26366  dchrelbas4  26372  axcontlem7  27319  nb3grpr  27730  nb3grpr2  27731  upgrwlkcompim  27990  wlkson  28004  wlkonprop  28006  wksonproplem  28052  ispth  28070  wwlknon  28201  wwlksnextinj  28243  wspthsnwspthsnon  28260  elwspths2spth  28311  rusgrnumwwlkl1  28312  clwwlkccatlem  28332  erclwwlkref  28363  frgr3v  28618  nmoubi  29113  nmobndseqi  29120  nmobndseqiALT  29121  minvecolem1  29215  isch2  29564  hlimreui  29580  isch3  29582  ocsh  29624  dfch2  29748  spanuni  29885  nonbooli  29992  5oalem7  30001  adjsym  30174  elbdop2  30212  dmadjss  30228  nmopub  30249  nmfnleub  30266  nmop0h  30332  pjssposi  30513  pjordi  30514  cvbr2  30624  cvnbtwn2  30628  mdsl2i  30663  cvmdi  30665  elat2  30681  atom1d  30694  chirredi  30735  cdj3i  30782  or3di  30789  opreu2reu1  30811  mo5f  30816  reuxfrdf  30818  rexunirn  30819  difrab2  30824  iuninc  30879  disjorf  30897  disjunsn  30912  rabfmpunirn  30969  aciunf1  30979  funcnv5mpt  30984  eliccelico  31077  elicoelioo  31078  isomnd  31306  omndmul2  31317  isslmd  31434  islinds5  31542  ismxidl  31613  hasheuni  32032  pwsiga  32077  sigainb  32083  issros  32122  2ndmbfm  32207  omssubaddlem  32245  omssubadd  32246  sitgaddlemb  32294  eulerpartlemgvv  32322  eulerpartlemn  32327  probun  32365  ballotlem2  32434  ballotlemodife  32443  bnj252  32661  bnj253  32662  bnj255  32663  bnj345  32672  bnj133  32685  bnj976  32736  bnj1098  32742  bnj121  32829  bnj130  32833  bnj150  32835  bnj581  32867  bnj607  32875  bnj865  32882  bnj917  32893  bnj934  32894  bnj964  32902  bnj983  32910  bnj996  32915  bnj1021  32925  bnj1033  32928  bnj1047  32932  bnj1049  32933  bnj1090  32938  bnj1128  32949  bnj1175  32963  bnj1189  32968  bnj1253  32976  bnj1312  33017  exdifsn  33032  fineqvrep  33043  fineqvac  33045  erdszelem9  33140  erdszelem10  33141  pconnconn  33172  cvmliftiota  33242  fmlaomn0  33331  fmla0disjsuc  33339  fmlasucdisj  33340  dmopab3rexdif  33346  elmthm  33517  nepss  33641  xpab  33656  dfso2  33701  elrn3  33708  imaindm  33732  elpotr  33736  dfon2lem5  33742  dfon2lem7  33744  dfon2lem8  33745  frxp2  33770  poxp3  33775  soseq  33782  elwlim  33796  wzel  33797  elno3  33837  nosgnn0  33840  nosepon  33847  nocvxminlem  33951  scutcut  33974  scutbday  33977  dmscut  33984  scutf  33985  sltrec  33993  made0  34036  brtxp2  34162  brpprod3a  34167  eltrans  34172  dfon3  34173  dffix2  34186  dffun10  34195  elfuns  34196  brsingle  34198  brimg  34218  funpartfun  34224  funpartfv  34226  cgrxfr  34336  segletr  34395  outsideoftr  34410  neifg  34539  filnetlem4  34549  df3nandALT1  34567  bj-consensusALT  34739  bj-df-ifc  34740  bj-biexal3  34868  bj-nfnnfTEMP  34919  bj-denoteslem  35034  bj-denotes  35035  bj-ralvw  35043  bj-rexvw  35044  bj-rexcom4bv  35046  bj-rexcom4b  35047  bj-sbeq  35065  bj-inrab  35094  bj-rcleqf  35194  bj-dfmpoa  35268  bj-imdirco  35340  topdifinffinlem  35497  topdifinfeq  35500  relowlssretop  35513  relowlpssretop  35514  rdgeqoa  35520  domalom  35554  nlpineqsn  35558  fvineqsneq  35562  wl-ifpimpr  35616  wl-df3xor3  35620  wl-3xorbi  35623  wl-3xorbi2  35624  wl-2xor  35633  wl-2mintru2  35641  wl-dfclab  35726  rabiun  35729  phpreu  35740  fin2solem  35742  matunitlindflem2  35753  ptrest  35755  poimirlem25  35781  poimirlem27  35783  poimirlem30  35786  ismblfin  35797  ovoliunnfl  35798  voliunnfl  35800  volsupnfl  35801  itg2addnclem2  35808  fdc  35882  prdstotbnd  35931  isdrngo1  36093  ispridl  36171  ismaxidl  36177  impor  36218  selconj  36237  tradd  36242  scott0f  36306  inxpss3  36428  idinxpssinxp2  36432  idinxpssinxp3  36433  dfrel5  36460  ineleq  36465  moantr  36473  dfxrn2  36485  inxpxrn  36500  rnxrnres  36504  1cossres  36531  cocossss  36538  cossssid4  36567  cossssid5  36568  cosscnvssid5  36575  cossid  36577  dfssr2  36596  cnvrefrelcoss2  36630  cosselcnvrefrels2  36631  eqvrelcoss  36709  eqvrelcoss2  36711  dfcoeleqvrel  36714  refrelredund4  36727  cnvepresdmqs  36744  dfmember  36763  dfdisjALTV  36803  dfeldisj3  36809  dfeldisj4  36810  dfeldisj5  36811  prter1  36872  islshp  36972  islshpat  37010  lcvbr2  37015  lcvnbtwn2  37020  cvrnbtwn3  37269  isatl  37292  ishlat1  37345  ishlat2  37346  cvrat4  37436  pmapglbx  37762  lhpexle3  38005  dib1dim  39158  diblsmopel  39164  lcfls1lem  39527  prjsperref  40425  prjspeclsp  40431  rexrabdioph  40596  dford4  40831  isdomn3  41009  ifpdfor2  41030  ifpdfan2  41032  ifpdfor  41034  ifpdfan  41035  ifpnot23b  41051  ifpnot23c  41053  ifpnot23d  41054  ifpim123g  41069  ifpbibib  41079  clss2lem  41172  imaiun1  41212  coiun1  41213  brfvrcld2  41253  iunrelexp0  41263  brtrclfv2  41288  snhesn  41347  dffrege76  41500  frege97  41521  frege98  41522  frege109  41533  frege110  41534  dffrege115  41539  frege131  41555  frege133  41557  ntrneineine1lem  41647  ntrneiel2  41649  ntrneiiso  41654  gneispace3  41696  scotteld  41817  ismnuprim  41865  ismnushort  41872  dfuniv2  41873  pm11.52  41958  pm11.58  41961  pm13.192  41981  impexpdcom  42088  sbc3or  42105  opelopab4  42124  uunT12p1  42373  uunT12p2  42374  uunT12p3  42375  uun2221  42386  uun2221p1  42387  uun2221p2  42388  undif3VD  42455  ndisj2  42552  nssrex  42589  rabssf  42621  bothtbothsame  44345  bothfbothsame  44346  aiffbtbat  44354  reuabaiotaiota  44530  2reu8i  44556  2reuimp0  44557  ichn  44860  dfodd2  45040  dfeven5  45070  dfodd7  45071  1nevenALTV  45095  oddprmne2  45119  isrng  45386  isrnghm  45402  islindeps2  45776  isldepslvec2  45778  line2xlem  46051  rextru  46101  rmotru  46102  reutru  46103  isnrm4  46176  iscnrm4  46200  isthincd2  46271  thinccic  46294  setrec1lem3  46347  aacllem  46457