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  2309  nf5  2315  nf6  2316  sbrim  2337  sbnf  2344  sb6x  2493  2sb5rf  2501  2sb6rf  2502  sb4b  2504  sb5f  2527  sbequ8  2530  sbhb  2550  eu6lem  2598  eu1  2635  iseqsetv-cleq  2824  issettru  2838  iseqsetv-clel  2839  issetlem  2840  cleqh  2889  cleqf  2950  sbabel  2954  necon3bii  3007  neor  3047  neorian  3050  rextru  3093  r19.26m  3121  r19.43  3130  3r19.43  3131  r2allem  3150  r19.23t  3258  ralcom4  3288  moel  3385  rabid2f  3442  eqv  3460  eqvf  3461  ralv  3476  rexv  3477  reuv  3478  rmov  3479  rexcom4b  3481  ceqsex4v  3503  ceqsex8v  3505  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  axrep6OLD  5242  vnexOLD  5275  inuni  5314  eusv2  5361  reusv2lem4  5366  rexxfr  5381  sspwb  5424  opthneg  5457  pwssun  5547  dfid3  5553  dffr6  5611  dffr2  5616  dffr2ALT  5617  opthprc  5719  elxp3  5721  xpiundir  5727  elvv  5730  raliunxp  5819  cnvuni  5870  dmopab2rex  5901  dm0rn0OLD  5909  dfres3  5977  ssdmres  6006  elidinxp  6040  idinxpres  6043  dfima2  6058  args  6088  dffr3  6095  cotrg  6105  intasym  6109  asymref  6110  intirr  6112  xpnz  6151  xp11  6168  ssrnres  6171  xpimasn  6178  coiun  6253  coass  6262  cnvso  6286  elsnxp  6289  dfpo2  6294  imaindm  6297  dffr4  6318  dfse3  6334  frpoind  6340  dflim2  6416  orddif  6456  dffun6  6544  dffun6f  6548  dffun7  6561  dffun9  6563  funfn  6564  svrelfun  6606  mptfnf  6668  dffn2  6705  dffn3  6716  fint  6755  dffn4  6796  dff1o4  6827  brprcneu  6869  brprcneuALT  6870  eqfnfv3  7025  fnreseql  7041  fsn  7130  ftpg  7154  abrexco  7242  imaiun  7243  dff13  7252  isof1oidb  7326  isof1oopb  7327  isocnv2  7333  eloprabga  7523  mpo2eqb  7546  elovmpo  7660  sorpss  7730  abexex  7969  elxp6  8021  elxp7  8022  releldm2  8041  opiota  8057  fnmpo  8067  frxp  8125  frxp2  8143  soseq  8158  cnvimadfsn  8171  mpoxneldm  8211  dftpos4  8244  frrlem9  8294  dfrecs3  8362  tfrlem7  8373  ondif1  8491  oarec  8552  oeeu  8594  brinxper  8729  0er  8738  eroveu  8815  erovlem  8816  elixpconst  8915  domen  8970  brsdom  8983  brdom2  8991  reuen1  9035  sbthlem10  9097  brsdom2  9102  xpf1o  9140  unfi  9168  sbthfilem  9195  onfin2  9214  0sdom1domALT  9220  modom  9224  marypha2lem3  9410  wemapsolem  9525  elom3  9630  dfom5  9632  brttrcl2  9696  ttrcltr  9698  ttrclse  9709  trcl  9710  epfrs  9713  frind  9735  rankf  9779  scottexsOLD  9885  scott0bsOLD  9887  cplem1OLD  9893  hta  9904  htaOLD  9905  djuexb  9917  pm54.43lem  10008  alephsuc2  10086  iscard3  10099  aceq0  10124  aceq3lem  10126  dfac3  10127  dfac5lem2  10130  dfac5  10134  dfac7  10138  dfac12a  10154  kmlem12  10167  kmlem14  10169  kmlem15  10170  infmap2  10222  ackbij2  10247  dfacfin7  10404  ituniiun  10427  zorng  10509  brdom7disj  10537  entri2  10569  alephreg  10594  fpwwe2lem11  10653  fpwwe2lem12  10654  pwfseqlem1  10670  grutsk  10834  axgroth4  10844  grothprim  10846  grothtsk  10847  elni2  10889  ltsopi  10900  genpass  11021  psslinpr  11043  ltexprlem4  11051  ltresr  11152  infm3  12201  elnnz  12628  dfz2  12637  2rexuz  12952  nnwos  12967  eluz2b1  12971  qexALT  13016  elxr  13170  dflt2  13202  xrsupss  13364  xrinfmss  13365  elixx1  13410  elioo2  13442  dfrp2  13450  elioopnf  13499  elicopnf  13501  elfz1  13569  fznn  13650  fzp1nel  13669  fznn0  13677  preduz  13708  prinfzo0  13757  injresinj  13850  nn0opthlem1  14335  faclbnd4lem1  14360  hashfxnn0  14404  hashprdifel  14465  hashgt23el  14492  hashfun  14505  hashf1  14525  fz1isolem  14529  f1oun2prg  14991  brtrclfv  15078  shftdm  15147  rediv  15221  imdiv  15228  rexanre  15437  caubnd  15449  climreu  15646  prodmo  16026  dvdslelem  16402  3dvdsdec  16425  3dvds2dec  16426  bitsval  16517  smueqlem  16583  algcvgblem  16670  lcmfunsnlem2  16733  isprm2  16775  isprm3  16776  isprm4  16777  pythagtriplem2  16912  elgz  17026  hashbc0  17100  0ram  17115  isstruct  17247  issect  17845  isfull2  18005  isfth2  18009  fucinv  18068  eldmcoa  18157  isdrs  18392  submacs  18939  isnsg4  19293  isgim  19392  gaorb  19437  oppgid  19486  oppgsubm  19492  oppgcntz  19494  ispgp  19722  efgsdm  19860  efgcpbllema  19884  iscyg2  20012  isomnd  20253  omndmul2  20263  isrng  20292  isring  20379  isirred2  20565  opprirred  20566  isrnghm  20585  dfrhm2  20618  rimval  20644  isnzr2  20681  opprsubrng  20724  opprsubrg  20758  isdomn3  20879  drngid2  20922  issdrg  20957  islmod  21051  lss1d  21150  islmhm  21214  islmim  21249  lbsextlem2  21349  lidlnz  21442  dfprm2  21689  isphl  21844  elocv  21884  iunocv  21897  isobs  21936  islinds  22025  1mavmul  22773  matunitlindflem2  22905  toprntopon  23153  isbasis3g  23177  fctop  23232  cctop  23234  isclo2  23316  restsn  23398  lmbr  23486  ist0-3  23573  2ndcdisj  23685  1stccnp  23691  islocfin  23746  1stckgenlem  23782  txbas  23796  ptbasin  23806  tx2cn  23839  fbfinnfr  24070  fbasrn  24113  filuni  24114  ufinffr  24158  fin1aufil  24161  rnelfmlem  24181  flimrest  24212  alexsubALTlem3  24278  alexsubALTlem4  24279  tgphaus  24346  istlm  24414  iscusp2  24530  metuel2  24794  isngp2  24826  isnlm  24904  isphtpc  25225  phtpcer  25226  om1elbas  25263  isclm  25295  iscvsp  25359  iscph  25401  iscau3  25509  minveclem3b  25659  elovolm  25706  ioombl1lem4  25792  dyaddisj  25827  vitali  25844  itg1climres  25945  itg2seq  25973  itg2monolem1  25981  itg2mono  25984  limcrcl  26104  lhop1  26244  itgsubst  26279  mdegleb  26292  isuc1p  26369  ismon1p  26371  plydivex  26530  ellogdm  26879  1cubr  27082  atandm2  27117  birthdaylem3  27193  dmarea  27197  dchrelbas2  27476  dchrelbas4  27482  elno3  27894  nosgnn0  27897  nosepon  27904  nocvxminlem  28022  cutcuts  28049  cutbday  28052  dmcuts  28059  cutsf  28060  ltsrec  28069  made0  28131  addsprop  28244  negsproplem2  28297  negsprop  28303  mulsprop  28398  precsexlem10  28484  elzs2  28667  elnnzs  28669  bdayfinbndlem1  28735  recut  28762  axcontlem7  29430  nb3grpr  29845  nb3grpr2  29846  upgrwlkcompim  30105  wlkson  30117  wlkonprop  30119  wksonproplem  30169  ispth  30188  wwlknon  30328  wwlksnextinj  30370  wspthsnwspthsnon  30387  elwspths2spth  30441  rusgrnumwwlkl1  30442  clwwlkccatlem  30462  erclwwlkref  30493  frgr3v  30758  nmoubi  31256  nmobndseqi  31263  nmobndseqiALT  31264  minvecolem1  31358  isch2  31707  hlimreui  31723  isch3  31725  ocsh  31767  dfch2  31891  spanuni  32028  nonbooli  32135  5oalem7  32144  adjsym  32317  elbdop2  32355  dmadjss  32371  nmopub  32392  nmfnleub  32409  nmop0h  32475  pjssposi  32656  pjordi  32657  cvbr2  32767  cvnbtwn2  32771  mdsl2i  32806  cvmdi  32808  elat2  32824  atom1d  32837  chirredi  32878  cdj3i  32925  or3di  32939  opreu2reu1  32962  mo5f  32967  reuxfrdf  32969  rexunirn  32970  difrab2  32976  rabsspr  32979  rabsstp  32980  tpssg  33015  iuninc  33037  disjorf  33055  disjunsn  33070  rabfmpunirn  33129  aciunf1  33139  funcnv5mpt  33143  eliccelico  33251  elicoelioo  33252  isslmd  33645  islinds5  33805  ismxidl  33868  1arithufdlem4  33960  hasheuni  34598  pwsiga  34643  sigainb  34650  issros  34689  2ndmbfm  34775  omssubaddlem  34813  omssubadd  34814  sitgaddlemb  34862  eulerpartlemgvv  34890  eulerpartlemn  34895  probun  34933  ballotlem2  35003  ballotlemodife  35012  bnj252  35216  bnj253  35217  bnj255  35218  bnj345  35227  bnj133  35240  bnj976  35290  bnj1098  35296  bnj121  35382  bnj130  35386  bnj150  35388  bnj581  35420  bnj607  35428  bnj865  35435  bnj917  35446  bnj934  35447  bnj964  35455  bnj983  35463  bnj996  35468  bnj1021  35478  bnj1033  35481  bnj1047  35485  bnj1049  35486  bnj1090  35491  bnj1128  35502  bnj1175  35516  bnj1189  35521  bnj1253  35529  bnj1312  35570  exdifsn  35592  scott0bOLD  35637  fineqvrep  35643  fineqvac  35645  kard0  35683  kardexen  35692  onvf1odlem4  35706  vonf1wev  35708  vonf1owevOLD  35710  vonf1osev  35712  erdszelem9  35781  erdszelem10  35782  pconnconn  35813  cvmliftiota  35883  fmlaomn0  35972  fmla0disjsuc  35980  fmlasucdisj  35981  dmopab3rexdif  35987  elmthm  36158  antnestALT  36276  nepss  36300  xpab  36308  dfso2  36337  elrn3  36344  elpotr  36361  dfon2lem5  36367  dfon2lem7  36369  dfon2lem8  36370  elwlim  36403  wzel  36404  brtxp2  36461  brpprod3a  36466  eltrans  36471  dfon3  36472  dffix2  36485  dffun10  36494  elfuns  36495  brsingle  36497  brimg  36517  funpartfun  36525  funpartfv  36527  cgrxfr  36638  segletr  36697  outsideoftr  36712  naddle  36802  neifg  36993  filnetlem4  37003  df3nandALT1  37021  weiunlem  37085  ttcwf3  37148  bj-consensusALT  37283  bj-df-ifc  37284  bj-exexalal  37310  bj-cbvaew  37377  bj-biexal3  37443  bj-alnnf  37473  bj-nfnnfTEMP  37518  bj-denoteslem  37617  bj-denotesALTV  37618  bj-ralvw  37625  bj-rexvw  37626  bj-rexcom4bv  37628  bj-rexcom4b  37629  bj-sbeq  37647  bj-inrab  37674  bj-rcleqf  37772  bj-dfmpoa  37871  bj-imdirco  37945  topdifinffinlem  38104  topdifinfeq  38107  relowlssretop  38120  relowlpssretop  38121  rdgeqoa  38127  domalom  38161  nlpineqsn  38165  fvineqsneq  38169  wl-ifpimpr  38223  wl-df3xor3  38227  wl-3xorbi  38230  wl-3xorbi2  38231  wl-2xor  38240  wl-2mintru2  38248  wl-dfclab  38351  rabiun  38355  phpreu  38361  fin2solem  38363  ptrest  38371  poimirlem25  38397  poimirlem27  38399  poimirlem30  38402  ismblfin  38413  ovoliunnfl  38414  voliunnfl  38416  volsupnfl  38417  itg2addnclem2  38424  fdc  38498  prdstotbnd  38547  isdrngo1  38709  ispridl  38787  ismaxidl  38793  impor  38834  selconj  38851  tradd  38856  r2alan  39002  inxpss3  39071  idinxpssinxp2  39075  idinxpssinxp3  39076  dfrel5  39097  ineleq  39105  ralmo  39111  ralrnmo  39112  ralrmo3  39115  moantr  39123  dfxrn2  39136  inxpxrn  39169  rnxrnres  39173  dfsuccl4  39225  coss1cnvres  39258  1cossres  39270  cocossss  39277  cossssid4  39311  cossssid5  39312  cosscnvssid5  39319  cossid  39321  dfssr2  39330  cnvrefrelcoss2  39368  cosselcnvrefrels2  39369  eqvrelcoss  39452  eqvrelcoss2  39454  dfcoeleqvrel  39457  refrelredund4  39470  cnvepresdmqs  39489  dfcomember  39508  dfdisjALTV  39549  disjimdmqseq  39560  dfeldisj3  39562  dfeldisj4  39563  dfeldisj5  39564  disjres  39595  prter1  39755  islshp  39855  islshpat  39893  lcvbr2  39898  lcvnbtwn2  39903  cvrnbtwn3  40152  isatl  40175  ishlat1  40228  ishlat2  40229  cvrat4  40319  pmapglbx  40645  lhpexle3  40888  dib1dim  42041  diblsmopel  42047  lcfls1lem  42410  prjsperref  43455  prjspeclsp  43461  euabsn2w  43528  rexrabdioph  43638  dford4  43873  onsupuni  44073  dflim6  44108  tfsconcatlem  44180  naddgeoa  44238  ifpdfor2  44304  ifpdfan2  44306  ifpdfor  44308  ifpdfan  44309  ifpnot23b  44325  ifpnot23c  44327  ifpnot23d  44328  ifpim123g  44343  ifpbibib  44353  clss2lem  44454  imaiun1  44494  coiun1  44495  brfvrcld2  44535  iunrelexp0  44545  brtrclfv2  44570  snhesn  44629  dffrege76  44782  frege97  44803  frege98  44804  frege109  44815  frege110  44816  dffrege115  44821  frege131  44837  frege133  44839  ntrneineine1lem  44927  ntrneiel2  44929  ntrneiiso  44934  gneispace3  44976  ismnuprim  45121  ismnushort  45128  dfuniv2  45129  pm11.52  45214  pm11.58  45217  pm13.192  45237  impexpdcom  45341  sbc3or  45358  opelopab4  45377  uunT12p1  45625  uunT12p2  45626  uunT12p3  45627  uun2221  45638  uun2221p1  45639  uun2221p2  45640  undif3VD  45707  modelaxreplem3  45806  permaxext  45831  permac8prim  45840  ndisj2  45888  rabssf  45954  wrddin2  47719  chndin2  47724  chnrin2  47729  bothtbothsame  47790  bothfbothsame  47791  aiffbtbat  47799  reuabaiotaiota  47978  2reu8i  48004  2reuimp0  48005  ichn  48359  dfodd2  48555  dfeven5  48585  dfodd7  48586  1nevenALTV  48610  oddprmne2  48634  dfvopnbgr2  48772  isuspgrim0lem  48812  gpg5nbgrvtx03starlem1  48987  gpg5nbgrvtx03starlem2  48988  gpg5nbgrvtx03starlem3  48989  gpg5nbgrvtx13starlem1  48990  gpg5nbgrvtx13starlem2  48991  gpg5nbgrvtx13starlem3  48992  gpg5edgnedg  49049  dfidom2  49261  islindeps2  49416  isldepslvec2  49418  line2xlem  49686  rmotru  49734  reutru  49735  isnrm4  49860  iscnrm4  49883  homf0  49938  fuco2el  50241  isthincd2  50366  thinccic  50400  istermc2  50404  istermc3  50405  dftermc3  50460  setrec1lem3  50618  dfrals2  50722  dfralseu2  50755  aacllem  50775