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  390  biancomi  466  dfbi2  478  imdistan  571  pm5.32  577  bianass  642  mpbiran  709  biadaniALT  821  imor  853  imimorb  951  pm5.6  1002  nbi2  1016  casesifp  1079  3ancoma  1100  3ancomb  1101  3anrev  1103  an3andi  1484  dfnan2  1490  nannan  1493  nanbi  1496  xorcom  1510  xorneg  1520  xorbi12i  1521  norcom  1528  noran  1532  norasslem1  1536  norassOLD  1540  trunortru  1592  trunorfal  1594  cadan  1616  cadcomb  1620  nic-ax  1681  nic-axALT  1682  nf3  1794  nfnbiOLD  1863  19.43  1890  equsv  2012  sbrimvlem  2099  sbcom2  2167  sb5  2274  nf5  2285  nf6  2286  sb6x  2463  2sb5rf  2471  2sb6rf  2472  sb4b  2474  sb4bOLD  2475  sb5f  2501  sbequ8  2504  sbhb  2524  eu6lem  2572  eu1  2611  elisset  2812  cleqh  2854  clelabOLD  2874  cleqf  2928  necon3bii  2984  neor  3023  neorian  3026  r19.26-3  3084  r19.26m  3085  r2allem  3111  r19.23t  3222  r19.43  3254  rexcom  3258  rabid2  3283  rabid2f  3284  moel  3325  eqv  3407  eqvf  3408  isset  3411  ralv  3422  rexv  3423  reuv  3424  rmov  3425  rexcom4b  3427  ceqsex4v  3451  ceqsex8v  3453  ceqsrexv  3553  ralrab2  3601  rexrab2  3604  reu2  3627  reu3  3629  reueq  3639  2reuswap  3648  2reuswap2  3649  reuind  3655  2reu5lem3  3659  2rmoswap  3663  sbc3an  3752  rmo2  3786  rmoanim  3793  rmoanimALT  3794  dfss2  3873  dfss2OLD  3874  dfss3  3875  dfss3f  3878  ssabral  3962  rabss  3971  ssrabeq  3983  uniiunlem  3985  sspsstri  4003  npss  4011  dfdif3  4015  raldifb  4045  uncom  4053  inass  4120  elsymdifxor  4150  nsspssun  4158  dfss4  4159  dfun2  4160  dfin2  4161  indi  4174  indifdirOLD  4186  difin2  4192  reupick3  4220  eq0f  4241  neq0f  4242  eq0  4244  eq0ALT  4245  dfnf5  4278  rabn0  4286  csbab  4338  vss  4344  disj  4348  disjOLD  4349  disj3  4354  undisj1  4362  undisj2  4363  inundif  4379  undif  4382  absn  4545  rabsssn  4569  exsnrex  4582  euabsn2  4627  euabsn  4628  raldifsni  4694  tppreqb  4704  pwpw0  4712  prssg  4718  ssunsn  4727  preqsn  4758  pwpr  4799  dfuni2  4807  unissb  4839  elint2  4852  ssint  4861  uniintab  4885  dfiin2g  4927  iunn0  4961  iunxun  4988  iunxiun  4991  iinpw  5000  disjor  5019  disjxiun  5036  dftr2  5148  dftr5  5149  dftr3  5150  dftr4  5151  axrep6  5171  vnex  5192  inuni  5221  eusv2  5274  reusv2lem4  5279  rexxfr  5294  snelpw  5315  sspwb  5319  opthneg  5350  pwssun  5436  dfid3  5442  dffr2  5500  dffr2ALT  5501  opthprc  5598  elxp3  5600  xpiundir  5605  elvv  5608  reliun  5671  inxp  5686  raliunxp  5693  cnvuni  5740  dmopab2rex  5771  dm0rn0  5779  dfres3  5841  ssdmres  5859  elidinxp  5896  idinxpres  5899  dfima2  5916  args  5942  dffr3  5947  cotrg  5956  intasym  5960  asymref  5961  intirr  5963  xpnz  6002  xp11  6018  ssrnres  6021  xpimasn  6028  coiun  6100  coass  6109  cnvso  6131  elsnxp  6134  dffr4  6156  frpoind  6174  wfi  6181  dflim2  6247  orddif  6284  dffun2  6368  dffun6f  6372  dffun7  6385  dffun9  6387  funfn  6388  svrelfun  6430  mptfnf  6491  dffn2  6525  dffn3  6536  fint  6576  dffn4  6617  dff1o4  6647  brprcneu  6686  fvprc  6687  eqfnfv3  6832  fnreseql  6846  fsn  6928  ftpg  6949  abrexco  7035  imaiun  7036  dff13  7045  isof1oidb  7111  isof1oopb  7112  isocnv2  7118  eloprabga  7296  mpo2eqb  7320  elovmpo  7428  sorpss  7494  abexex  7722  elxp6  7773  elxp7  7774  releldm2  7792  opiota  7807  fnmpo  7817  frxp  7871  cnvimadfsn  7892  mpoxneldm  7932  dftpos4  7965  frrlem9  8013  wfrlem8  8040  wfrfun  8043  dfrecs3  8087  tfrlem7  8097  ondif1  8206  oarec  8268  oeeu  8309  0er  8406  eroveu  8472  erovlem  8473  elixpconst  8564  domen  8619  brsdom  8629  brdom2  8636  reuen1  8680  sbthlem10  8743  brsdom2  8748  xpf1o  8786  unfi  8828  onfin2  8847  0sdom1dom  8852  modom  8855  unfiOLD  8916  marypha2lem3  9031  wemapsolem  9144  elom3  9241  dfom5  9243  trcl  9322  epfrs  9325  rankf  9375  scottexs  9468  scott0s  9469  cplem1  9470  karden  9476  hta  9478  djuexb  9490  pm54.43lem  9581  alephsuc2  9659  iscard3  9672  aceq0  9697  aceq3lem  9699  dfac3  9700  dfac5lem2  9703  dfac5  9707  dfac7  9711  dfac12a  9727  kmlem12  9740  kmlem14  9742  kmlem15  9743  infmap2  9797  ackbij2  9822  dfacfin7  9978  ituniiun  10001  zorng  10083  brdom7disj  10110  entri2  10137  alephreg  10161  fpwwe2lem11  10220  fpwwe2lem12  10221  pwfseqlem1  10237  grutsk  10401  axgroth4  10411  grothprim  10413  grothtsk  10414  elni2  10456  ltsopi  10467  genpass  10588  psslinpr  10610  ltexprlem4  10618  ltresr  10719  1re  10798  infm3  11756  elnnz  12151  dfz2  12160  2rexuz  12461  nnwos  12476  eluz2b1  12480  qexALT  12525  elxr  12673  dflt2  12703  xrsupss  12864  xrinfmss  12865  elixx1  12909  elioo2  12941  dfrp2  12949  elioopnf  12996  elicopnf  12998  elfz1  13065  fznn  13145  fzp1nel  13161  fznn0  13169  preduz  13199  prinfzo0  13246  injresinj  13328  nn0opthlem1  13799  faclbnd4lem1  13824  hashfxnn0  13868  hashprdifel  13930  hashgt23el  13956  hashfun  13969  hashf1  13988  fz1isolem  13992  f1oun2prg  14447  brtrclfv  14530  shftdm  14599  rediv  14659  imdiv  14666  rexanre  14875  caubnd  14887  climreu  15082  prodmo  15461  dvdslelem  15833  3dvdsdec  15856  3dvds2dec  15857  bitsval  15946  smueqlem  16012  algcvgblem  16097  lcmfunsnlem2  16160  isprm2  16202  isprm3  16203  isprm4  16204  pythagtriplem2  16333  elgz  16447  hashbc0  16521  0ram  16536  isstruct  16679  issect  17212  isfull2  17372  isfth2  17376  fucinv  17436  eldmcoa  17525  isdrs  17762  submacs  18207  isnsg4  18537  isgim  18620  gaorb  18655  oppgid  18702  oppgsubm  18708  oppgcntz  18710  ispgp  18935  efgsdm  19074  efgcpbllema  19098  iscyg2  19220  isring  19520  isirred2  19673  opprirred  19674  dfrhm2  19691  drngid2  19737  opprsubrg  19775  issdrg  19793  islmod  19857  lss1d  19954  islmhm  20018  islmim  20053  lbsextlem2  20150  lidlnz  20220  isnzr2  20255  dfprm2  20414  isphl  20544  elocv  20584  iunocv  20597  isobs  20636  islinds  20725  isassa  20772  1mavmul  21399  toprntopon  21776  isbasis3g  21800  fctop  21855  cctop  21857  isclo2  21939  restsn  22021  lmbr  22109  ist0-3  22196  2ndcdisj  22307  1stccnp  22313  islocfin  22368  1stckgenlem  22404  txbas  22418  ptbasin  22428  tx2cn  22461  fbfinnfr  22692  fbasrn  22735  filuni  22736  ufinffr  22780  fin1aufil  22783  rnelfmlem  22803  flimrest  22834  alexsubALTlem3  22900  alexsubALTlem4  22901  tgphaus  22968  istlm  23036  iscusp2  23153  metuel2  23417  isngp2  23449  isnlm  23527  isphtpc  23845  phtpcer  23846  om1elbas  23883  isclm  23915  iscvsp  23979  iscph  24021  iscau3  24129  minveclem3b  24279  elovolm  24326  ioombl1lem4  24412  dyaddisj  24447  vitali  24464  itg1climres  24566  itg2seq  24594  itg2monolem1  24602  itg2mono  24605  limcrcl  24725  lhop1  24865  itgsubst  24900  mdegleb  24916  isuc1p  24992  ismon1p  24994  plydivex  25144  ellogdm  25481  1cubr  25679  atandm2  25714  birthdaylem3  25790  dmarea  25794  dchrelbas2  26072  dchrelbas4  26078  axcontlem7  27015  nb3grpr  27424  nb3grpr2  27425  upgrwlkcompim  27684  wlkson  27698  wlkonprop  27700  wksonproplem  27746  ispth  27764  wwlknon  27895  wwlksnextinj  27937  wspthsnwspthsnon  27954  elwspths2spth  28005  rusgrnumwwlkl1  28006  clwwlkccatlem  28026  erclwwlkref  28057  frgr3v  28312  nmoubi  28807  nmobndseqi  28814  nmobndseqiALT  28815  minvecolem1  28909  isch2  29258  hlimreui  29274  isch3  29276  ocsh  29318  dfch2  29442  spanuni  29579  nonbooli  29686  5oalem7  29695  adjsym  29868  elbdop2  29906  dmadjss  29922  nmopub  29943  nmfnleub  29960  nmop0h  30026  pjssposi  30207  pjordi  30208  cvbr2  30318  cvnbtwn2  30322  mdsl2i  30357  cvmdi  30359  elat2  30375  atom1d  30388  chirredi  30429  cdj3i  30476  or3di  30483  opreu2reu1  30505  mo5f  30510  reuxfrdf  30512  rexunirn  30513  difrab2  30518  iuninc  30573  disjorf  30591  disjunsn  30606  rabfmpunirn  30664  aciunf1  30674  funcnv5mpt  30679  eliccelico  30772  elicoelioo  30773  isomnd  31000  omndmul2  31011  isslmd  31128  islinds5  31231  ismxidl  31302  hasheuni  31719  pwsiga  31764  sigainb  31770  issros  31809  2ndmbfm  31894  omssubaddlem  31932  omssubadd  31933  sitgaddlemb  31981  eulerpartlemgvv  32009  eulerpartlemn  32014  probun  32052  ballotlem2  32121  ballotlemodife  32130  bnj252  32348  bnj253  32349  bnj255  32350  bnj345  32359  bnj133  32372  bnj976  32424  bnj1098  32430  bnj121  32517  bnj130  32521  bnj150  32523  bnj581  32555  bnj607  32563  bnj865  32570  bnj917  32581  bnj934  32582  bnj964  32590  bnj983  32598  bnj996  32603  bnj1021  32613  bnj1033  32616  bnj1047  32620  bnj1049  32621  bnj1090  32626  bnj1128  32637  bnj1175  32651  bnj1189  32656  bnj1253  32664  bnj1312  32705  exdifsn  32720  fineqvrep  32731  fineqvac  32733  erdszelem9  32828  erdszelem10  32829  pconnconn  32860  cvmliftiota  32930  fmlaomn0  33019  fmla0disjsuc  33027  fmlasucdisj  33028  dmopab3rexdif  33034  elmthm  33205  nepss  33331  xpab  33346  dfse3  33347  dfso2  33391  dfpo2  33392  elrn3  33399  imaindm  33423  elpotr  33427  dfon2lem5  33433  dfon2lem7  33435  dfon2lem8  33436  frind  33460  frxp2  33471  poxp3  33476  soseq  33483  elwlim  33497  wzel  33498  elno3  33544  nosgnn0  33547  nosepon  33554  nocvxminlem  33658  scutcut  33681  scutbday  33684  dmscut  33691  scutf  33692  sltrec  33700  made0  33743  brtxp2  33869  brpprod3a  33874  eltrans  33879  dfon3  33880  dffix2  33893  dffun10  33902  elfuns  33903  brsingle  33905  brimg  33925  funpartfun  33931  funpartfv  33933  cgrxfr  34043  segletr  34102  outsideoftr  34117  neifg  34246  filnetlem4  34256  df3nandALT1  34274  bj-consensusALT  34446  bj-df-ifc  34447  bj-biexal3  34575  bj-nfnnfTEMP  34626  bj-denoteslem  34741  bj-denotes  34742  bj-ralvw  34751  bj-rexvw  34752  bj-rexcom4bv  34754  bj-rexcom4b  34755  bj-sbeq  34773  bj-inrab  34801  bj-rcleqf  34901  bj-dfmpoa  34973  bj-imdirco  35045  topdifinffinlem  35204  topdifinfeq  35207  relowlssretop  35220  relowlpssretop  35221  rdgeqoa  35227  domalom  35261  nlpineqsn  35265  fvineqsneq  35269  wl-ifpimpr  35323  wl-df3xor3  35327  wl-3xorbi  35330  wl-3xorbi2  35331  wl-2xor  35340  wl-2mintru2  35348  wl-dfclab  35433  rabiun  35436  phpreu  35447  fin2solem  35449  matunitlindflem2  35460  ptrest  35462  poimirlem25  35488  poimirlem27  35490  poimirlem30  35493  ismblfin  35504  ovoliunnfl  35505  voliunnfl  35507  volsupnfl  35508  itg2addnclem2  35515  fdc  35589  prdstotbnd  35638  isdrngo1  35800  ispridl  35878  ismaxidl  35884  impor  35925  selconj  35944  tradd  35949  scott0f  36013  inxpss3  36135  idinxpssinxp2  36139  idinxpssinxp3  36140  dfrel5  36167  ineleq  36172  moantr  36180  dfxrn2  36192  inxpxrn  36207  rnxrnres  36211  1cossres  36238  cocossss  36245  cossssid4  36274  cossssid5  36275  cosscnvssid5  36282  cossid  36284  dfssr2  36303  cnvrefrelcoss2  36337  cosselcnvrefrels2  36338  eqvrelcoss  36416  eqvrelcoss2  36418  dfcoeleqvrel  36421  refrelredund4  36434  cnvepresdmqs  36451  dfmember  36470  dfdisjALTV  36510  dfeldisj3  36516  dfeldisj4  36517  dfeldisj5  36518  prter1  36579  islshp  36679  islshpat  36717  lcvbr2  36722  lcvnbtwn2  36727  cvrnbtwn3  36976  isatl  36999  ishlat1  37052  ishlat2  37053  cvrat4  37143  pmapglbx  37469  lhpexle3  37712  dib1dim  38865  diblsmopel  38871  lcfls1lem  39234  prjsperref  40094  prjspeclsp  40100  rexrabdioph  40260  dford4  40495  isdomn3  40673  ifpdfor2  40694  ifpdfan2  40696  ifpdfor  40698  ifpdfan  40699  ifpnot23b  40715  ifpnot23c  40717  ifpnot23d  40718  ifpim123g  40733  ifpbibib  40743  clss2lem  40836  imaiun1  40877  coiun1  40878  brfvrcld2  40918  iunrelexp0  40928  brtrclfv2  40953  snhesn  41012  dffrege76  41165  frege97  41186  frege98  41187  frege109  41198  frege110  41199  dffrege115  41204  frege131  41220  frege133  41222  ntrneineine1lem  41312  ntrneiel2  41314  ntrneiiso  41319  gneispace3  41361  scotteld  41478  ismnuprim  41526  ismnushort  41533  dfuniv2  41534  pm11.52  41619  pm11.58  41622  pm13.192  41642  impexpdcom  41749  sbc3or  41766  opelopab4  41785  uunT12p1  42034  uunT12p2  42035  uunT12p3  42036  uun2221  42047  uun2221p1  42048  uun2221p2  42049  undif3VD  42116  ndisj2  42213  nssrex  42250  rabssf  42282  bothtbothsame  44009  bothfbothsame  44010  aiffbtbat  44018  reuabaiotaiota  44194  2reu8i  44220  2reuimp0  44221  ichn  44524  dfodd2  44704  dfeven5  44734  dfodd7  44735  1nevenALTV  44759  oddprmne2  44783  isrng  45050  isrnghm  45066  islindeps2  45440  isldepslvec2  45442  line2xlem  45715  rextru  45765  rmotru  45766  reutru  45767  isnrm4  45840  iscnrm4  45864  isthincd2  45935  thinccic  45958  setrec1lem3  46009  aacllem  46119