Theorem bitr4i 281

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 227	. 2 ⊢ (𝜓 ↔ 𝜒)
4	1, 3	bitri 278	1 ⊢ (𝜑 ↔ 𝜒)

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  3bitr2i  302  3bitr2ri  303  3bitr4i  306  3bitr4ri  307  biluk  389  biancomi  467  dfbi2  479  imdistan  577  pm5.32  583  bianass  654  mpbiran  721  biadaniALT  832  imor  866  imimorb  965  pm5.6  1017  nbi2  1033  ifpdfbi  1086  casesifp  1094  3ancoma  1115  3ancomb  1116  3anrev  1118  4anpull2  1382  dfnan2  1524  nannan  1527  nanbi  1530  xorcom  1544  xorneg  1553  xorbi12i  1554  norcom  1560  noran  1562  norasslem1  1564  trunortru  1619  trunorfal  1620  cadan  1639  cadcomb  1643  nic-ax  1703  nic-axALT  1704  nf3  1816  19.43  1912  equsv  2033  sbrimvwOLD  2126  sbcom2  2207  sb5  2311  nf5  2317  nf6  2318  sbrim  2339  sbnf  2346  sb6x  2496  2sb5rf  2504  2sb6rf  2505  sb4b  2507  sb5f  2530  sbequ8  2533  sbhb  2553  eu6lem  2601  eu1  2638  iseqsetv-cleq  2827  issettru  2841  iseqsetv-clel  2842  issetlem  2843  cleqh  2892  cleqf  2953  sbabel  2957  necon3bii  3010  neor  3050  neorian  3053  rextru  3096  r19.26m  3124  r19.43  3133  3r19.43  3134  r2allem  3153  r19.23t  3261  ralcom4  3291  moel  3389  rabid2f  3447  eqv  3465  eqvf  3466  ralv  3481  rexv  3482  reuv  3483  rmov  3484  rexcom4b  3486  ceqsex4v  3508  ceqsex8v  3510  ceqsrexv  3615  rexab  3659  ralrab2  3662  rexrab2  3664  reu2  3689  reu3  3691  reueq  3701  2reuswap  3710  2reuswap2  3711  reuind  3717  2reu5lem3  3721  2rmoswap  3725  rmo2  3841  rmoanim  3849  rmoanimALT  3850  dfss3  3927  dfss3f  3930  nssrex  4003  ssabral  4019  rabss  4025  ssrabeq  4039  uniiunlem  4042  sspsstri  4061  npss  4069  dfdif3OLD  4074  raldifb  4104  uncom  4113  inass  4181  elsymdifxor  4214  nsspssun  4222  dfss4  4223  dfun2  4224  dfin2  4225  indi  4238  reupick3  4284  eq0f  4302  neq0f  4303  eq0ALT  4306  inssdif0  4330  dfnf5  4339  rabn0  4347  vss  4366  csbab  4406  disj  4411  disj3  4415  undisj1  4423  undisj2  4424  inundif  4441  undif  4444  undifr  4445  rabsssn  4635  exsnrex  4647  euabsn2  4692  euabsn  4693  raldifsni  4764  tppreqb  4774  pwpw0  4780  prssg  4786  ssunsn  4795  prneimg2  4821  preqsn  4828  pwpr  4867  dfuni2  4875  unissb  4907  elint2  4920  ssint  4930  uniintab  4952  dfiin2g  4996  iunid  5026  iunn0  5032  iunxun  5061  iunxiun  5064  iinpw  5073  disjor  5092  disjxiun  5107  dftr2  5221  dftr3  5224  dftr4  5225  axrep6OLD  5249  vnexOLD  5282  inuni  5322  eusv2  5369  reusv2lem4  5374  rexxfr  5389  sspwb  5432  opthneg  5465  pwssun  5555  dfid3  5561  dffr6  5619  dffr2  5624  dffr2ALT  5625  opthprc  5727  elxp3  5729  xpiundir  5735  elvv  5738  raliunxp  5827  cnvuni  5878  dmopab2rex  5909  dm0rn0OLD  5917  dfres3  5985  ssdmres  6014  elidinxp  6048  idinxpres  6051  dfima2  6066  args  6096  dffr3  6103  cotrg  6113  intasym  6117  asymref  6118  intirr  6120  xpnz  6158  xp11  6175  ssrnres  6178  xpimasn  6185  coiun  6260  coass  6269  cnvso  6291  elsnxp  6294  dfpo2  6299  imaindm  6302  dffr4  6323  dfse3  6339  frpoind  6345  dflim2  6421  orddif  6461  dffun6  6549  dffun6f  6553  dffun7  6565  dffun9  6567  funfn  6568  svrelfun  6610  mptfnf  6672  dffn2  6709  dffn3  6720  fint  6759  dffn4  6800  dff1o4  6831  brprcneu  6873  brprcneuALT  6874  eqfnfv3  7029  fnreseql  7045  fsn  7133  ftpg  7155  abrexco  7244  imaiun  7245  dff13  7254  isof1oidb  7324  isof1oopb  7325  isocnv2  7331  eloprabga  7521  mpo2eqb  7544  elovmpo  7657  sorpss  7727  abexex  7969  elxp6  8021  elxp7  8022  releldm2  8041  opiota  8057  fnmpo  8067  frxp  8123  frxp2  8141  soseq  8156  cnvimadfsn  8169  mpoxneldm  8209  dftpos4  8242  frrlem9  8292  dfrecs3  8360  tfrlem7  8371  ondif1  8487  oarec  8548  oeeu  8590  brinxper  8725  0er  8734  eroveu  8811  erovlem  8812  elixpconst  8904  domen  8959  brsdom  8972  brdom2  8980  reuen1  9024  sbthlem10  9085  brsdom2  9090  xpf1o  9128  unfi  9156  sbthfilem  9183  onfin2  9202  0sdom1domALT  9208  modom  9212  marypha2lem3  9398  wemapsolem  9513  elom3  9618  dfom5  9620  brttrcl2  9684  ttrcltr  9686  ttrclse  9697  trcl  9698  epfrs  9701  frind  9723  rankf  9767  scottexs  9862  scott0s  9863  scotteld  9873  cplem1  9876  hta  9884  djuexb  9896  pm54.43lem  9987  alephsuc2  10065  iscard3  10078  aceq0  10103  aceq3lem  10105  dfac3  10106  dfac5lem2  10109  dfac5  10113  dfac7  10117  dfac12a  10133  kmlem12  10146  kmlem14  10148  kmlem15  10149  infmap2  10201  ackbij2  10226  dfacfin7  10384  ituniiun  10407  zorng  10489  brdom7disj  10516  entri2  10543  alephreg  10568  fpwwe2lem11  10627  fpwwe2lem12  10628  pwfseqlem1  10644  grutsk  10808  axgroth4  10818  grothprim  10820  grothtsk  10821  elni2  10863  ltsopi  10874  genpass  10995  psslinpr  11017  ltexprlem4  11025  ltresr  11126  infm3  12175  elnnz  12602  dfz2  12611  2rexuz  12925  nnwos  12940  eluz2b1  12944  qexALT  12989  elxr  13142  dflt2  13174  xrsupss  13336  xrinfmss  13337  elixx1  13382  elioo2  13414  dfrp2  13422  elioopnf  13471  elicopnf  13473  elfz1  13541  fznn  13622  fzp1nel  13641  fznn0  13649  preduz  13680  prinfzo0  13729  injresinj  13822  nn0opthlem1  14306  faclbnd4lem1  14331  hashfxnn0  14375  hashprdifel  14436  hashgt23el  14463  hashfun  14476  hashf1  14496  fz1isolem  14500  f1oun2prg  14956  brtrclfv  15041  shftdm  15110  rediv  15184  imdiv  15191  rexanre  15400  caubnd  15412  climreu  15609  prodmo  15992  dvdslelem  16368  3dvdsdec  16391  3dvds2dec  16392  bitsval  16483  smueqlem  16549  algcvgblem  16636  lcmfunsnlem2  16699  isprm2  16741  isprm3  16742  isprm4  16743  pythagtriplem2  16878  elgz  16992  hashbc0  17066  0ram  17081  isstruct  17213  issect  17811  isfull2  17971  isfth2  17975  fucinv  18034  eldmcoa  18123  isdrs  18358  submacs  18887  isnsg4  19234  isgim  19333  gaorb  19378  oppgid  19427  oppgsubm  19433  oppgcntz  19435  ispgp  19663  efgsdm  19801  efgcpbllema  19825  iscyg2  19953  isomnd  20194  omndmul2  20204  isrng  20233  isring  20320  isirred2  20504  opprirred  20505  isrnghm  20524  dfrhm2  20557  isnzr2  20602  opprsubrng  20645  opprsubrg  20679  isdomn3  20800  drngid2  20838  issdrg  20872  islmod  20966  lss1d  21065  islmhm  21129  islmim  21164  lbsextlem2  21264  lidlnz  21357  dfprm2  21604  isphl  21759  elocv  21799  iunocv  21812  isobs  21851  islinds  21940  1mavmul  22686  toprntopon  23063  isbasis3g  23087  fctop  23142  cctop  23144  isclo2  23226  restsn  23308  lmbr  23396  ist0-3  23483  2ndcdisj  23594  1stccnp  23600  islocfin  23655  1stckgenlem  23691  txbas  23705  ptbasin  23715  tx2cn  23748  fbfinnfr  23979  fbasrn  24022  filuni  24023  ufinffr  24067  fin1aufil  24070  rnelfmlem  24090  flimrest  24121  alexsubALTlem3  24187  alexsubALTlem4  24188  tgphaus  24255  istlm  24323  iscusp2  24439  metuel2  24703  isngp2  24735  isnlm  24813  isphtpc  25134  phtpcer  25135  om1elbas  25172  isclm  25204  iscvsp  25268  iscph  25310  iscau3  25418  minveclem3b  25568  elovolm  25615  ioombl1lem4  25701  dyaddisj  25736  vitali  25753  itg1climres  25854  itg2seq  25882  itg2monolem1  25890  itg2mono  25893  limcrcl  26014  lhop1  26154  itgsubst  26189  mdegleb  26202  isuc1p  26279  ismon1p  26281  plydivex  26439  ellogdm  26785  1cubr  26988  atandm2  27023  birthdaylem3  27099  dmarea  27103  dchrelbas2  27382  dchrelbas4  27388  elno3  27800  nosgnn0  27803  nosepon  27810  nocvxminlem  27928  cutcuts  27955  cutbday  27958  dmcuts  27965  cutsf  27966  ltsrec  27975  made0  28037  addsprop  28150  negsproplem2  28203  negsprop  28209  mulsprop  28304  precsexlem10  28390  elzs2  28573  elnnzs  28575  bdayfinbndlem1  28641  recut  28668  axcontlem7  29301  nb3grpr  29713  nb3grpr2  29714  upgrwlkcompim  29973  wlkson  29985  wlkonprop  29987  wksonproplem  30033  ispth  30051  wwlknon  30187  wwlksnextinj  30229  wspthsnwspthsnon  30246  elwspths2spth  30300  rusgrnumwwlkl1  30301  clwwlkccatlem  30321  erclwwlkref  30352  frgr3v  30607  nmoubi  31105  nmobndseqi  31112  nmobndseqiALT  31113  minvecolem1  31207  isch2  31556  hlimreui  31572  isch3  31574  ocsh  31616  dfch2  31740  spanuni  31877  nonbooli  31984  5oalem7  31993  adjsym  32166  elbdop2  32204  dmadjss  32220  nmopub  32241  nmfnleub  32258  nmop0h  32324  pjssposi  32505  pjordi  32506  cvbr2  32616  cvnbtwn2  32620  mdsl2i  32655  cvmdi  32657  elat2  32673  atom1d  32686  chirredi  32727  cdj3i  32774  or3di  32788  opreu2reu1  32811  mo5f  32816  reuxfrdf  32818  rexunirn  32819  difrab2  32825  rabsspr  32828  rabsstp  32829  tpssg  32864  iuninc  32886  disjorf  32905  disjunsn  32920  rabfmpunirn  32979  aciunf1  32989  funcnv5mpt  32993  eliccelico  33103  elicoelioo  33104  isslmd  33503  islinds5  33663  ismxidl  33726  1arithufdlem4  33818  hasheuni  34456  pwsiga  34501  sigainb  34507  issros  34546  2ndmbfm  34632  omssubaddlem  34670  omssubadd  34671  sitgaddlemb  34719  eulerpartlemgvv  34747  eulerpartlemn  34752  probun  34790  ballotlem2  34860  ballotlemodife  34869  bnj252  35073  bnj253  35074  bnj255  35075  bnj345  35084  bnj133  35097  bnj976  35147  bnj1098  35153  bnj121  35239  bnj130  35243  bnj150  35245  bnj581  35277  bnj607  35285  bnj865  35292  bnj917  35303  bnj934  35304  bnj964  35312  bnj983  35320  bnj996  35325  bnj1021  35335  bnj1033  35338  bnj1047  35342  bnj1049  35343  bnj1090  35348  bnj1128  35359  bnj1175  35373  bnj1189  35378  bnj1253  35386  bnj1312  35427  exdifsn  35449  scott0b  35502  fineqvrep  35508  fineqvac  35510  kard0  35548  kardexen  35557  onvf1odlem4  35571  vonf1wev  35573  vonf1owevOLD  35575  vonf1osev  35577  erdszelem9  35672  erdszelem10  35673  pconnconn  35704  cvmliftiota  35774  fmlaomn0  35863  fmla0disjsuc  35871  fmlasucdisj  35872  dmopab3rexdif  35878  elmthm  36049  antnestALT  36167  nepss  36191  xpab  36199  dfso2  36228  elrn3  36235  elpotr  36252  dfon2lem5  36258  dfon2lem7  36260  dfon2lem8  36261  elwlim  36294  wzel  36295  brtxp2  36352  brpprod3a  36357  eltrans  36362  dfon3  36363  dffix2  36376  dffun10  36385  elfuns  36386  brsingle  36388  brimg  36408  funpartfun  36416  funpartfv  36418  cgrxfr  36528  segletr  36587  outsideoftr  36602  naddle  36677  neifg  36863  filnetlem4  36873  df3nandALT1  36891  weiunlem  36955  ttcwf3  37018  bj-consensusALT  37153  bj-df-ifc  37154  bj-exexalal  37180  bj-cbvaew  37247  bj-biexal3  37313  bj-alnnf  37343  bj-nfnnfTEMP  37388  bj-denoteslem  37487  bj-denotesALTV  37488  bj-ralvw  37495  bj-rexvw  37496  bj-rexcom4bv  37498  bj-rexcom4b  37499  bj-sbeq  37517  bj-inrab  37544  bj-rcleqf  37642  bj-dfmpoa  37741  bj-imdirco  37815  topdifinffinlem  37974  topdifinfeq  37977  relowlssretop  37990  relowlpssretop  37991  rdgeqoa  37997  domalom  38031  nlpineqsn  38035  fvineqsneq  38039  wl-ifpimpr  38093  wl-df3xor3  38097  wl-3xorbi  38100  wl-3xorbi2  38101  wl-2xor  38110  wl-2mintru2  38118  wl-dfclab  38221  rabiun  38225  phpreu  38236  fin2solem  38238  matunitlindflem2  38249  ptrest  38251  poimirlem25  38277  poimirlem27  38279  poimirlem30  38282  ismblfin  38293  ovoliunnfl  38294  voliunnfl  38296  volsupnfl  38297  itg2addnclem2  38304  fdc  38377  prdstotbnd  38426  isdrngo1  38588  ispridl  38666  ismaxidl  38672  impor  38713  selconj  38730  tradd  38735  scott0f  38799  r2alan  38881  inxpss3  38950  idinxpssinxp2  38954  idinxpssinxp3  38955  dfrel5  38976  ineleq  38984  ralmo  38990  ralrnmo  38991  ralrmo3  38994  moantr  39002  dfxrn2  39015  inxpxrn  39048  rnxrnres  39052  dfsuccl4  39104  coss1cnvres  39137  1cossres  39149  cocossss  39156  cossssid4  39190  cossssid5  39191  cosscnvssid5  39198  cossid  39200  dfssr2  39209  cnvrefrelcoss2  39247  cosselcnvrefrels2  39248  eqvrelcoss  39331  eqvrelcoss2  39333  dfcoeleqvrel  39336  refrelredund4  39349  cnvepresdmqs  39368  dfcomember  39387  dfdisjALTV  39428  disjimdmqseq  39439  dfeldisj3  39441  dfeldisj4  39442  dfeldisj5  39443  disjres  39474  prter1  39634  islshp  39734  islshpat  39772  lcvbr2  39777  lcvnbtwn2  39782  cvrnbtwn3  40031  isatl  40054  ishlat1  40107  ishlat2  40108  cvrat4  40198  pmapglbx  40524  lhpexle3  40767  dib1dim  41920  diblsmopel  41926  lcfls1lem  42289  prjsperref  43321  prjspeclsp  43327  euabsn2w  43394  rexrabdioph  43504  dford4  43739  onsupuni  43939  dflim6  43974  tfsconcatlem  44046  naddgeoa  44104  ifpdfor2  44170  ifpdfan2  44172  ifpdfor  44174  ifpdfan  44175  ifpnot23b  44191  ifpnot23c  44193  ifpnot23d  44194  ifpim123g  44209  ifpbibib  44219  clss2lem  44320  imaiun1  44360  coiun1  44361  brfvrcld2  44401  iunrelexp0  44411  brtrclfv2  44436  snhesn  44495  dffrege76  44648  frege97  44669  frege98  44670  frege109  44681  frege110  44682  dffrege115  44687  frege131  44703  frege133  44705  ntrneineine1lem  44793  ntrneiel2  44795  ntrneiiso  44800  gneispace3  44842  ismnuprim  44987  ismnushort  44994  dfuniv2  44995  pm11.52  45080  pm11.58  45083  pm13.192  45103  impexpdcom  45207  sbc3or  45224  opelopab4  45243  uunT12p1  45491  uunT12p2  45492  uunT12p3  45493  uun2221  45504  uun2221p1  45505  uun2221p2  45506  undif3VD  45573  modelaxreplem3  45672  permaxext  45697  permac8prim  45706  ndisj2  45754  rabssf  45820  bothtbothsame  47619  bothfbothsame  47620  aiffbtbat  47628  reuabaiotaiota  47807  2reu8i  47833  2reuimp0  47834  ichn  48188  dfodd2  48384  dfeven5  48414  dfodd7  48415  1nevenALTV  48439  oddprmne2  48463  dfvopnbgr2  48601  isuspgrim0lem  48641  gpg5nbgrvtx03starlem1  48816  gpg5nbgrvtx03starlem2  48817  gpg5nbgrvtx03starlem3  48818  gpg5nbgrvtx13starlem1  48819  gpg5nbgrvtx13starlem2  48820  gpg5nbgrvtx13starlem3  48821  gpg5edgnedg  48878  dfidom2  49091  islindeps2  49246  isldepslvec2  49248  line2xlem  49516  rmotru  49564  reutru  49565  isnrm4  49692  iscnrm4  49715  homf0  49770  fuco2el  50073  isthincd2  50198  thinccic  50232  istermc2  50236  istermc3  50237  dftermc3  50292  setrec1lem3  50450  dfrals2  50551  aacllem  50584