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 ⊢ (𝜑 ↔ 𝜒)

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3bitr2i  302  3bitr2ri  303  3bitr4i  306  3bitr4ri  307  biluk  390  biancomi  468  dfbi2  480  imdistan  578  pm5.32  584  bianass  655  mpbiran  722  biadaniALT  833  imor  867  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  1642  cadcomb  1646  nic-ax  1706  nic-axALT  1707  nf3  1819  19.43  1915  equsv  2036  sbrimvwOLD  2129  sbcom2  2209  sb5  2310  nf5  2316  nf6  2317  sbrim  2338  sbnf  2345  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  3094  r19.26m  3122  r19.43  3131  3r19.43  3132  r2allem  3151  r19.23t  3259  ralcom4  3289  moel  3386  rabid2f  3443  eqv  3461  eqvf  3462  ralv  3477  rexv  3478  reuv  3479  rmov  3480  rexcom4b  3482  ceqsex4v  3504  ceqsex8v  3506  ceqsrexv  3609  rexab  3653  ralrab2  3656  rexrab2  3658  reu2  3683  reu3  3685  reueq  3695  2reuswap  3704  2reuswap2  3705  reuind  3711  2reu5lem3  3715  2rmoswap  3719  rmo2  3834  rmoanim  3842  rmoanimALT  3843  dfss3  3920  dfss3f  3923  nssrex  3996  ssabral  4012  rabss  4018  ssrabeq  4032  uniiunlem  4035  sspsstri  4054  npss  4062  raldifb  4096  uncom  4105  inass  4173  elsymdifxor  4206  nsspssun  4214  dfss4  4215  dfun2  4216  dfin2  4217  indi  4230  reupick3  4276  eq0f  4294  neq0f  4295  eq0ALT  4298  inssdif0  4322  dfnf5  4331  rabn0  4339  vss  4358  csbab  4398  disj  4403  disj3  4407  undisj1  4415  undisj2  4416  inundif  4435  undif  4438  undifr  4439  rabsssn  4629  exsnrex  4641  euabsn2  4686  euabsn  4687  raldifsni  4758  tppreqb  4768  pwpw0  4774  prssg  4780  ssunsn  4789  prneimg2  4815  preqsn  4822  pwpr  4861  dfuni2  4869  unissb  4901  elint2  4914  ssint  4924  uniintab  4946  dfiin2g  4989  iunid  5019  iunn0  5025  iunxun  5054  iunxiun  5057  iinpw  5066  disjor  5085  disjxiun  5100  dftr2  5214  dftr3  5217  dftr4  5218  vnexOLD  5272  inuni  5311  eusv2  5358  reusv2lem4  5363  rexxfr  5378  sspwb  5417  opthneg  5450  pwssun  5543  dfid3  5549  dffr6  5607  dffr2  5612  dffr2ALT  5613  opthprc  5715  elxp3  5717  xpiundir  5723  elvv  5726  raliunxp  5816  cnvuni  5868  dmopab2rex  5899  dm0rn0OLD  5907  dfres3  5975  ssdmres  6004  elidinxp  6036  idinxpres  6039  dfima2  6058  args  6090  dffr3  6097  cotrg  6105  intasym  6109  asymref  6110  intirr  6112  xpnz  6150  xp11  6167  ssrnres  6170  xpimasn  6177  coiun  6257  coass  6266  cnvso  6290  elsnxp  6293  dfpo2  6298  imaindm  6301  dffr4  6322  dfse3  6338  frpoind  6344  dflim2  6420  orddif  6460  dffun6  6548  dffun6f  6552  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  7134  ftpg  7158  abrexco  7246  imaiun  7247  dff13  7256  isof1oidb  7330  isof1oopb  7331  isocnv2  7337  eloprabga  7527  mpo2eqb  7550  elovmpo  7664  mpt3eqdv  7684  funmpt3  7685  mpt3fvd  7686  sorpss  7742  abexex  7981  elxp6  8033  elxp7  8034  releldm2  8052  opiota  8068  fnmpo  8078  frxp  8136  frxp2  8154  soseq  8169  cnvimadfsn  8182  mpoxneldm  8222  dftpos4  8255  frrlem9  8305  dfrecs3  8373  tfrlem7  8384  ondif1  8502  oarec  8563  oeeu  8605  brinxper  8740  0er  8749  eroveu  8826  erovlem  8827  elixpconst  8926  domen  8981  brsdom  8994  brdom2  9002  reuen1  9046  sbthlem10  9108  brsdom2  9113  xpf1o  9151  unfi  9179  sbthfilem  9206  onfin2  9225  0sdom1domALT  9231  modom  9235  marypha2lem3  9422  wemapsolem  9537  elom3  9642  dfom5  9644  brttrcl2  9708  ttrcltr  9710  ttrclse  9721  trcl  9722  epfrs  9725  frind  9747  rankf  9795  elhf3  9906  scottexsOLD  9936  scott0bsOLD  9938  cplem1OLD  9944  hta  9955  htaOLD  9956  setrec1lem3  9962  djuexb  9983  pm54.43lem  10074  alephsuc2  10152  iscard3  10165  aceq0  10190  aceq3lem  10192  dfac3  10193  dfac5lem2  10196  dfac5  10200  dfac7  10204  dfac12a  10220  kmlem12  10233  kmlem14  10235  kmlem15  10236  infmap2  10288  ackbij2  10313  dfacfin7  10470  ituniiun  10493  zorng  10575  brdom7disj  10603  entri2  10635  alephreg  10660  fpwwe2lem11  10719  fpwwe2lem12  10720  pwfseqlem1  10736  grutsk  10900  axgroth4  10910  grothprim  10912  grothtsk  10913  elni2  10955  ltsopi  10966  genpass  11087  psslinpr  11109  ltexprlem4  11117  ltresr  11218  infm3  12269  elnnz  12696  dfz2  12705  2rexuz  13020  nnwos  13035  eluz2b1  13039  qexALT  13084  elxr  13238  dflt2  13270  xrsupss  13432  xrinfmss  13433  elixx1  13478  elioo2  13510  dfrp2  13518  elioopnf  13567  elicopnf  13569  elfz1  13637  fznn  13719  fzp1nel  13738  fznn0  13746  preduz  13777  prinfzo0  13826  injresinj  13919  nn0opthlem1  14405  faclbnd4lem1  14430  hashfxnn0  14474  hashprdifel  14535  hashgt23el  14562  hashfun  14575  hashf1  14595  fz1isolem  14599  f1oun2prg  15061  brtrclfv  15148  shftdm  15217  rediv  15291  imdiv  15298  rexanre  15507  caubnd  15519  climreu  15716  prodmo  16096  dvdslelem  16472  3dvdsdec  16495  3dvds2dec  16496  bitsval  16587  smueqlem  16653  algcvgblem  16745  lcmfunsnlem2  16808  isprm2  16850  isprm3  16851  isprm4  16852  pythagtriplem2  16988  elgz  17102  hashbc0  17176  0ram  17191  isstruct  17323  issect  17921  isfull2  18081  isfth2  18085  fucinv  18144  eldmcoa  18233  isdrs  18468  submacs  19016  isnsg4  19370  isgim  19469  gaorb  19514  oppgid  19563  oppgsubm  19569  oppgcntz  19571  ispgp  19799  efgsdm  19937  efgcpbllema  19961  iscyg2  20089  isomnd  20330  omndmul2  20340  isrng  20369  isring  20456  isirred2  20644  opprirred  20645  isrnghm  20664  dfrhm2  20697  rimval  20723  isnzr2  20761  opprsubrng  20804  opprsubrg  20838  isdomn3  20959  drngid2  21003  issdrg  21038  islmod  21132  lss1d  21231  islmhm  21295  islmim  21330  lbsextlem2  21430  lidlnz  21523  dfprm2  21772  isphl  21927  elocv  21967  iunocv  21980  isobs  22019  islinds  22108  1mavmul  22856  matunitlindflem2  22988  toprntopon  23236  isbasis3g  23260  fctop  23315  cctop  23317  isclo2  23399  restsn  23481  lmbr  23569  ist0-3  23656  2ndcdisj  23768  1stccnp  23774  islocfin  23829  1stckgenlem  23865  txbas  23879  ptbasin  23889  tx2cn  23922  fbfinnfr  24153  fbasrn  24196  filuni  24197  ufinffr  24241  fin1aufil  24244  rnelfmlem  24264  flimrest  24295  alexsubALTlem3  24361  alexsubALTlem4  24362  tgphaus  24429  istlm  24497  iscusp2  24613  metuel2  24877  isngp2  24909  isnlm  24987  isphtpc  25308  phtpcer  25309  om1elbas  25346  isclm  25378  iscvsp  25442  iscph  25484  iscau3  25592  minveclem3b  25742  elovolm  25789  ioombl1lem4  25875  dyaddisj  25910  vitali  25927  itg1climres  26028  itg2seq  26056  itg2monolem1  26064  itg2mono  26067  limcrcl  26187  lhop1  26327  itgsubst  26362  mdegleb  26375  isuc1p  26452  ismon1p  26454  plydivex  26611  ellogdm  26960  1cubr  27163  atandm2  27198  birthdaylem3  27274  dmarea  27278  dchrelbas2  27557  dchrelbas4  27563  elno3  28005  nosgnn0  28008  nosepon  28015  nocvxminlem  28133  cutcuts  28160  cutbday  28163  dmcuts  28170  cutsf  28171  ltsrec  28180  made0  28242  addsprop  28355  negsproplem2  28408  negsprop  28414  mulsprop  28509  precsexlem10  28595  elzs2  28778  elnnzs  28780  bdayfinbndlem1  28846  recut  28873  axcontlem7  29541  nb3grpr  29956  nb3grpr2  29957  upgrwlkcompim  30216  wlkson  30228  wlkonprop  30230  wksonproplem  30280  ispth  30299  wwlknon  30439  wwlksnextinj  30481  wspthsnwspthsnon  30498  elwspths2spth  30552  rusgrnumwwlkl1  30553  clwwlkccatlem  30573  erclwwlkref  30604  frgr3v  30869  nmoubi  31367  nmobndseqi  31374  nmobndseqiALT  31375  minvecolem1  31469  isch2  31818  hlimreui  31834  isch3  31836  ocsh  31878  dfch2  32002  spanuni  32139  nonbooli  32246  5oalem7  32255  adjsym  32428  elbdop2  32466  dmadjss  32482  nmopub  32503  nmfnleub  32520  nmop0h  32586  pjssposi  32767  pjordi  32768  cvbr2  32878  cvnbtwn2  32882  mdsl2i  32917  cvmdi  32919  elat2  32935  atom1d  32948  chirredi  32989  cdj3i  33036  or3di  33050  opreu2reu1  33073  mo5f  33078  reuxfrdf  33080  rexunirn  33081  difrab2  33087  rabsspr  33090  rabsstp  33091  tpssg  33126  iuninc  33148  disjorf  33166  disjunsn  33181  rabfmpunirn  33240  aciunf1  33250  funcnv5mpt  33254  eliccelico  33362  elicoelioo  33363  isslmd  33756  islinds5  33916  ismxidl  33980  1arithufdlem4  34072  hasheuni  34710  pwsiga  34755  sigainb  34762  issros  34801  2ndmbfm  34886  omssubaddlem  34924  omssubadd  34925  sitgaddlemb  34973  eulerpartlemgvv  35001  eulerpartlemn  35006  probun  35044  ballotlem2  35114  ballotlemodife  35123  bnj252  35327  bnj253  35328  bnj255  35329  bnj345  35338  bnj133  35351  bnj976  35401  bnj1098  35407  bnj121  35493  bnj130  35497  bnj150  35499  bnj581  35531  bnj607  35539  bnj865  35546  bnj917  35557  bnj934  35558  bnj964  35566  bnj983  35574  bnj996  35579  bnj1021  35589  bnj1033  35592  bnj1047  35596  bnj1049  35597  bnj1090  35602  bnj1128  35613  bnj1175  35627  bnj1189  35632  bnj1253  35640  bnj1312  35681  exdifsn  35703  scott0bOLD  35739  fineqvrep  35765  fineqvac  35767  kard0  35805  kardexen  35814  onvf1odlem4  35868  vonf1wev  35870  vonf1owevOLD  35872  vonf1osev  35874  erdszelem9  35943  erdszelem10  35944  pconnconn  35975  cvmliftiota  36045  fmlaomn0  36134  fmla0disjsuc  36142  fmlasucdisj  36143  dmopab3rexdif  36149  elmthm  36320  antnestALT  36438  nepss  36462  xpab  36470  dfso2  36499  elrn3  36506  elpotr  36523  dfon2lem5  36529  dfon2lem7  36531  dfon2lem8  36532  elwlim  36565  wzel  36566  brtxp2  36623  brpprod3a  36628  eltrans  36633  dfon3  36634  dffix2  36647  dffun10  36656  elfuns  36657  brsingle  36659  brimg  36679  funpartfun  36687  funpartfv  36689  cgrxfr  36800  segletr  36859  outsideoftr  36874  naddle  36948  neifg  37139  filnetlem4  37149  df3nandALT1  37167  weiunlem  37231  ttcwf3  37294  bj-consensusALT  37429  bj-df-ifc  37430  bj-exexalal  37456  bj-cbvaew  37523  bj-biexal3  37589  bj-alnnf  37619  bj-nfnnfTEMP  37664  bj-denoteslem  37763  bj-denotesALTV  37764  bj-ralvw  37771  bj-rexvw  37772  bj-rexcom4bv  37774  bj-rexcom4b  37775  bj-sbeq  37793  bj-inrab  37820  bj-rcleqf  37918  bj-dfmpoa  38019  bj-imdirco  38091  topdifinffinlem  38250  topdifinfeq  38253  relowlssretop  38266  relowlpssretop  38267  rdgeqoa  38273  domalom  38307  nlpineqsn  38311  fvineqsneq  38315  wl-ifpimpr  38369  wl-df3xor3  38373  wl-3xorbi  38376  wl-3xorbi2  38377  wl-2xor  38386  wl-2mintru2  38394  wl-dfclab  38497  rabiun  38501  phpreu  38507  fin2solem  38509  ptrest  38517  poimirlem25  38543  poimirlem27  38545  poimirlem30  38548  ismblfin  38559  ovoliunnfl  38560  voliunnfl  38562  volsupnfl  38563  itg2addnclem2  38570  dfprop1  38625  fdc  38659  prdstotbnd  38708  isdrngo1  38870  ispridl  38948  ismaxidl  38954  impor  38995  selconj  39012  tradd  39017  r2alan  39163  inxpss3  39232  idinxpssinxp2  39236  idinxpssinxp3  39237  dfrel5  39258  ineleq  39266  ralmo  39272  ralrnmo  39273  ralrmo3  39276  moantr  39284  dfxrn2  39297  inxpxrn  39330  rnxrnres  39334  dfsuccl4  39386  coss1cnvres  39419  1cossres  39431  cocossss  39438  cossssid4  39472  cossssid5  39473  cosscnvssid5  39480  cossid  39482  dfssr2  39491  cnvrefrelcoss2  39529  cosselcnvrefrels2  39530  eqvrelcoss  39613  eqvrelcoss2  39615  dfcoeleqvrel  39618  refrelredund4  39631  cnvepresdmqs  39650  dfcomember  39669  dfdisjALTV  39710  disjimdmqseq  39721  dfeldisj3  39723  dfeldisj4  39724  dfeldisj5  39725  disjres  39756  prter1  39916  islshp  40016  islshpat  40054  lcvbr2  40059  lcvnbtwn2  40064  cvrnbtwn3  40313  isatl  40336  ishlat1  40389  ishlat2  40390  cvrat4  40480  pmapglbx  40806  lhpexle3  41049  dib1dim  42202  diblsmopel  42208  lcfls1lem  42571  prjsperref  43614  prjspeclsp  43620  euabsn2w  43670  rexrabdioph  43780  dford4  44015  onsupuni  44215  dflim6  44250  tfsconcatlem  44322  naddgeoa  44380  ifpdfor2  44446  ifpdfan2  44448  ifpdfor  44450  ifpdfan  44451  ifpnot23b  44467  ifpnot23c  44469  ifpnot23d  44470  ifpim123g  44485  ifpbibib  44495  clss2lem  44596  imaiun1  44636  coiun1  44637  brfvrcld2  44677  iunrelexp0  44687  brtrclfv2  44712  snhesn  44771  dffrege76  44924  frege97  44945  frege98  44946  frege109  44957  frege110  44958  dffrege115  44963  frege131  44979  frege133  44981  ntrneineine1lem  45069  ntrneiel2  45071  ntrneiiso  45076  gneispace3  45118  ismnuprim  45263  ismnushort  45270  dfuniv2  45271  pm11.52  45356  pm11.58  45359  pm13.192  45379  impexpdcom  45483  sbc3or  45500  opelopab4  45519  uunT12p1  45767  uunT12p2  45768  uunT12p3  45769  uun2221  45780  uun2221p1  45781  uun2221p2  45782  undif3VD  45849  modelaxreplem3  45948  permaxext  45973  permac8prim  45982  ndisj2  46037  rabssf  46103  wrddin2  47867  chndin2  47872  chnrin2  47877  bothtbothsame  47938  bothfbothsame  47939  aiffbtbat  47947  reuabaiotaiota  48126  2reu8i  48152  2reuimp0  48153  ichn  48507  dfodd2  48703  dfeven5  48733  dfodd7  48734  1nevenALTV  48758  oddprmne2  48782  dfvopnbgr2  48920  isuspgrim0lem  48960  gpg5nbgrvtx03starlem1  49135  gpg5nbgrvtx03starlem2  49136  gpg5nbgrvtx03starlem3  49137  gpg5nbgrvtx13starlem1  49138  gpg5nbgrvtx13starlem2  49139  gpg5nbgrvtx13starlem3  49140  gpg5edgnedg  49197  dfidom2  49409  islindeps2  49564  isldepslvec2  49566  line2xlem  49834  rmotru  49882  reutru  49883  isnrm4  50008  iscnrm4  50031  homf0  50086  fuco2el  50389  isthincd2  50514  thinccic  50548  istermc2  50552  istermc3  50553  dftermc3  50608  dfrals2  50855  dfralseu2  50888  aacllem  50908