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  642  mpbiran  709  biadaniALT  820  imor  853  imimorb  952  pm5.6  1003  nbi2  1017  casesifp  1077  3ancoma  1097  3ancomb  1098  3anrev  1100  dfnan2  1494  nannan  1497  nanbi  1500  xorcom  1514  xorneg  1523  xorbi12i  1524  norcom  1530  noran  1532  norasslem1  1534  trunortru  1589  trunorfal  1590  cadan  1609  cadcomb  1613  nic-ax  1673  nic-axALT  1674  nf3  1786  19.43  1882  equsv  2003  sbrimvw  2092  sbcom2  2174  sb5  2276  nf5  2282  nf6  2283  sbrim  2304  sbnf  2311  sb6x  2462  2sb5rf  2470  2sb6rf  2471  sb4b  2473  sb5f  2496  sbequ8  2499  sbhb  2519  eu6lem  2566  eu1  2603  iseqsetv-cleq  2793  issettru  2806  iseqsetv-clel  2807  issetlem  2808  cleqh  2857  cleqf  2920  sbabel  2924  necon3bii  2977  neor  3017  neorian  3020  rextru  3060  r19.26m  3088  r19.43  3097  3r19.43  3098  r2allem  3117  r19.23t  3225  ralcom4  3255  moel  3367  rabid2f  3428  eqv  3448  eqvf  3449  ralv  3465  rexv  3466  reuv  3467  rmov  3468  rexcom4b  3470  ceqsex4v  3495  ceqsex8v  3497  ceqsrexv  3612  rexab  3657  ralrab2  3660  rexrab2  3662  reu2  3687  reu3  3689  reueq  3699  2reuswap  3708  2reuswap2  3709  reuind  3715  2reu5lem3  3719  2rmoswap  3723  rmo2  3841  rmoanim  3848  rmoanimALT  3849  dfss3  3926  dfss3f  3929  ssabral  4019  rabss  4025  ssrabeq  4037  uniiunlem  4040  sspsstri  4058  npss  4066  dfdif3OLD  4071  raldifb  4102  uncom  4111  inass  4181  elsymdifxor  4213  nsspssun  4221  dfss4  4222  dfun2  4223  dfin2  4224  indi  4237  reupick3  4283  eq0f  4300  neq0f  4301  eq0  4303  eq0ALT  4304  dfnf5  4335  rabn0  4342  csbab  4393  vss  4399  disj  4403  disj3  4407  undisj1  4415  undisj2  4416  inundif  4432  undif  4435  undifr  4436  rabsssn  4622  exsnrex  4634  euabsn2  4679  euabsn  4680  raldifsni  4749  tppreqb  4759  pwpw0  4767  prssg  4773  ssunsn  4782  prneimg2  4809  preqsn  4816  pwpr  4855  dfuni2  4863  unissb  4893  elint2  4906  ssint  4917  uniintab  4939  dfiin2g  4984  iunid  5012  iunn0  5019  iunxun  5046  iunxiun  5049  iinpw  5058  disjor  5077  disjxiun  5092  dftr2  5204  dftr3  5207  dftr4  5208  axrep6OLD  5231  vnex  5256  inuni  5292  eusv2  5338  reusv2lem4  5343  rexxfr  5358  sspwb  5396  opthneg  5428  pwssun  5515  dfid3  5521  dffr6  5579  dffr2  5584  dffr2ALT  5585  opthprc  5687  elxp3  5689  xpiundir  5695  elvv  5698  reliun  5763  inxpOLD  5779  raliunxp  5786  cnvuni  5833  dmopab2rex  5864  dm0rn0  5871  dfres3  5939  ssdmres  5968  elidinxp  5999  idinxpres  6002  dfima2  6017  args  6047  dffr3  6054  cotrg  6064  intasym  6068  asymref  6069  intirr  6071  xpnz  6112  xp11  6128  ssrnres  6131  xpimasn  6138  coiun  6209  coass  6218  cnvso  6240  elsnxp  6243  dfpo2  6248  imaindm  6251  dffr4  6272  dfse3  6288  frpoind  6294  dflim2  6369  orddif  6409  dffun6  6497  dffun6f  6501  dffun7  6513  dffun9  6515  funfn  6516  svrelfun  6558  mptfnf  6621  dffn2  6658  dffn3  6668  fint  6707  dffn4  6746  dff1o4  6776  brprcneu  6816  brprcneuALT  6817  eqfnfv3  6971  fnreseql  6986  fsn  7073  ftpg  7094  abrexco  7184  imaiun  7185  dff13  7195  isof1oidb  7265  isof1oopb  7266  isocnv2  7272  eloprabga  7462  mpo2eqb  7485  elovmpo  7598  sorpss  7668  abexex  7913  elxp6  7965  elxp7  7966  releldm2  7985  opiota  8001  fnmpo  8011  frxp  8066  frxp2  8084  soseq  8099  cnvimadfsn  8112  mpoxneldm  8152  dftpos4  8185  frrlem9  8234  dfrecs3  8302  tfrlem7  8312  ondif1  8426  oarec  8487  oeeu  8528  brinxper  8661  0er  8670  eroveu  8746  erovlem  8747  elixpconst  8839  domen  8894  brsdom  8907  brdom2  8914  reuen1  8958  sbthlem10  9020  brsdom2  9025  xpf1o  9063  unfi  9095  sbthfilem  9122  onfin2  9140  0sdom1domALT  9146  modom  9150  marypha2lem3  9346  wemapsolem  9461  elom3  9563  dfom5  9565  brttrcl2  9629  ttrcltr  9631  ttrclse  9642  trcl  9643  epfrs  9646  frind  9665  rankf  9709  scottexs  9802  scott0s  9803  cplem1  9804  hta  9812  djuexb  9824  pm54.43lem  9915  alephsuc2  9993  iscard3  10006  aceq0  10031  aceq3lem  10033  dfac3  10034  dfac5lem2  10037  dfac5  10042  dfac7  10046  dfac12a  10062  kmlem12  10075  kmlem14  10077  kmlem15  10078  infmap2  10130  ackbij2  10155  dfacfin7  10312  ituniiun  10335  zorng  10417  brdom7disj  10444  entri2  10471  alephreg  10495  fpwwe2lem11  10554  fpwwe2lem12  10555  pwfseqlem1  10571  grutsk  10735  axgroth4  10745  grothprim  10747  grothtsk  10748  elni2  10790  ltsopi  10801  genpass  10922  psslinpr  10944  ltexprlem4  10952  ltresr  11053  infm3  12102  elnnz  12499  dfz2  12508  2rexuz  12819  nnwos  12834  eluz2b1  12838  qexALT  12883  elxr  13036  dflt2  13068  xrsupss  13229  xrinfmss  13230  elixx1  13275  elioo2  13307  dfrp2  13315  elioopnf  13364  elicopnf  13366  elfz1  13433  fznn  13513  fzp1nel  13532  fznn0  13540  preduz  13571  prinfzo0  13619  injresinj  13709  nn0opthlem1  14193  faclbnd4lem1  14218  hashfxnn0  14262  hashprdifel  14323  hashgt23el  14349  hashfun  14362  hashf1  14382  fz1isolem  14386  f1oun2prg  14842  brtrclfv  14927  shftdm  14996  rediv  15056  imdiv  15063  rexanre  15272  caubnd  15284  climreu  15481  prodmo  15861  dvdslelem  16238  3dvdsdec  16261  3dvds2dec  16262  bitsval  16353  smueqlem  16419  algcvgblem  16506  lcmfunsnlem2  16569  isprm2  16611  isprm3  16612  isprm4  16613  pythagtriplem2  16747  elgz  16861  hashbc0  16935  0ram  16950  isstruct  17081  issect  17678  isfull2  17838  isfth2  17842  fucinv  17901  eldmcoa  17990  isdrs  18225  submacs  18719  isnsg4  19064  isgim  19159  gaorb  19204  oppgid  19253  oppgsubm  19259  oppgcntz  19261  ispgp  19489  efgsdm  19627  efgcpbllema  19651  iscyg2  19779  isomnd  20020  omndmul2  20030  isrng  20057  isring  20140  isirred2  20324  opprirred  20325  isrnghm  20344  dfrhm2  20377  isnzr2  20421  opprsubrng  20462  opprsubrg  20496  isdomn3  20618  drngid2  20655  issdrg  20691  islmod  20785  lss1d  20884  islmhm  20949  islmim  20984  lbsextlem2  21084  lidlnz  21167  dfprm2  21398  isphl  21553  elocv  21593  iunocv  21606  isobs  21645  islinds  21734  1mavmul  22451  toprntopon  22828  isbasis3g  22852  fctop  22907  cctop  22909  isclo2  22991  restsn  23073  lmbr  23161  ist0-3  23248  2ndcdisj  23359  1stccnp  23365  islocfin  23420  1stckgenlem  23456  txbas  23470  ptbasin  23480  tx2cn  23513  fbfinnfr  23744  fbasrn  23787  filuni  23788  ufinffr  23832  fin1aufil  23835  rnelfmlem  23855  flimrest  23886  alexsubALTlem3  23952  alexsubALTlem4  23953  tgphaus  24020  istlm  24088  iscusp2  24205  metuel2  24469  isngp2  24501  isnlm  24579  isphtpc  24909  phtpcer  24910  om1elbas  24948  isclm  24980  iscvsp  25044  iscph  25086  iscau3  25194  minveclem3b  25344  elovolm  25392  ioombl1lem4  25478  dyaddisj  25513  vitali  25530  itg1climres  25631  itg2seq  25659  itg2monolem1  25667  itg2mono  25670  limcrcl  25791  lhop1  25935  itgsubst  25972  mdegleb  25985  isuc1p  26062  ismon1p  26064  plydivex  26221  ellogdm  26564  1cubr  26768  atandm2  26803  birthdaylem3  26879  dmarea  26883  dchrelbas2  27164  dchrelbas4  27170  elno3  27583  nosgnn0  27586  nosepon  27593  nocvxminlem  27706  scutcut  27730  scutbday  27733  dmscut  27740  scutf  27741  sltrec  27750  made0  27805  addsprop  27906  negsproplem2  27958  negsprop  27964  mulsprop  28056  precsexlem10  28141  elzs2  28310  elnnzs  28312  recut  28383  0reno  28384  axcontlem7  28933  nb3grpr  29345  nb3grpr2  29346  upgrwlkcompim  29606  wlkson  29618  wlkonprop  29620  wksonproplem  29666  ispth  29684  wwlknon  29820  wwlksnextinj  29862  wspthsnwspthsnon  29879  elwspths2spth  29930  rusgrnumwwlkl1  29931  clwwlkccatlem  29951  erclwwlkref  29982  frgr3v  30237  nmoubi  30734  nmobndseqi  30741  nmobndseqiALT  30742  minvecolem1  30836  isch2  31185  hlimreui  31201  isch3  31203  ocsh  31245  dfch2  31369  spanuni  31506  nonbooli  31613  5oalem7  31622  adjsym  31795  elbdop2  31833  dmadjss  31849  nmopub  31870  nmfnleub  31887  nmop0h  31953  pjssposi  32134  pjordi  32135  cvbr2  32245  cvnbtwn2  32249  mdsl2i  32284  cvmdi  32286  elat2  32302  atom1d  32315  chirredi  32356  cdj3i  32403  or3di  32421  opreu2reu1  32446  mo5f  32451  reuxfrdf  32453  rexunirn  32454  difrab2  32460  rabsspr  32463  rabsstp  32464  tpssg  32499  iuninc  32522  disjorf  32541  disjunsn  32556  rabfmpunirn  32610  aciunf1  32620  funcnv5mpt  32625  eliccelico  32733  elicoelioo  32734  isslmd  33154  islinds5  33314  ismxidl  33409  1arithufdlem4  33494  hasheuni  34051  pwsiga  34096  sigainb  34102  issros  34141  2ndmbfm  34228  omssubaddlem  34266  omssubadd  34267  sitgaddlemb  34315  eulerpartlemgvv  34343  eulerpartlemn  34348  probun  34386  ballotlem2  34456  ballotlemodife  34465  bnj252  34669  bnj253  34670  bnj255  34671  bnj345  34680  bnj133  34693  bnj976  34743  bnj1098  34749  bnj121  34836  bnj130  34840  bnj150  34842  bnj581  34874  bnj607  34882  bnj865  34889  bnj917  34900  bnj934  34901  bnj964  34909  bnj983  34917  bnj996  34922  bnj1021  34932  bnj1033  34935  bnj1047  34939  bnj1049  34940  bnj1090  34945  bnj1128  34956  bnj1175  34970  bnj1189  34975  bnj1253  34983  bnj1312  35024  exdifsn  35045  fineqvrep  35069  fineqvac  35071  onvf1odlem4  35078  vonf1owev  35080  erdszelem9  35171  erdszelem10  35172  pconnconn  35203  cvmliftiota  35273  fmlaomn0  35362  fmla0disjsuc  35370  fmlasucdisj  35371  dmopab3rexdif  35377  elmthm  35548  antnestALT  35666  nepss  35690  xpab  35698  dfso2  35727  elrn3  35734  elpotr  35754  dfon2lem5  35760  dfon2lem7  35762  dfon2lem8  35763  elwlim  35796  wzel  35797  brtxp2  35854  brpprod3a  35859  eltrans  35864  dfon3  35865  dffix2  35878  dffun10  35887  elfuns  35888  brsingle  35890  brimg  35910  funpartfun  35916  funpartfv  35918  cgrxfr  36028  segletr  36087  outsideoftr  36102  neifg  36344  filnetlem4  36354  df3nandALT1  36372  weiunlem2  36436  bj-consensusALT  36552  bj-df-ifc  36553  bj-biexal3  36680  bj-nfnnfTEMP  36731  bj-denoteslem  36844  bj-denotesALTV  36845  bj-ralvw  36852  bj-rexvw  36853  bj-rexcom4bv  36855  bj-rexcom4b  36856  bj-sbeq  36874  bj-inrab  36900  bj-rcleqf  36998  bj-dfmpoa  37091  bj-imdirco  37163  topdifinffinlem  37320  topdifinfeq  37323  relowlssretop  37336  relowlpssretop  37337  rdgeqoa  37343  domalom  37377  nlpineqsn  37381  fvineqsneq  37385  wl-ifpimpr  37439  wl-df3xor3  37443  wl-3xorbi  37446  wl-3xorbi2  37447  wl-2xor  37456  wl-2mintru2  37464  wl-dfclab  37569  rabiun  37572  phpreu  37583  fin2solem  37585  matunitlindflem2  37596  ptrest  37598  poimirlem25  37624  poimirlem27  37626  poimirlem30  37629  ismblfin  37640  ovoliunnfl  37641  voliunnfl  37643  volsupnfl  37644  itg2addnclem2  37651  fdc  37724  prdstotbnd  37773  isdrngo1  37935  ispridl  38013  ismaxidl  38019  impor  38060  selconj  38079  tradd  38084  scott0f  38148  r2alan  38223  inxpss3  38287  idinxpssinxp2  38291  idinxpssinxp3  38292  dfrel5  38313  ineleq  38321  moantr  38331  dfxrn2  38343  inxpxrn  38366  rnxrnres  38370  coss1cnvres  38393  1cossres  38405  cocossss  38412  cossssid4  38446  cossssid5  38447  cosscnvssid5  38454  cossid  38456  dfssr2  38475  cnvrefrelcoss2  38513  cosselcnvrefrels2  38514  eqvrelcoss  38593  eqvrelcoss2  38595  dfcoeleqvrel  38598  refrelredund4  38611  cnvepresdmqs  38630  dfcomember  38649  dfdisjALTV  38690  dfeldisj3  38696  dfeldisj4  38697  dfeldisj5  38698  disjres  38721  prter1  38857  islshp  38957  islshpat  38995  lcvbr2  39000  lcvnbtwn2  39005  cvrnbtwn3  39254  isatl  39277  ishlat1  39330  ishlat2  39331  cvrat4  39422  pmapglbx  39748  lhpexle3  39991  dib1dim  41144  diblsmopel  41150  lcfls1lem  41513  prjsperref  42579  prjspeclsp  42585  euabsn2w  42652  rexrabdioph  42767  dford4  43002  onsupuni  43202  dflim6  43237  tfsconcatlem  43309  naddgeoa  43367  ifpdfor2  43434  ifpdfan2  43436  ifpdfor  43438  ifpdfan  43439  ifpnot23b  43455  ifpnot23c  43457  ifpnot23d  43458  ifpim123g  43473  ifpbibib  43483  clss2lem  43584  imaiun1  43624  coiun1  43625  brfvrcld2  43665  iunrelexp0  43675  brtrclfv2  43700  snhesn  43759  dffrege76  43912  frege97  43933  frege98  43934  frege109  43945  frege110  43946  dffrege115  43951  frege131  43967  frege133  43969  ntrneineine1lem  44057  ntrneiel2  44059  ntrneiiso  44064  gneispace3  44106  scotteld  44219  ismnuprim  44267  ismnushort  44274  dfuniv2  44275  pm11.52  44360  pm11.58  44363  pm13.192  44383  impexpdcom  44489  sbc3or  44506  opelopab4  44525  uunT12p1  44773  uunT12p2  44774  uunT12p3  44775  uun2221  44786  uun2221p1  44787  uun2221p2  44788  undif3VD  44855  modelaxreplem3  44954  permaxext  44979  permac8prim  44988  ndisj2  45029  nssrex  45064  rabssf  45097  bothtbothsame  46884  bothfbothsame  46885  aiffbtbat  46893  reuabaiotaiota  47072  2reu8i  47098  2reuimp0  47099  ichn  47441  dfodd2  47621  dfeven5  47651  dfodd7  47652  1nevenALTV  47676  oddprmne2  47700  dfvopnbgr2  47838  isuspgrim0lem  47878  gpg5nbgrvtx03starlem1  48053  gpg5nbgrvtx03starlem2  48054  gpg5nbgrvtx03starlem3  48055  gpg5nbgrvtx13starlem1  48056  gpg5nbgrvtx13starlem2  48057  gpg5nbgrvtx13starlem3  48058  gpg5edgnedg  48115  islindeps2  48469  isldepslvec2  48471  line2xlem  48739  rmotru  48788  reutru  48789  isnrm4  48916  iscnrm4  48939  homf0  48995  fuco2el  49298  isthincd2  49423  thinccic  49457  istermc2  49461  istermc3  49462  dftermc3  49517  setrec1lem3  49675  aacllem  49787