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  463  dfbi2  475  imdistan  568  pm5.32  574  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  1492  nannan  1495  nanbi  1498  xorcom  1512  xorneg  1522  xorbi12i  1523  norcom  1530  noran  1533  norasslem1  1535  trunortru  1590  trunorfal  1591  cadan  1610  cadcomb  1614  nic-ax  1675  nic-axALT  1676  nf3  1788  nfnbiOLD  1858  19.43  1885  equsv  2006  sbrimvw  2094  sbcom2  2161  sb5  2267  nf5  2278  nf6  2279  sbrim  2300  sb6x  2463  2sb5rf  2471  2sb6rf  2472  sb4b  2474  sb5f  2497  sbequ8  2500  sbhb  2520  eu6lem  2567  eu1  2606  issetlem  2813  cleqh  2863  clelabOLD  2880  cleqf  2934  sbabel  2938  necon3bii  2993  neor  3034  neorian  3037  rextru  3077  r19.26m  3110  r19.26-3  3112  r19.43  3122  r2allem  3142  r19.23t  3252  ralcom4  3283  rexcomOLD  3288  moel  3398  moelOLD  3401  rabid2f  3463  rabid2OLD  3465  eqv  3483  eqvf  3484  ralv  3498  rexv  3499  reuv  3500  rmov  3501  rexcom4b  3503  ceqsex4v  3532  ceqsex8v  3534  ceqsrexv  3643  rexab  3690  ralrab2  3694  rexrab2  3696  reu2  3721  reu3  3723  reueq  3733  2reuswap  3742  2reuswap2  3743  reuind  3749  2reu5lem3  3753  2rmoswap  3757  sbc3an  3847  rmo2  3881  rmoanim  3888  rmoanimALT  3889  dfss2  3968  dfss2OLD  3969  dfss3  3970  dfss3f  3973  ssabral  4059  rabss  4069  ssrabeq  4082  uniiunlem  4084  sspsstri  4102  npss  4110  dfdif3  4114  raldifb  4144  uncom  4153  inass  4219  elsymdifxor  4249  nsspssun  4257  dfss4  4258  dfun2  4259  dfin2  4260  indi  4273  indifdirOLD  4285  difin2  4291  reupick3  4319  eq0f  4340  neq0f  4341  eq0  4343  eq0ALT  4344  dfnf5  4377  rabn0  4385  csbab  4437  vss  4443  disj  4447  disjOLD  4448  disj3  4453  undisj1  4461  undisj2  4462  inundif  4478  undif  4481  undifr  4482  rabsssn  4670  exsnrex  4684  euabsn2  4729  euabsn  4730  raldifsni  4798  tppreqb  4808  pwpw0  4816  prssg  4822  ssunsn  4831  preqsn  4862  pwpr  4902  dfuni2  4910  unissb  4943  unissbOLD  4944  elint2  4957  ssint  4968  uniintab  4992  dfiin2g  5035  iunid  5063  iunn0  5070  iunxun  5097  iunxiun  5100  iinpw  5109  disjor  5128  disjxiun  5145  dftr2  5267  dftr5OLD  5270  dftr3  5271  dftr4  5272  axrep6  5292  vnex  5314  inuni  5343  eusv2  5394  reusv2lem4  5399  rexxfr  5414  sspwb  5449  opthneg  5481  pwssun  5571  dfid3  5577  dffr6  5634  dffr2  5640  dffr2ALT  5641  opthprc  5740  elxp3  5742  xpiundir  5747  elvv  5750  reliun  5816  inxp  5832  raliunxp  5839  cnvuni  5886  dmopab2rex  5917  dm0rn0  5924  dfres3  5986  ssdmres  6004  elidinxp  6043  idinxpres  6046  dfima2  6061  args  6091  dffr3  6098  cotrg  6108  cotrgOLD  6109  cotrgOLDOLD  6110  intasym  6116  asymref  6117  intirr  6119  xpnz  6158  xp11  6174  ssrnres  6177  xpimasn  6184  coiun  6255  coass  6264  cnvso  6287  elsnxp  6290  dfpo2  6295  imaindm  6298  dffr4  6320  dfse3  6337  frpoind  6343  wfiOLD  6352  dflim2  6421  orddif  6460  dffun2OLDOLD  6555  dffun6  6556  dffun6f  6561  dffun7  6575  dffun9  6577  funfn  6578  svrelfun  6620  mptfnf  6685  dffn2  6719  dffn3  6730  fint  6770  dffn4  6811  dff1o4  6841  brprcneu  6881  brprcneuALT  6882  eqfnfv3  7034  fnreseql  7049  fsn  7135  ftpg  7156  abrexco  7245  imaiun  7246  dff13  7256  isof1oidb  7323  isof1oopb  7324  isocnv2  7330  eloprabga  7518  mpo2eqb  7543  elovmpo  7653  sorpss  7720  abexex  7960  elxp6  8011  elxp7  8012  releldm2  8031  opiota  8047  fnmpo  8057  frxp  8114  frxp2  8132  soseq  8147  cnvimadfsn  8159  mpoxneldm  8199  dftpos4  8232  frrlem9  8281  wfrlem8OLD  8318  wfrfunOLD  8321  dfrecs3  8374  dfrecs3OLD  8375  tfrlem7  8385  ondif1  8503  oarec  8564  oeeu  8605  0er  8742  eroveu  8808  erovlem  8809  elixpconst  8901  domen  8959  brsdom  8973  brdom2  8980  reuen1  9027  sbthlem10  9094  brsdom2  9099  xpf1o  9141  unfi  9174  sbthfilem  9203  onfin2  9233  0sdom1domALT  9241  modom  9246  unfiOLD  9315  marypha2lem3  9434  wemapsolem  9547  elom3  9645  dfom5  9647  brttrcl2  9711  ttrcltr  9713  ttrclse  9724  trcl  9725  epfrs  9728  frind  9747  rankf  9791  scottexs  9884  scott0s  9885  cplem1  9886  hta  9894  djuexb  9906  pm54.43lem  9997  alephsuc2  10077  iscard3  10090  aceq0  10115  aceq3lem  10117  dfac3  10118  dfac5lem2  10121  dfac5  10125  dfac7  10129  dfac12a  10145  kmlem12  10158  kmlem14  10160  kmlem15  10161  infmap2  10215  ackbij2  10240  dfacfin7  10396  ituniiun  10419  zorng  10501  brdom7disj  10528  entri2  10555  alephreg  10579  fpwwe2lem11  10638  fpwwe2lem12  10639  pwfseqlem1  10655  grutsk  10819  axgroth4  10829  grothprim  10831  grothtsk  10832  elni2  10874  ltsopi  10885  genpass  11006  psslinpr  11028  ltexprlem4  11036  ltresr  11137  1re  11218  infm3  12177  elnnz  12572  dfz2  12581  2rexuz  12888  nnwos  12903  eluz2b1  12907  qexALT  12952  elxr  13100  dflt2  13131  xrsupss  13292  xrinfmss  13293  elixx1  13337  elioo2  13369  dfrp2  13377  elioopnf  13424  elicopnf  13426  elfz1  13493  fznn  13573  fzp1nel  13589  fznn0  13597  preduz  13627  prinfzo0  13675  injresinj  13757  nn0opthlem1  14232  faclbnd4lem1  14257  hashfxnn0  14301  hashprdifel  14362  hashgt23el  14388  hashfun  14401  hashf1  14422  fz1isolem  14426  f1oun2prg  14872  brtrclfv  14953  shftdm  15022  rediv  15082  imdiv  15089  rexanre  15297  caubnd  15309  climreu  15504  prodmo  15884  dvdslelem  16256  3dvdsdec  16279  3dvds2dec  16280  bitsval  16369  smueqlem  16435  algcvgblem  16518  lcmfunsnlem2  16581  isprm2  16623  isprm3  16624  isprm4  16625  pythagtriplem2  16754  elgz  16868  hashbc0  16942  0ram  16957  isstruct  17089  issect  17704  isfull2  17866  isfth2  17870  fucinv  17930  eldmcoa  18019  isdrs  18258  submacs  18744  isnsg4  19083  isgim  19176  gaorb  19212  oppgid  19264  oppgsubm  19270  oppgcntz  19272  ispgp  19501  efgsdm  19639  efgcpbllema  19663  iscyg2  19791  isrng  20048  isring  20131  isirred2  20312  opprirred  20313  isrnghm  20332  dfrhm2  20365  isnzr2  20409  opprsubrng  20447  opprsubrg  20483  drngid2  20521  issdrg  20547  islmod  20618  lss1d  20718  islmhm  20782  islmim  20817  lbsextlem2  20917  lidlnz  21002  dfprm2  21244  isphl  21400  elocv  21440  iunocv  21453  isobs  21494  islinds  21583  1mavmul  22270  toprntopon  22647  isbasis3g  22672  fctop  22727  cctop  22729  isclo2  22812  restsn  22894  lmbr  22982  ist0-3  23069  2ndcdisj  23180  1stccnp  23186  islocfin  23241  1stckgenlem  23277  txbas  23291  ptbasin  23301  tx2cn  23334  fbfinnfr  23565  fbasrn  23608  filuni  23609  ufinffr  23653  fin1aufil  23656  rnelfmlem  23676  flimrest  23707  alexsubALTlem3  23773  alexsubALTlem4  23774  tgphaus  23841  istlm  23909  iscusp2  24027  metuel2  24294  isngp2  24326  isnlm  24412  isphtpc  24734  phtpcer  24735  om1elbas  24772  isclm  24804  iscvsp  24868  iscph  24911  iscau3  25019  minveclem3b  25169  elovolm  25216  ioombl1lem4  25302  dyaddisj  25337  vitali  25354  itg1climres  25456  itg2seq  25484  itg2monolem1  25492  itg2mono  25495  limcrcl  25615  lhop1  25755  itgsubst  25790  mdegleb  25806  isuc1p  25882  ismon1p  25884  plydivex  26034  ellogdm  26371  1cubr  26571  atandm2  26606  birthdaylem3  26682  dmarea  26686  dchrelbas2  26964  dchrelbas4  26970  elno3  27382  nosgnn0  27385  nosepon  27392  nocvxminlem  27503  scutcut  27527  scutbday  27530  dmscut  27537  scutf  27538  sltrec  27546  made0  27593  addsprop  27686  negsproplem2  27730  negsprop  27736  mulsprop  27813  precsexlem10  27889  axcontlem7  28483  nb3grpr  28894  nb3grpr2  28895  upgrwlkcompim  29155  wlkson  29168  wlkonprop  29170  wksonproplem  29216  wksonproplemOLD  29217  ispth  29235  wwlknon  29366  wwlksnextinj  29408  wspthsnwspthsnon  29425  elwspths2spth  29476  rusgrnumwwlkl1  29477  clwwlkccatlem  29497  erclwwlkref  29528  frgr3v  29783  nmoubi  30280  nmobndseqi  30287  nmobndseqiALT  30288  minvecolem1  30382  isch2  30731  hlimreui  30747  isch3  30749  ocsh  30791  dfch2  30915  spanuni  31052  nonbooli  31159  5oalem7  31168  adjsym  31341  elbdop2  31379  dmadjss  31395  nmopub  31416  nmfnleub  31433  nmop0h  31499  pjssposi  31680  pjordi  31681  cvbr2  31791  cvnbtwn2  31795  mdsl2i  31830  cvmdi  31832  elat2  31848  atom1d  31861  chirredi  31902  cdj3i  31949  or3di  31956  opreu2reu1  31979  mo5f  31984  reuxfrdf  31986  rexunirn  31987  difrab2  31993  iuninc  32047  disjorf  32065  disjunsn  32080  rabfmpunirn  32133  aciunf1  32143  funcnv5mpt  32148  eliccelico  32243  elicoelioo  32244  isomnd  32477  omndmul2  32488  isslmd  32605  islinds5  32742  ismxidl  32840  hasheuni  33369  pwsiga  33414  sigainb  33420  issros  33459  2ndmbfm  33546  omssubaddlem  33584  omssubadd  33585  sitgaddlemb  33633  eulerpartlemgvv  33661  eulerpartlemn  33666  probun  33704  ballotlem2  33773  ballotlemodife  33782  bnj252  34000  bnj253  34001  bnj255  34002  bnj345  34011  bnj133  34024  bnj976  34074  bnj1098  34080  bnj121  34167  bnj130  34171  bnj150  34173  bnj581  34205  bnj607  34213  bnj865  34220  bnj917  34231  bnj934  34232  bnj964  34240  bnj983  34248  bnj996  34253  bnj1021  34263  bnj1033  34266  bnj1047  34270  bnj1049  34271  bnj1090  34276  bnj1128  34287  bnj1175  34301  bnj1189  34306  bnj1253  34314  bnj1312  34355  exdifsn  34370  fineqvrep  34381  fineqvac  34383  erdszelem9  34476  erdszelem10  34477  pconnconn  34508  cvmliftiota  34578  fmlaomn0  34667  fmla0disjsuc  34675  fmlasucdisj  34676  dmopab3rexdif  34682  elmthm  34853  nepss  34979  xpab  34987  dfso2  35017  elrn3  35024  elpotr  35045  dfon2lem5  35051  dfon2lem7  35053  dfon2lem8  35054  elwlim  35087  wzel  35088  brtxp2  35145  brpprod3a  35150  eltrans  35155  dfon3  35156  dffix2  35169  dffun10  35178  elfuns  35179  brsingle  35181  brimg  35201  funpartfun  35207  funpartfv  35209  cgrxfr  35319  segletr  35378  outsideoftr  35393  neifg  35559  filnetlem4  35569  df3nandALT1  35587  bj-consensusALT  35759  bj-df-ifc  35760  bj-biexal3  35888  bj-nfnnfTEMP  35939  bj-denoteslem  36053  bj-denotes  36054  bj-ralvw  36062  bj-rexvw  36063  bj-rexcom4bv  36065  bj-rexcom4b  36066  bj-sbeq  36084  bj-inrab  36110  bj-rcleqf  36209  bj-dfmpoa  36302  bj-imdirco  36374  topdifinffinlem  36531  topdifinfeq  36534  relowlssretop  36547  relowlpssretop  36548  rdgeqoa  36554  domalom  36588  nlpineqsn  36592  fvineqsneq  36596  wl-ifpimpr  36650  wl-df3xor3  36654  wl-3xorbi  36657  wl-3xorbi2  36658  wl-2xor  36667  wl-2mintru2  36675  wl-dfclab  36761  rabiun  36764  phpreu  36775  fin2solem  36777  matunitlindflem2  36788  ptrest  36790  poimirlem25  36816  poimirlem27  36818  poimirlem30  36821  ismblfin  36832  ovoliunnfl  36833  voliunnfl  36835  volsupnfl  36836  itg2addnclem2  36843  fdc  36916  prdstotbnd  36965  isdrngo1  37127  ispridl  37205  ismaxidl  37211  impor  37252  selconj  37271  tradd  37276  scott0f  37340  r2alan  37419  inxpss3  37486  idinxpssinxp2  37490  idinxpssinxp3  37491  dfrel5  37518  ineleq  37526  moantr  37536  dfxrn2  37549  inxpxrn  37568  rnxrnres  37572  coss1cnvres  37590  1cossres  37602  cocossss  37609  cossssid4  37643  cossssid5  37644  cosscnvssid5  37651  cossid  37653  dfssr2  37672  cnvrefrelcoss2  37710  cosselcnvrefrels2  37711  eqvrelcoss  37790  eqvrelcoss2  37792  dfcoeleqvrel  37795  refrelredund4  37808  cnvepresdmqs  37826  dfcomember  37845  dfdisjALTV  37886  dfeldisj3  37892  dfeldisj4  37893  dfeldisj5  37894  disjres  37917  prter1  38052  islshp  38152  islshpat  38190  lcvbr2  38195  lcvnbtwn2  38200  cvrnbtwn3  38449  isatl  38472  ishlat1  38525  ishlat2  38526  cvrat4  38617  pmapglbx  38943  lhpexle3  39186  dib1dim  40339  diblsmopel  40345  lcfls1lem  40708  prjsperref  41650  prjspeclsp  41656  rexrabdioph  41834  dford4  42070  isdomn3  42248  onsupuni  42280  dflim6  42316  tfsconcatlem  42388  naddgeoa  42447  ifpdfor2  42514  ifpdfan2  42516  ifpdfor  42518  ifpdfan  42519  ifpnot23b  42535  ifpnot23c  42537  ifpnot23d  42538  ifpim123g  42553  ifpbibib  42563  clss2lem  42664  imaiun1  42704  coiun1  42705  brfvrcld2  42745  iunrelexp0  42755  brtrclfv2  42780  snhesn  42839  dffrege76  42992  frege97  43013  frege98  43014  frege109  43025  frege110  43026  dffrege115  43031  frege131  43047  frege133  43049  ntrneineine1lem  43137  ntrneiel2  43139  ntrneiiso  43144  gneispace3  43186  scotteld  43307  ismnuprim  43355  ismnushort  43362  dfuniv2  43363  pm11.52  43448  pm11.58  43451  pm13.192  43471  impexpdcom  43578  sbc3or  43595  opelopab4  43614  uunT12p1  43863  uunT12p2  43864  uunT12p3  43865  uun2221  43876  uun2221p1  43877  uun2221p2  43878  undif3VD  43945  ndisj2  44040  nssrex  44077  rabssf  44110  bothtbothsame  45908  bothfbothsame  45909  aiffbtbat  45917  reuabaiotaiota  46094  2reu8i  46120  2reuimp0  46121  ichn  46423  dfodd2  46603  dfeven5  46633  dfodd7  46634  1nevenALTV  46658  oddprmne2  46682  islindeps2  47252  isldepslvec2  47254  line2xlem  47527  rmotru  47577  reutru  47578  isnrm4  47651  iscnrm4  47675  isthincd2  47746  thinccic  47769  setrec1lem3  47822  aacllem  47936