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  299  3bitr2ri  300  3bitr4i  303  3bitr4ri  304  biluk  387  biancomi  463  dfbi2  475  imdistan  568  pm5.32  574  bianass  639  mpbiran  706  biadaniALT  818  imor  850  imimorb  948  pm5.6  999  nbi2  1013  casesifp  1076  3ancoma  1097  3ancomb  1098  3anrev  1100  an3andi  1481  dfnan2  1489  nannan  1492  nanbi  1495  xorcom  1509  xorneg  1519  xorbi12i  1520  norcom  1527  noran  1531  norasslem1  1535  norassOLD  1539  trunortru  1591  trunorfal  1593  cadan  1615  cadcomb  1619  nic-ax  1680  nic-axALT  1681  nf3  1793  nfnbiOLD  1862  19.43  1889  equsv  2010  sbrimvw  2098  sbcom2  2165  sb5  2272  nf5  2283  nf6  2284  sbrim  2305  sb6x  2466  2sb5rf  2474  2sb6rf  2475  sb4b  2477  sb4bOLD  2478  sb5f  2504  sbequ8  2507  sbhb  2527  eu6lem  2575  eu1  2614  elisset  2822  cleqh  2864  clelabOLD  2886  cleqf  2940  sbabel  2943  necon3bii  2998  neor  3038  neorian  3041  r19.26-3  3099  r19.26m  3100  r2allem  3126  ralcom4  3164  r19.23t  3244  r19.43  3280  rexcom  3284  rabid2f  3312  rabid2OLD  3314  moelOLD  3358  eqv  3440  eqvf  3441  isset  3444  ralv  3455  rexv  3456  reuv  3457  rmov  3458  rexcom4b  3460  ceqsex4v  3484  ceqsex8v  3486  ceqsrexv  3587  rexab  3633  ralrab2  3638  rexrab2  3641  reu2  3664  reu3  3666  reueq  3676  2reuswap  3685  2reuswap2  3686  reuind  3692  2reu5lem3  3696  2rmoswap  3700  sbc3an  3791  rmo2  3825  rmoanim  3832  rmoanimALT  3833  dfss2  3912  dfss2OLD  3913  dfss3  3914  dfss3f  3917  ssabral  4001  rabss  4010  ssrabeq  4022  uniiunlem  4024  sspsstri  4042  npss  4050  dfdif3  4054  raldifb  4084  uncom  4092  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  4585  rabsssn  4609  exsnrex  4622  euabsn2  4667  euabsn  4668  raldifsni  4734  tppreqb  4744  pwpw0  4752  prssg  4758  ssunsn  4767  preqsn  4798  pwpr  4839  dfuni2  4847  unissb  4879  elint2  4892  ssint  4901  uniintab  4925  dfiin2g  4967  iunn0  5001  iunxun  5028  iunxiun  5031  iinpw  5040  disjor  5059  disjxiun  5076  dftr2  5198  dftr5  5199  dftr3  5200  dftr4  5201  axrep6  5221  vnex  5242  inuni  5271  eusv2  5323  reusv2lem4  5328  rexxfr  5343  snelpw  5365  sspwb  5369  opthneg  5400  pwssun  5486  dfid3  5493  dffr6  5548  dffr2  5554  dffr2ALT  5555  opthprc  5652  elxp3  5654  xpiundir  5659  elvv  5662  reliun  5725  inxp  5740  raliunxp  5747  cnvuni  5794  dmopab2rex  5825  dm0rn0  5833  dfres3  5895  ssdmres  5913  elidinxp  5950  idinxpres  5953  dfima2  5970  args  5999  dffr3  6006  cotrg  6015  intasym  6019  asymref  6020  intirr  6022  xpnz  6061  xp11  6077  ssrnres  6080  xpimasn  6087  coiun  6159  coass  6168  cnvso  6190  elsnxp  6193  dfpo2  6198  dffr4  6221  dfse3  6238  frpoind  6244  wfiOLD  6253  dflim2  6321  orddif  6358  dffun2  6442  dffun6f  6446  dffun7  6459  dffun9  6461  funfn  6462  svrelfun  6504  mptfnf  6566  dffn2  6600  dffn3  6611  fint  6651  dffn4  6692  dff1o4  6722  brprcneu  6761  brprcneuALT  6762  eqfnfv3  6908  fnreseql  6922  fsn  7004  ftpg  7025  abrexco  7114  imaiun  7115  dff13  7125  isof1oidb  7192  isof1oopb  7193  isocnv2  7199  eloprabga  7377  mpo2eqb  7401  elovmpo  7509  sorpss  7576  abexex  7808  elxp6  7859  elxp7  7860  releldm2  7878  opiota  7893  fnmpo  7903  frxp  7959  cnvimadfsn  7980  mpoxneldm  8020  dftpos4  8053  frrlem9  8102  wfrlem8OLD  8139  wfrfunOLD  8142  dfrecs3  8195  dfrecs3OLD  8196  tfrlem7  8206  ondif1  8323  oarec  8385  oeeu  8426  0er  8527  eroveu  8593  erovlem  8594  elixpconst  8685  domen  8743  brsdom  8755  brdom2  8762  reuen1  8807  sbthlem10  8870  brsdom2  8875  xpf1o  8917  unfi  8946  sbthfilem  8975  onfin2  9003  0sdom1dom  9008  modom  9011  unfiOLD  9069  marypha2lem3  9184  wemapsolem  9297  elom3  9394  dfom5  9396  brttrcl2  9460  ttrcltr  9462  ttrclse  9473  trcl  9496  epfrs  9499  frind  9519  rankf  9563  scottexs  9656  scott0s  9657  cplem1  9658  karden  9664  hta  9666  djuexb  9678  pm54.43lem  9769  alephsuc2  9847  iscard3  9860  aceq0  9885  aceq3lem  9887  dfac3  9888  dfac5lem2  9891  dfac5  9895  dfac7  9899  dfac12a  9915  kmlem12  9928  kmlem14  9930  kmlem15  9931  infmap2  9985  ackbij2  10010  dfacfin7  10166  ituniiun  10189  zorng  10271  brdom7disj  10298  entri2  10325  alephreg  10349  fpwwe2lem11  10408  fpwwe2lem12  10409  pwfseqlem1  10425  grutsk  10589  axgroth4  10599  grothprim  10601  grothtsk  10602  elni2  10644  ltsopi  10655  genpass  10776  psslinpr  10798  ltexprlem4  10806  ltresr  10907  1re  10986  infm3  11945  elnnz  12340  dfz2  12349  2rexuz  12651  nnwos  12666  eluz2b1  12670  qexALT  12715  elxr  12863  dflt2  12893  xrsupss  13054  xrinfmss  13055  elixx1  13099  elioo2  13131  dfrp2  13139  elioopnf  13186  elicopnf  13188  elfz1  13255  fznn  13335  fzp1nel  13351  fznn0  13359  preduz  13389  prinfzo0  13437  injresinj  13519  nn0opthlem1  13993  faclbnd4lem1  14018  hashfxnn0  14062  hashprdifel  14124  hashgt23el  14150  hashfun  14163  hashf1  14182  fz1isolem  14186  f1oun2prg  14641  brtrclfv  14724  shftdm  14793  rediv  14853  imdiv  14860  rexanre  15069  caubnd  15081  climreu  15276  prodmo  15657  dvdslelem  16029  3dvdsdec  16052  3dvds2dec  16053  bitsval  16142  smueqlem  16208  algcvgblem  16293  lcmfunsnlem2  16356  isprm2  16398  isprm3  16399  isprm4  16400  pythagtriplem2  16529  elgz  16643  hashbc0  16717  0ram  16732  isstruct  16864  issect  17476  isfull2  17638  isfth2  17642  fucinv  17702  eldmcoa  17791  isdrs  18030  submacs  18476  isnsg4  18806  isgim  18889  gaorb  18924  oppgid  18974  oppgsubm  18980  oppgcntz  18982  ispgp  19208  efgsdm  19347  efgcpbllema  19371  iscyg2  19493  isring  19798  isirred2  19954  opprirred  19955  dfrhm2  19972  drngid2  20018  opprsubrg  20056  issdrg  20074  islmod  20138  lss1d  20236  islmhm  20300  islmim  20335  lbsextlem2  20432  lidlnz  20510  isnzr2  20545  dfprm2  20706  isphl  20844  elocv  20884  iunocv  20897  isobs  20938  islinds  21027  isassa  21074  1mavmul  21708  toprntopon  22085  isbasis3g  22110  fctop  22165  cctop  22167  isclo2  22250  restsn  22332  lmbr  22420  ist0-3  22507  2ndcdisj  22618  1stccnp  22624  islocfin  22679  1stckgenlem  22715  txbas  22729  ptbasin  22739  tx2cn  22772  fbfinnfr  23003  fbasrn  23046  filuni  23047  ufinffr  23091  fin1aufil  23094  rnelfmlem  23114  flimrest  23145  alexsubALTlem3  23211  alexsubALTlem4  23212  tgphaus  23279  istlm  23347  iscusp2  23465  metuel2  23732  isngp2  23764  isnlm  23850  isphtpc  24168  phtpcer  24169  om1elbas  24206  isclm  24238  iscvsp  24302  iscph  24345  iscau3  24453  minveclem3b  24603  elovolm  24650  ioombl1lem4  24736  dyaddisj  24771  vitali  24788  itg1climres  24890  itg2seq  24918  itg2monolem1  24926  itg2mono  24929  limcrcl  25049  lhop1  25189  itgsubst  25224  mdegleb  25240  isuc1p  25316  ismon1p  25318  plydivex  25468  ellogdm  25805  1cubr  26003  atandm2  26038  birthdaylem3  26114  dmarea  26118  dchrelbas2  26396  dchrelbas4  26402  axcontlem7  27349  nb3grpr  27760  nb3grpr2  27761  upgrwlkcompim  28020  wlkson  28034  wlkonprop  28036  wksonproplem  28082  ispth  28100  wwlknon  28231  wwlksnextinj  28273  wspthsnwspthsnon  28290  elwspths2spth  28341  rusgrnumwwlkl1  28342  clwwlkccatlem  28362  erclwwlkref  28393  frgr3v  28648  nmoubi  29143  nmobndseqi  29150  nmobndseqiALT  29151  minvecolem1  29245  isch2  29594  hlimreui  29610  isch3  29612  ocsh  29654  dfch2  29778  spanuni  29915  nonbooli  30022  5oalem7  30031  adjsym  30204  elbdop2  30242  dmadjss  30258  nmopub  30279  nmfnleub  30296  nmop0h  30362  pjssposi  30543  pjordi  30544  cvbr2  30654  cvnbtwn2  30658  mdsl2i  30693  cvmdi  30695  elat2  30711  atom1d  30724  chirredi  30765  cdj3i  30812  or3di  30819  opreu2reu1  30841  mo5f  30846  reuxfrdf  30848  rexunirn  30849  difrab2  30854  iuninc  30909  disjorf  30927  disjunsn  30942  rabfmpunirn  30999  aciunf1  31009  funcnv5mpt  31014  eliccelico  31107  elicoelioo  31108  isomnd  31336  omndmul2  31347  isslmd  31464  islinds5  31572  ismxidl  31643  hasheuni  32062  pwsiga  32107  sigainb  32113  issros  32152  2ndmbfm  32237  omssubaddlem  32275  omssubadd  32276  sitgaddlemb  32324  eulerpartlemgvv  32352  eulerpartlemn  32357  probun  32395  ballotlem2  32464  ballotlemodife  32473  bnj252  32691  bnj253  32692  bnj255  32693  bnj345  32702  bnj133  32715  bnj976  32766  bnj1098  32772  bnj121  32859  bnj130  32863  bnj150  32865  bnj581  32897  bnj607  32905  bnj865  32912  bnj917  32923  bnj934  32924  bnj964  32932  bnj983  32940  bnj996  32945  bnj1021  32955  bnj1033  32958  bnj1047  32962  bnj1049  32963  bnj1090  32968  bnj1128  32979  bnj1175  32993  bnj1189  32998  bnj1253  33006  bnj1312  33047  exdifsn  33062  fineqvrep  33073  fineqvac  33075  erdszelem9  33170  erdszelem10  33171  pconnconn  33202  cvmliftiota  33272  fmlaomn0  33361  fmla0disjsuc  33369  fmlasucdisj  33370  dmopab3rexdif  33376  elmthm  33547  nepss  33671  xpab  33686  dfso2  33731  elrn3  33738  imaindm  33762  elpotr  33766  dfon2lem5  33772  dfon2lem7  33774  dfon2lem8  33775  frxp2  33800  poxp3  33805  soseq  33812  elwlim  33826  wzel  33827  elno3  33867  nosgnn0  33870  nosepon  33877  nocvxminlem  33981  scutcut  34004  scutbday  34007  dmscut  34014  scutf  34015  sltrec  34023  made0  34066  brtxp2  34192  brpprod3a  34197  eltrans  34202  dfon3  34203  dffix2  34216  dffun10  34225  elfuns  34226  brsingle  34228  brimg  34248  funpartfun  34254  funpartfv  34256  cgrxfr  34366  segletr  34425  outsideoftr  34440  neifg  34569  filnetlem4  34579  df3nandALT1  34597  bj-consensusALT  34769  bj-df-ifc  34770  bj-biexal3  34898  bj-nfnnfTEMP  34949  bj-denoteslem  35064  bj-denotes  35065  bj-ralvw  35073  bj-rexvw  35074  bj-rexcom4bv  35076  bj-rexcom4b  35077  bj-sbeq  35095  bj-inrab  35124  bj-rcleqf  35224  bj-dfmpoa  35298  bj-imdirco  35370  topdifinffinlem  35527  topdifinfeq  35530  relowlssretop  35543  relowlpssretop  35544  rdgeqoa  35550  domalom  35584  nlpineqsn  35588  fvineqsneq  35592  wl-ifpimpr  35646  wl-df3xor3  35650  wl-3xorbi  35653  wl-3xorbi2  35654  wl-2xor  35663  wl-2mintru2  35671  wl-dfclab  35756  rabiun  35759  phpreu  35770  fin2solem  35772  matunitlindflem2  35783  ptrest  35785  poimirlem25  35811  poimirlem27  35813  poimirlem30  35816  ismblfin  35827  ovoliunnfl  35828  voliunnfl  35830  volsupnfl  35831  itg2addnclem2  35838  fdc  35912  prdstotbnd  35961  isdrngo1  36123  ispridl  36201  ismaxidl  36207  impor  36248  selconj  36267  tradd  36272  scott0f  36336  inxpss3  36458  idinxpssinxp2  36462  idinxpssinxp3  36463  dfrel5  36490  ineleq  36495  moantr  36503  dfxrn2  36515  inxpxrn  36530  rnxrnres  36534  1cossres  36561  cocossss  36568  cossssid4  36597  cossssid5  36598  cosscnvssid5  36605  cossid  36607  dfssr2  36626  cnvrefrelcoss2  36660  cosselcnvrefrels2  36661  eqvrelcoss  36739  eqvrelcoss2  36741  dfcoeleqvrel  36744  refrelredund4  36757  cnvepresdmqs  36774  dfmember  36793  dfdisjALTV  36833  dfeldisj3  36839  dfeldisj4  36840  dfeldisj5  36841  prter1  36902  islshp  37002  islshpat  37040  lcvbr2  37045  lcvnbtwn2  37050  cvrnbtwn3  37299  isatl  37322  ishlat1  37375  ishlat2  37376  cvrat4  37466  pmapglbx  37792  lhpexle3  38035  dib1dim  39188  diblsmopel  39194  lcfls1lem  39557  prjsperref  40454  prjspeclsp  40460  rexrabdioph  40625  dford4  40860  isdomn3  41038  ifpdfor2  41059  ifpdfan2  41061  ifpdfor  41063  ifpdfan  41064  ifpnot23b  41080  ifpnot23c  41082  ifpnot23d  41083  ifpim123g  41098  ifpbibib  41108  clss2lem  41201  imaiun1  41241  coiun1  41242  brfvrcld2  41282  iunrelexp0  41292  brtrclfv2  41317  snhesn  41376  dffrege76  41529  frege97  41550  frege98  41551  frege109  41562  frege110  41563  dffrege115  41568  frege131  41584  frege133  41586  ntrneineine1lem  41676  ntrneiel2  41678  ntrneiiso  41683  gneispace3  41725  scotteld  41846  ismnuprim  41894  ismnushort  41901  dfuniv2  41902  pm11.52  41987  pm11.58  41990  pm13.192  42010  impexpdcom  42117  sbc3or  42134  opelopab4  42153  uunT12p1  42402  uunT12p2  42403  uunT12p3  42404  uun2221  42415  uun2221p1  42416  uun2221p2  42417  undif3VD  42484  ndisj2  42581  nssrex  42618  rabssf  42650  bothtbothsame  44373  bothfbothsame  44374  aiffbtbat  44382  reuabaiotaiota  44558  2reu8i  44584  2reuimp0  44585  ichn  44887  dfodd2  45067  dfeven5  45097  dfodd7  45098  1nevenALTV  45122  oddprmne2  45146  isrng  45413  isrnghm  45429  islindeps2  45803  isldepslvec2  45805  line2xlem  46078  rextru  46128  rmotru  46129  reutru  46130  isnrm4  46203  iscnrm4  46227  isthincd2  46298  thinccic  46321  setrec1lem3  46374  aacllem  46484