Theorem bitr4i 280

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

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  3bitr2i  301  3bitr2ri  302  3bitr4i  305  3bitr4ri  306  biluk  388  biancomi  466  dfbi2  478  imdistan  575  pm5.32  581  bianass  652  mpbiran  719  biadaniALT  830  imor  864  imimorb  963  pm5.6  1014  nbi2  1028  casesifp  1088  3ancoma  1109  3ancomb  1110  3anrev  1112  dfnan2  1513  nannan  1516  nanbi  1519  xorcom  1533  xorneg  1542  xorbi12i  1543  norcom  1549  noran  1551  norasslem1  1553  trunortru  1608  trunorfal  1609  cadan  1628  cadcomb  1632  nic-ax  1692  nic-axALT  1693  nf3  1805  19.43  1901  equsv  2022  sbrimvwOLD  2124  sbcom2  2205  sb5  2309  nf5  2315  nf6  2316  sbrim  2337  sbnf  2344  sb6x  2494  2sb5rf  2502  2sb6rf  2503  sb4b  2505  sb5f  2528  sbequ8  2531  sbhb  2551  eu6lem  2599  eu1  2636  iseqsetv-cleq  2825  issettru  2839  iseqsetv-clel  2840  issetlem  2841  cleqh  2890  cleqf  2951  sbabel  2955  necon3bii  3008  neor  3048  neorian  3051  rextru  3092  r19.26m  3120  r19.43  3129  3r19.43  3130  r2allem  3149  r19.23t  3257  ralcom4  3287  moel  3386  rabid2f  3444  eqv  3463  eqvf  3464  ralv  3479  rexv  3480  reuv  3481  rmov  3482  rexcom4b  3484  ceqsex4v  3506  ceqsex8v  3508  ceqsrexv  3613  rexab  3656  ralrab2  3659  rexrab2  3661  reu2  3686  reu3  3688  reueq  3698  2reuswap  3707  2reuswap2  3708  reuind  3714  2reu5lem3  3718  2rmoswap  3722  rmo2  3838  rmoanim  3845  rmoanimALT  3846  dfss3  3923  dfss3f  3926  nssrex  3999  ssabral  4015  rabss  4021  ssrabeq  4035  uniiunlem  4038  sspsstri  4057  npss  4065  dfdif3OLD  4070  raldifb  4100  uncom  4109  inass  4177  elsymdifxor  4210  nsspssun  4218  dfss4  4219  dfun2  4220  dfin2  4221  indi  4234  reupick3  4280  eq0f  4297  neq0f  4298  eq0ALT  4301  dfnf5  4332  rabn0  4340  csbab  4391  vss  4397  disj  4401  disj3  4405  undisj1  4413  undisj2  4414  inundif  4430  undif  4433  undifr  4434  rabsssn  4624  exsnrex  4636  euabsn2  4681  euabsn  4682  raldifsni  4752  tppreqb  4762  pwpw0  4768  prssg  4774  ssunsn  4783  prneimg2  4810  preqsn  4817  pwpr  4856  dfuni2  4864  unissb  4896  elint2  4909  ssint  4919  uniintab  4941  dfiin2g  4985  iunid  5015  iunn0  5021  iunxun  5048  iunxiun  5051  iinpw  5060  disjor  5079  disjxiun  5094  dftr2  5206  dftr3  5209  dftr4  5210  axrep6OLD  5234  vnexOLD  5265  inuni  5303  eusv2  5350  reusv2lem4  5355  rexxfr  5370  sspwb  5413  opthneg  5446  pwssun  5535  dfid3  5541  dffr6  5599  dffr2  5604  dffr2ALT  5605  opthprc  5707  elxp3  5709  xpiundir  5715  elvv  5718  raliunxp  5807  cnvuni  5858  dmopab2rex  5889  dm0rn0OLD  5897  dfres3  5966  ssdmres  5995  elidinxp  6029  idinxpres  6032  dfima2  6047  args  6077  dffr3  6084  cotrg  6094  intasym  6098  asymref  6099  intirr  6101  xpnz  6140  xp11  6156  ssrnres  6159  xpimasn  6166  coiun  6239  coass  6248  cnvso  6270  elsnxp  6273  dfpo2  6278  imaindm  6281  dffr4  6302  dfse3  6318  frpoind  6324  dflim2  6399  orddif  6439  dffun6  6527  dffun6f  6531  dffun7  6543  dffun9  6545  funfn  6546  svrelfun  6588  mptfnf  6651  dffn2  6688  dffn3  6699  fint  6738  dffn4  6779  dff1o4  6810  brprcneu  6852  brprcneuALT  6853  eqfnfv3  7008  fnreseql  7024  fsn  7112  ftpg  7134  abrexco  7223  imaiun  7224  dff13  7233  isof1oidb  7303  isof1oopb  7304  isocnv2  7310  eloprabga  7500  mpo2eqb  7523  elovmpo  7636  sorpss  7706  abexex  7947  elxp6  7999  elxp7  8000  releldm2  8019  opiota  8035  fnmpo  8045  frxp  8100  frxp2  8118  soseq  8133  cnvimadfsn  8146  mpoxneldm  8186  dftpos4  8219  frrlem9  8269  dfrecs3  8337  tfrlem7  8348  ondif1  8464  oarec  8525  oeeu  8567  brinxper  8702  0er  8711  eroveu  8788  erovlem  8789  elixpconst  8881  domen  8936  brsdom  8949  brdom2  8957  reuen1  9001  sbthlem10  9062  brsdom2  9067  xpf1o  9105  unfi  9133  sbthfilem  9160  onfin2  9179  0sdom1domALT  9185  modom  9189  marypha2lem3  9377  wemapsolem  9492  elom3  9597  dfom5  9599  brttrcl2  9663  ttrcltr  9665  ttrclse  9676  trcl  9677  epfrs  9680  frind  9702  rankf  9746  scottexs  9839  scott0s  9840  cplem1  9841  hta  9849  djuexb  9861  pm54.43lem  9952  alephsuc2  10030  iscard3  10043  aceq0  10068  aceq3lem  10070  dfac3  10071  dfac5lem2  10074  dfac5  10079  dfac7  10083  dfac12a  10099  kmlem12  10112  kmlem14  10114  kmlem15  10115  infmap2  10167  ackbij2  10192  dfacfin7  10350  ituniiun  10373  zorng  10455  brdom7disj  10482  entri2  10509  alephreg  10534  fpwwe2lem11  10593  fpwwe2lem12  10594  pwfseqlem1  10610  grutsk  10774  axgroth4  10784  grothprim  10786  grothtsk  10787  elni2  10829  ltsopi  10840  genpass  10961  psslinpr  10983  ltexprlem4  10991  ltresr  11092  infm3  12145  elnnz  12572  dfz2  12581  2rexuz  12895  nnwos  12910  eluz2b1  12914  qexALT  12959  elxr  13112  dflt2  13144  xrsupss  13306  xrinfmss  13307  elixx1  13352  elioo2  13384  dfrp2  13392  elioopnf  13441  elicopnf  13443  elfz1  13511  fznn  13591  fzp1nel  13610  fznn0  13618  preduz  13649  prinfzo0  13698  injresinj  13791  nn0opthlem1  14275  faclbnd4lem1  14300  hashfxnn0  14344  hashprdifel  14405  hashgt23el  14431  hashfun  14444  hashf1  14464  fz1isolem  14468  f1oun2prg  14924  brtrclfv  15009  shftdm  15078  rediv  15149  imdiv  15156  rexanre  15365  caubnd  15377  climreu  15574  prodmo  15957  dvdslelem  16334  3dvdsdec  16357  3dvds2dec  16358  bitsval  16449  smueqlem  16515  algcvgblem  16602  lcmfunsnlem2  16665  isprm2  16707  isprm3  16708  isprm4  16709  pythagtriplem2  16844  elgz  16958  hashbc0  17032  0ram  17047  isstruct  17179  issect  17777  isfull2  17937  isfth2  17941  fucinv  18000  eldmcoa  18089  isdrs  18324  submacs  18852  isnsg4  19199  isgim  19293  gaorb  19338  oppgid  19387  oppgsubm  19393  oppgcntz  19395  ispgp  19623  efgsdm  19761  efgcpbllema  19785  iscyg2  19913  isomnd  20154  omndmul2  20164  isrng  20191  isring  20274  isirred2  20457  opprirred  20458  isrnghm  20477  dfrhm2  20510  isnzr2  20555  opprsubrng  20596  opprsubrg  20630  isdomn3  20752  drngid2  20789  issdrg  20825  islmod  20919  lss1d  21018  islmhm  21082  islmim  21117  lbsextlem2  21217  lidlnz  21300  dfprm2  21513  isphl  21668  elocv  21708  iunocv  21721  isobs  21760  islinds  21849  1mavmul  22596  toprntopon  22973  isbasis3g  22997  fctop  23052  cctop  23054  isclo2  23136  restsn  23218  lmbr  23306  ist0-3  23393  2ndcdisj  23504  1stccnp  23510  islocfin  23565  1stckgenlem  23601  txbas  23615  ptbasin  23625  tx2cn  23658  fbfinnfr  23889  fbasrn  23932  filuni  23933  ufinffr  23977  fin1aufil  23980  rnelfmlem  24000  flimrest  24031  alexsubALTlem3  24097  alexsubALTlem4  24098  tgphaus  24165  istlm  24233  iscusp2  24349  metuel2  24613  isngp2  24645  isnlm  24723  isphtpc  25044  phtpcer  25045  om1elbas  25082  isclm  25114  iscvsp  25178  iscph  25220  iscau3  25328  minveclem3b  25478  elovolm  25525  ioombl1lem4  25611  dyaddisj  25646  vitali  25663  itg1climres  25764  itg2seq  25792  itg2monolem1  25800  itg2mono  25803  limcrcl  25924  lhop1  26064  itgsubst  26099  mdegleb  26112  isuc1p  26189  ismon1p  26191  plydivex  26349  ellogdm  26692  1cubr  26895  atandm2  26930  birthdaylem3  27006  dmarea  27010  dchrelbas2  27289  dchrelbas4  27295  elno3  27707  nosgnn0  27710  nosepon  27717  nocvxminlem  27835  cutcuts  27862  cutbday  27865  dmcuts  27872  cutsf  27873  ltsrec  27882  made0  27944  addsprop  28057  negsproplem2  28110  negsprop  28116  mulsprop  28211  precsexlem10  28297  elzs2  28480  elnnzs  28482  bdayfinbndlem1  28548  recut  28575  axcontlem7  29128  nb3grpr  29540  nb3grpr2  29541  upgrwlkcompim  29800  wlkson  29812  wlkonprop  29814  wksonproplem  29860  ispth  29878  wwlknon  30014  wwlksnextinj  30056  wspthsnwspthsnon  30073  elwspths2spth  30127  rusgrnumwwlkl1  30128  clwwlkccatlem  30148  erclwwlkref  30179  frgr3v  30434  nmoubi  30932  nmobndseqi  30939  nmobndseqiALT  30940  minvecolem1  31034  isch2  31383  hlimreui  31399  isch3  31401  ocsh  31443  dfch2  31567  spanuni  31704  nonbooli  31811  5oalem7  31820  adjsym  31993  elbdop2  32031  dmadjss  32047  nmopub  32068  nmfnleub  32085  nmop0h  32151  pjssposi  32332  pjordi  32333  cvbr2  32443  cvnbtwn2  32447  mdsl2i  32482  cvmdi  32484  elat2  32500  atom1d  32513  chirredi  32554  cdj3i  32601  or3di  32617  opreu2reu1  32642  mo5f  32647  reuxfrdf  32649  rexunirn  32650  difrab2  32656  rabsspr  32660  rabsstp  32661  tpssg  32696  iuninc  32720  disjorf  32739  disjunsn  32754  rabfmpunirn  32816  aciunf1  32826  funcnv5mpt  32830  eliccelico  32940  elicoelioo  32941  isslmd  33343  islinds5  33514  ismxidl  33611  1arithufdlem4  33704  hasheuni  34343  pwsiga  34388  sigainb  34394  issros  34433  2ndmbfm  34519  omssubaddlem  34557  omssubadd  34558  sitgaddlemb  34606  eulerpartlemgvv  34634  eulerpartlemn  34639  probun  34677  ballotlem2  34747  ballotlemodife  34756  bnj252  34960  bnj253  34961  bnj255  34962  bnj345  34971  bnj133  34984  bnj976  35034  bnj1098  35040  bnj121  35126  bnj130  35130  bnj150  35132  bnj581  35164  bnj607  35172  bnj865  35179  bnj917  35190  bnj934  35191  bnj964  35199  bnj983  35207  bnj996  35212  bnj1021  35222  bnj1033  35225  bnj1047  35229  bnj1049  35230  bnj1090  35235  bnj1128  35246  bnj1175  35260  bnj1189  35265  bnj1253  35273  bnj1312  35314  exdifsn  35335  fineqvrep  35371  fineqvac  35373  onvf1odlem4  35410  vonf1wev  35412  vonf1owevOLD  35414  vonf1osev  35416  erdszelem9  35510  erdszelem10  35511  pconnconn  35542  cvmliftiota  35612  fmlaomn0  35701  fmla0disjsuc  35709  fmlasucdisj  35710  dmopab3rexdif  35716  elmthm  35887  antnestALT  36005  nepss  36029  xpab  36037  dfso2  36066  elrn3  36073  elpotr  36090  dfon2lem5  36096  dfon2lem7  36098  dfon2lem8  36099  elwlim  36132  wzel  36133  brtxp2  36190  brpprod3a  36195  eltrans  36200  dfon3  36201  dffix2  36214  dffun10  36223  elfuns  36224  brsingle  36226  brimg  36246  funpartfun  36254  funpartfv  36256  cgrxfr  36366  segletr  36425  outsideoftr  36440  neifg  36692  filnetlem4  36702  df3nandALT1  36720  weiunlem  36784  ttcwf3  36847  bj-consensusALT  36983  bj-df-ifc  36984  bj-exexalal  37010  bj-cbvaew  37077  bj-biexal3  37143  bj-alnnf  37173  bj-nfnnfTEMP  37218  bj-denoteslem  37317  bj-denotesALTV  37318  bj-ralvw  37325  bj-rexvw  37326  bj-rexcom4bv  37328  bj-rexcom4b  37329  bj-sbeq  37347  bj-inrab  37373  bj-rcleqf  37471  bj-dfmpoa  37569  bj-imdirco  37643  topdifinffinlem  37802  topdifinfeq  37805  relowlssretop  37818  relowlpssretop  37819  rdgeqoa  37825  domalom  37859  nlpineqsn  37863  fvineqsneq  37867  wl-ifpimpr  37921  wl-df3xor3  37925  wl-3xorbi  37928  wl-3xorbi2  37929  wl-2xor  37938  wl-2mintru2  37946  wl-dfclab  38049  rabiun  38053  phpreu  38064  fin2solem  38066  matunitlindflem2  38077  ptrest  38079  poimirlem25  38105  poimirlem27  38107  poimirlem30  38110  ismblfin  38121  ovoliunnfl  38122  voliunnfl  38124  volsupnfl  38125  itg2addnclem2  38132  fdc  38205  prdstotbnd  38254  isdrngo1  38416  ispridl  38494  ismaxidl  38500  impor  38541  selconj  38560  tradd  38565  scott0f  38629  r2alan  38711  inxpss3  38780  idinxpssinxp2  38784  idinxpssinxp3  38785  dfrel5  38806  ineleq  38814  ralmo  38820  ralrnmo  38821  ralrmo3  38824  moantr  38832  dfxrn2  38845  inxpxrn  38878  rnxrnres  38882  dfsuccl4  38934  coss1cnvres  38967  1cossres  38979  cocossss  38986  cossssid4  39020  cossssid5  39021  cosscnvssid5  39028  cossid  39030  dfssr2  39039  cnvrefrelcoss2  39077  cosselcnvrefrels2  39078  eqvrelcoss  39161  eqvrelcoss2  39163  dfcoeleqvrel  39166  refrelredund4  39179  cnvepresdmqs  39198  dfcomember  39217  dfdisjALTV  39258  disjimdmqseq  39269  dfeldisj3  39271  dfeldisj4  39272  dfeldisj5  39273  disjres  39304  prter1  39464  islshp  39564  islshpat  39602  lcvbr2  39607  lcvnbtwn2  39612  cvrnbtwn3  39861  isatl  39884  ishlat1  39937  ishlat2  39938  cvrat4  40028  pmapglbx  40354  lhpexle3  40597  dib1dim  41750  diblsmopel  41756  lcfls1lem  42119  prjsperref  43149  prjspeclsp  43155  euabsn2w  43222  rexrabdioph  43332  dford4  43567  onsupuni  43767  dflim6  43802  tfsconcatlem  43874  naddgeoa  43932  ifpdfor2  43998  ifpdfan2  44000  ifpdfor  44002  ifpdfan  44003  ifpnot23b  44019  ifpnot23c  44021  ifpnot23d  44022  ifpim123g  44037  ifpbibib  44047  clss2lem  44148  imaiun1  44188  coiun1  44189  brfvrcld2  44229  iunrelexp0  44239  brtrclfv2  44264  snhesn  44323  dffrege76  44476  frege97  44497  frege98  44498  frege109  44509  frege110  44510  dffrege115  44515  frege131  44531  frege133  44533  ntrneineine1lem  44621  ntrneiel2  44623  ntrneiiso  44628  gneispace3  44670  scotteld  44783  ismnuprim  44831  ismnushort  44838  dfuniv2  44839  pm11.52  44924  pm11.58  44927  pm13.192  44947  impexpdcom  45052  sbc3or  45069  opelopab4  45088  uunT12p1  45336  uunT12p2  45337  uunT12p3  45338  uun2221  45349  uun2221p1  45350  uun2221p2  45351  undif3VD  45418  modelaxreplem3  45517  permaxext  45542  permac8prim  45551  ndisj2  45592  rabssf  45658  bothtbothsame  47454  bothfbothsame  47455  aiffbtbat  47463  reuabaiotaiota  47642  2reu8i  47668  2reuimp0  47669  ichn  48023  dfodd2  48219  dfeven5  48249  dfodd7  48250  1nevenALTV  48274  oddprmne2  48298  dfvopnbgr2  48436  isuspgrim0lem  48476  gpg5nbgrvtx03starlem1  48651  gpg5nbgrvtx03starlem2  48652  gpg5nbgrvtx03starlem3  48653  gpg5nbgrvtx13starlem1  48654  gpg5nbgrvtx13starlem2  48655  gpg5nbgrvtx13starlem3  48656  gpg5edgnedg  48713  islindeps2  49066  isldepslvec2  49068  line2xlem  49336  rmotru  49385  reutru  49386  isnrm4  49513  iscnrm4  49536  homf0  49591  fuco2el  49894  isthincd2  50019  thinccic  50053  istermc2  50057  istermc3  50058  dftermc3  50113  setrec1lem3  50271  aacllem  50383