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  3372  rabid2f  3432  eqv  3452  eqvf  3453  ralv  3469  rexv  3470  reuv  3471  rmov  3472  rexcom4b  3474  ceqsex4v  3498  ceqsex8v  3500  ceqsrexv  3611  rexab  3655  ralrab2  3658  rexrab2  3660  reu2  3685  reu3  3687  reueq  3697  2reuswap  3706  2reuswap2  3707  reuind  3713  2reu5lem3  3717  2rmoswap  3721  rmo2  3839  rmoanim  3846  rmoanimALT  3847  dfss3  3924  dfss3f  3927  ssabral  4018  rabss  4024  ssrabeq  4038  uniiunlem  4041  sspsstri  4059  npss  4067  dfdif3OLD  4072  raldifb  4103  uncom  4112  inass  4182  elsymdifxor  4214  nsspssun  4222  dfss4  4223  dfun2  4224  dfin2  4225  indi  4238  reupick3  4284  eq0f  4301  neq0f  4302  eq0ALT  4305  dfnf5  4336  rabn0  4343  csbab  4394  vss  4400  disj  4404  disj3  4408  undisj1  4416  undisj2  4417  inundif  4433  undif  4436  undifr  4437  rabsssn  4627  exsnrex  4639  euabsn2  4684  euabsn  4685  raldifsni  4753  tppreqb  4763  pwpw0  4771  prssg  4777  ssunsn  4786  prneimg2  4813  preqsn  4820  pwpr  4859  dfuni2  4867  unissb  4898  elint2  4911  ssint  4921  uniintab  4943  dfiin2g  4988  iunid  5018  iunn0  5024  iunxun  5051  iunxiun  5054  iinpw  5063  disjor  5082  disjxiun  5097  dftr2  5209  dftr3  5212  dftr4  5213  axrep6OLD  5236  vnex  5261  inuni  5297  eusv2  5343  reusv2lem4  5348  rexxfr  5363  sspwb  5404  opthneg  5437  pwssun  5524  dfid3  5530  dffr6  5588  dffr2  5593  dffr2ALT  5594  opthprc  5696  elxp3  5698  xpiundir  5704  elvv  5707  inxpOLD  5789  raliunxp  5796  cnvuni  5843  dmopab2rex  5874  dm0rn0OLD  5882  dfres3  5951  ssdmres  5980  elidinxp  6011  idinxpres  6014  dfima2  6029  args  6059  dffr3  6066  cotrg  6076  intasym  6080  asymref  6081  intirr  6083  xpnz  6125  xp11  6141  ssrnres  6144  xpimasn  6151  coiun  6223  coass  6232  cnvso  6254  elsnxp  6257  dfpo2  6262  imaindm  6265  dffr4  6286  dfse3  6302  frpoind  6308  dflim2  6383  orddif  6423  dffun6  6511  dffun6f  6515  dffun7  6527  dffun9  6529  funfn  6530  svrelfun  6572  mptfnf  6635  dffn2  6672  dffn3  6682  fint  6721  dffn4  6760  dff1o4  6790  brprcneu  6832  brprcneuALT  6833  eqfnfv3  6987  fnreseql  7002  fsn  7090  ftpg  7111  abrexco  7200  imaiun  7201  dff13  7210  isof1oidb  7280  isof1oopb  7281  isocnv2  7287  eloprabga  7477  mpo2eqb  7500  elovmpo  7613  sorpss  7683  abexex  7925  elxp6  7977  elxp7  7978  releldm2  7997  opiota  8013  fnmpo  8023  frxp  8078  frxp2  8096  soseq  8111  cnvimadfsn  8124  mpoxneldm  8164  dftpos4  8197  frrlem9  8246  dfrecs3  8314  tfrlem7  8324  ondif1  8438  oarec  8499  oeeu  8541  brinxper  8675  0er  8684  eroveu  8761  erovlem  8762  elixpconst  8855  domen  8910  brsdom  8923  brdom2  8931  reuen1  8975  sbthlem10  9036  brsdom2  9041  xpf1o  9079  unfi  9107  sbthfilem  9134  onfin2  9153  0sdom1domALT  9159  modom  9163  marypha2lem3  9352  wemapsolem  9467  elom3  9569  dfom5  9571  brttrcl2  9635  ttrcltr  9637  ttrclse  9648  trcl  9649  epfrs  9652  frind  9674  rankf  9718  scottexs  9811  scott0s  9812  cplem1  9813  hta  9821  djuexb  9833  pm54.43lem  9924  alephsuc2  10002  iscard3  10015  aceq0  10040  aceq3lem  10042  dfac3  10043  dfac5lem2  10046  dfac5  10051  dfac7  10055  dfac12a  10071  kmlem12  10084  kmlem14  10086  kmlem15  10087  infmap2  10139  ackbij2  10164  dfacfin7  10321  ituniiun  10344  zorng  10426  brdom7disj  10453  entri2  10480  alephreg  10505  fpwwe2lem11  10564  fpwwe2lem12  10565  pwfseqlem1  10581  grutsk  10745  axgroth4  10755  grothprim  10757  grothtsk  10758  elni2  10800  ltsopi  10811  genpass  10932  psslinpr  10954  ltexprlem4  10962  ltresr  11063  infm3  12113  elnnz  12510  dfz2  12519  2rexuz  12825  nnwos  12840  eluz2b1  12844  qexALT  12889  elxr  13042  dflt2  13074  xrsupss  13236  xrinfmss  13237  elixx1  13282  elioo2  13314  dfrp2  13322  elioopnf  13371  elicopnf  13373  elfz1  13440  fznn  13520  fzp1nel  13539  fznn0  13547  preduz  13578  prinfzo0  13626  injresinj  13719  nn0opthlem1  14203  faclbnd4lem1  14228  hashfxnn0  14272  hashprdifel  14333  hashgt23el  14359  hashfun  14372  hashf1  14392  fz1isolem  14396  f1oun2prg  14852  brtrclfv  14937  shftdm  15006  rediv  15066  imdiv  15073  rexanre  15282  caubnd  15294  climreu  15491  prodmo  15871  dvdslelem  16248  3dvdsdec  16271  3dvds2dec  16272  bitsval  16363  smueqlem  16429  algcvgblem  16516  lcmfunsnlem2  16579  isprm2  16621  isprm3  16622  isprm4  16623  pythagtriplem2  16757  elgz  16871  hashbc0  16945  0ram  16960  isstruct  17091  issect  17689  isfull2  17849  isfth2  17853  fucinv  17912  eldmcoa  18001  isdrs  18236  submacs  18764  isnsg4  19108  isgim  19203  gaorb  19248  oppgid  19297  oppgsubm  19303  oppgcntz  19305  ispgp  19533  efgsdm  19671  efgcpbllema  19695  iscyg2  19823  isomnd  20064  omndmul2  20074  isrng  20101  isring  20184  isirred2  20369  opprirred  20370  isrnghm  20389  dfrhm2  20422  isnzr2  20463  opprsubrng  20504  opprsubrg  20538  isdomn3  20660  drngid2  20697  issdrg  20733  islmod  20827  lss1d  20926  islmhm  20991  islmim  21026  lbsextlem2  21126  lidlnz  21209  dfprm2  21440  isphl  21595  elocv  21635  iunocv  21648  isobs  21687  islinds  21776  1mavmul  22504  toprntopon  22881  isbasis3g  22905  fctop  22960  cctop  22962  isclo2  23044  restsn  23126  lmbr  23214  ist0-3  23301  2ndcdisj  23412  1stccnp  23418  islocfin  23473  1stckgenlem  23509  txbas  23523  ptbasin  23533  tx2cn  23566  fbfinnfr  23797  fbasrn  23840  filuni  23841  ufinffr  23885  fin1aufil  23888  rnelfmlem  23908  flimrest  23939  alexsubALTlem3  24005  alexsubALTlem4  24006  tgphaus  24073  istlm  24141  iscusp2  24257  metuel2  24521  isngp2  24553  isnlm  24631  isphtpc  24961  phtpcer  24962  om1elbas  25000  isclm  25032  iscvsp  25096  iscph  25138  iscau3  25246  minveclem3b  25396  elovolm  25444  ioombl1lem4  25530  dyaddisj  25565  vitali  25582  itg1climres  25683  itg2seq  25711  itg2monolem1  25719  itg2mono  25722  limcrcl  25843  lhop1  25987  itgsubst  26024  mdegleb  26037  isuc1p  26114  ismon1p  26116  plydivex  26273  ellogdm  26616  1cubr  26820  atandm2  26855  birthdaylem3  26931  dmarea  26935  dchrelbas2  27216  dchrelbas4  27222  elno3  27635  nosgnn0  27638  nosepon  27645  nocvxminlem  27762  cutcuts  27789  cutbday  27792  dmcuts  27799  cutsf  27800  ltsrec  27809  made0  27871  addsprop  27984  negsproplem2  28037  negsprop  28043  mulsprop  28138  precsexlem10  28224  elzs2  28407  elnnzs  28409  bdayfinbndlem1  28475  recut  28502  axcontlem7  29055  nb3grpr  29467  nb3grpr2  29468  upgrwlkcompim  29728  wlkson  29740  wlkonprop  29742  wksonproplem  29788  ispth  29806  wwlknon  29942  wwlksnextinj  29984  wspthsnwspthsnon  30001  elwspths2spth  30055  rusgrnumwwlkl1  30056  clwwlkccatlem  30076  erclwwlkref  30107  frgr3v  30362  nmoubi  30859  nmobndseqi  30866  nmobndseqiALT  30867  minvecolem1  30961  isch2  31310  hlimreui  31326  isch3  31328  ocsh  31370  dfch2  31494  spanuni  31631  nonbooli  31738  5oalem7  31747  adjsym  31920  elbdop2  31958  dmadjss  31974  nmopub  31995  nmfnleub  32012  nmop0h  32078  pjssposi  32259  pjordi  32260  cvbr2  32370  cvnbtwn2  32374  mdsl2i  32409  cvmdi  32411  elat2  32427  atom1d  32440  chirredi  32481  cdj3i  32528  or3di  32544  opreu2reu1  32569  mo5f  32574  reuxfrdf  32576  rexunirn  32577  difrab2  32583  rabsspr  32587  rabsstp  32588  tpssg  32623  iuninc  32646  disjorf  32665  disjunsn  32680  rabfmpunirn  32742  aciunf1  32752  funcnv5mpt  32756  eliccelico  32867  elicoelioo  32868  isslmd  33295  islinds5  33459  ismxidl  33554  1arithufdlem4  33639  hasheuni  34262  pwsiga  34307  sigainb  34313  issros  34352  2ndmbfm  34438  omssubaddlem  34476  omssubadd  34477  sitgaddlemb  34525  eulerpartlemgvv  34553  eulerpartlemn  34558  probun  34596  ballotlem2  34666  ballotlemodife  34675  bnj252  34879  bnj253  34880  bnj255  34881  bnj345  34890  bnj133  34903  bnj976  34953  bnj1098  34959  bnj121  35045  bnj130  35049  bnj150  35051  bnj581  35083  bnj607  35091  bnj865  35098  bnj917  35109  bnj934  35110  bnj964  35118  bnj983  35126  bnj996  35131  bnj1021  35141  bnj1033  35144  bnj1047  35148  bnj1049  35149  bnj1090  35154  bnj1128  35165  bnj1175  35179  bnj1189  35184  bnj1253  35192  bnj1312  35233  exdifsn  35254  fineqvrep  35289  fineqvac  35291  onvf1odlem4  35319  vonf1owev  35321  erdszelem9  35412  erdszelem10  35413  pconnconn  35444  cvmliftiota  35514  fmlaomn0  35603  fmla0disjsuc  35611  fmlasucdisj  35612  dmopab3rexdif  35618  elmthm  35789  antnestALT  35907  nepss  35931  xpab  35939  dfso2  35968  elrn3  35975  elpotr  35992  dfon2lem5  35998  dfon2lem7  36000  dfon2lem8  36001  elwlim  36034  wzel  36035  brtxp2  36092  brpprod3a  36097  eltrans  36102  dfon3  36103  dffix2  36116  dffun10  36125  elfuns  36126  brsingle  36128  brimg  36148  funpartfun  36156  funpartfv  36158  cgrxfr  36268  segletr  36327  outsideoftr  36342  neifg  36584  filnetlem4  36594  df3nandALT1  36612  weiunlem  36676  bj-consensusALT  36801  bj-df-ifc  36802  bj-exexalal  36828  bj-cbvaew  36884  bj-biexal3  36949  bj-alnnf  36977  bj-nfnnfTEMP  37017  bj-denoteslem  37116  bj-denotesALTV  37117  bj-ralvw  37124  bj-rexvw  37125  bj-rexcom4bv  37127  bj-rexcom4b  37128  bj-sbeq  37146  bj-inrab  37172  bj-rcleqf  37270  bj-dfmpoa  37368  bj-imdirco  37442  topdifinffinlem  37599  topdifinfeq  37602  relowlssretop  37615  relowlpssretop  37616  rdgeqoa  37622  domalom  37656  nlpineqsn  37660  fvineqsneq  37664  wl-ifpimpr  37718  wl-df3xor3  37722  wl-3xorbi  37725  wl-3xorbi2  37726  wl-2xor  37735  wl-2mintru2  37743  wl-dfclab  37837  rabiun  37841  phpreu  37852  fin2solem  37854  matunitlindflem2  37865  ptrest  37867  poimirlem25  37893  poimirlem27  37895  poimirlem30  37898  ismblfin  37909  ovoliunnfl  37910  voliunnfl  37912  volsupnfl  37913  itg2addnclem2  37920  fdc  37993  prdstotbnd  38042  isdrngo1  38204  ispridl  38282  ismaxidl  38288  impor  38329  selconj  38348  tradd  38353  scott0f  38417  r2alan  38499  inxpss3  38568  idinxpssinxp2  38572  idinxpssinxp3  38573  dfrel5  38594  ineleq  38602  ralmo  38608  ralrnmo  38609  ralrmo3  38612  moantr  38620  dfxrn2  38633  inxpxrn  38666  rnxrnres  38670  dfsuccl4  38722  coss1cnvres  38755  1cossres  38767  cocossss  38774  cossssid4  38808  cossssid5  38809  cosscnvssid5  38816  cossid  38818  dfssr2  38827  cnvrefrelcoss2  38865  cosselcnvrefrels2  38866  eqvrelcoss  38949  eqvrelcoss2  38951  dfcoeleqvrel  38954  refrelredund4  38967  cnvepresdmqs  38986  dfcomember  39005  dfdisjALTV  39046  disjimdmqseq  39057  dfeldisj3  39059  dfeldisj4  39060  dfeldisj5  39061  disjres  39092  prter1  39252  islshp  39352  islshpat  39390  lcvbr2  39395  lcvnbtwn2  39400  cvrnbtwn3  39649  isatl  39672  ishlat1  39725  ishlat2  39726  cvrat4  39816  pmapglbx  40142  lhpexle3  40385  dib1dim  41538  diblsmopel  41544  lcfls1lem  41907  prjsperref  42961  prjspeclsp  42967  euabsn2w  43034  rexrabdioph  43148  dford4  43383  onsupuni  43583  dflim6  43618  tfsconcatlem  43690  naddgeoa  43748  ifpdfor2  43814  ifpdfan2  43816  ifpdfor  43818  ifpdfan  43819  ifpnot23b  43835  ifpnot23c  43837  ifpnot23d  43838  ifpim123g  43853  ifpbibib  43863  clss2lem  43964  imaiun1  44004  coiun1  44005  brfvrcld2  44045  iunrelexp0  44055  brtrclfv2  44080  snhesn  44139  dffrege76  44292  frege97  44313  frege98  44314  frege109  44325  frege110  44326  dffrege115  44331  frege131  44347  frege133  44349  ntrneineine1lem  44437  ntrneiel2  44439  ntrneiiso  44444  gneispace3  44486  scotteld  44599  ismnuprim  44647  ismnushort  44654  dfuniv2  44655  pm11.52  44740  pm11.58  44743  pm13.192  44763  impexpdcom  44868  sbc3or  44885  opelopab4  44904  uunT12p1  45152  uunT12p2  45153  uunT12p3  45154  uun2221  45165  uun2221p1  45166  uun2221p2  45167  undif3VD  45234  modelaxreplem3  45333  permaxext  45358  permac8prim  45367  ndisj2  45408  nssrex  45442  rabssf  45475  bothtbothsame  47256  bothfbothsame  47257  aiffbtbat  47265  reuabaiotaiota  47444  2reu8i  47470  2reuimp0  47471  ichn  47813  dfodd2  47993  dfeven5  48023  dfodd7  48024  1nevenALTV  48048  oddprmne2  48072  dfvopnbgr2  48210  isuspgrim0lem  48250  gpg5nbgrvtx03starlem1  48425  gpg5nbgrvtx03starlem2  48426  gpg5nbgrvtx03starlem3  48427  gpg5nbgrvtx13starlem1  48428  gpg5nbgrvtx13starlem2  48429  gpg5nbgrvtx13starlem3  48430  gpg5edgnedg  48487  islindeps2  48840  isldepslvec2  48842  line2xlem  49110  rmotru  49159  reutru  49160  isnrm4  49287  iscnrm4  49310  homf0  49365  fuco2el  49668  isthincd2  49793  thinccic  49827  istermc2  49831  istermc3  49832  dftermc3  49887  setrec1lem3  50045  aacllem  50157