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  2210  sb5  2313  nf5  2319  nf6  2320  sbrim  2341  sbnf  2348  sb6x  2498  2sb5rf  2506  2sb6rf  2507  sb4b  2509  sb5f  2532  sbequ8  2535  sbhb  2555  eu6lem  2603  eu1  2640  iseqsetv-cleq  2829  issettru  2843  iseqsetv-clel  2844  issetlem  2845  cleqh  2894  cleqf  2955  sbabel  2959  necon3bii  3012  neor  3052  neorian  3055  rextru  3098  r19.26m  3126  r19.43  3135  3r19.43  3136  r2allem  3155  r19.23t  3263  ralcom4  3293  moel  3391  rabid2f  3449  eqv  3467  eqvf  3468  ralv  3483  rexv  3484  reuv  3485  rmov  3486  rexcom4b  3488  ceqsex4v  3510  ceqsex8v  3512  ceqsrexv  3616  rexab  3660  ralrab2  3663  rexrab2  3665  reu2  3690  reu3  3692  reueq  3702  2reuswap  3711  2reuswap2  3712  reuind  3718  2reu5lem3  3722  2rmoswap  3726  rmo2  3841  rmoanim  3849  rmoanimALT  3850  dfss3  3927  dfss3f  3930  nssrex  4003  ssabral  4019  rabss  4025  ssrabeq  4039  uniiunlem  4042  sspsstri  4061  npss  4069  raldifb  4103  uncom  4112  inass  4180  elsymdifxor  4213  nsspssun  4221  dfss4  4222  dfun2  4223  dfin2  4224  indi  4237  reupick3  4283  eq0f  4301  neq0f  4302  eq0ALT  4305  inssdif0  4329  dfnf5  4338  rabn0  4346  vss  4365  csbab  4405  disj  4410  disj3  4414  undisj1  4422  undisj2  4423  inundif  4442  undif  4445  undifr  4446  rabsssn  4636  exsnrex  4648  euabsn2  4693  euabsn  4694  raldifsni  4765  tppreqb  4775  pwpw0  4781  prssg  4787  ssunsn  4796  prneimg2  4822  preqsn  4829  pwpr  4868  dfuni2  4876  unissb  4908  elint2  4921  ssint  4931  uniintab  4953  dfiin2g  4997  iunid  5027  iunn0  5033  iunxun  5062  iunxiun  5065  iinpw  5074  disjor  5093  disjxiun  5108  dftr2  5222  dftr3  5225  dftr4  5226  axrep6OLD  5250  vnexOLD  5283  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  6293  elsnxp  6296  dfpo2  6301  imaindm  6304  dffr4  6325  dfse3  6341  frpoind  6347  dflim2  6423  orddif  6463  dffun6  6551  dffun6f  6555  dffun7  6567  dffun9  6569  funfn  6570  svrelfun  6612  mptfnf  6674  dffn2  6711  dffn3  6722  fint  6761  dffn4  6802  dff1o4  6833  brprcneu  6875  brprcneuALT  6876  eqfnfv3  7031  fnreseql  7047  fsn  7135  ftpg  7157  abrexco  7244  imaiun  7245  dff13  7254  isof1oidb  7328  isof1oopb  7329  isocnv2  7335  eloprabga  7525  mpo2eqb  7548  elovmpo  7661  sorpss  7731  abexex  7970  elxp6  8022  elxp7  8023  releldm2  8042  opiota  8058  fnmpo  8068  frxp  8124  frxp2  8142  soseq  8157  cnvimadfsn  8170  mpoxneldm  8210  dftpos4  8243  frrlem9  8293  dfrecs3  8361  tfrlem7  8372  ondif1  8488  oarec  8549  oeeu  8591  brinxper  8726  0er  8735  eroveu  8812  erovlem  8813  elixpconst  8905  domen  8960  brsdom  8973  brdom2  8981  reuen1  9025  sbthlem10  9087  brsdom2  9092  xpf1o  9130  unfi  9158  sbthfilem  9185  onfin2  9204  0sdom1domALT  9210  modom  9214  marypha2lem3  9400  wemapsolem  9515  elom3  9620  dfom5  9622  brttrcl2  9686  ttrcltr  9688  ttrclse  9699  trcl  9700  epfrs  9703  frind  9725  rankf  9769  scottexsOLD  9875  scott0bsOLD  9877  cplem1OLD  9883  hta  9894  htaOLD  9895  djuexb  9907  pm54.43lem  9998  alephsuc2  10076  iscard3  10089  aceq0  10114  aceq3lem  10116  dfac3  10117  dfac5lem2  10120  dfac5  10124  dfac7  10128  dfac12a  10144  kmlem12  10157  kmlem14  10159  kmlem15  10160  infmap2  10212  ackbij2  10237  dfacfin7  10394  ituniiun  10417  zorng  10499  brdom7disj  10526  entri2  10553  alephreg  10578  fpwwe2lem11  10637  fpwwe2lem12  10638  pwfseqlem1  10654  grutsk  10818  axgroth4  10828  grothprim  10830  grothtsk  10831  elni2  10873  ltsopi  10884  genpass  11005  psslinpr  11027  ltexprlem4  11035  ltresr  11136  infm3  12185  elnnz  12612  dfz2  12621  2rexuz  12935  nnwos  12950  eluz2b1  12954  qexALT  12999  elxr  13152  dflt2  13184  xrsupss  13346  xrinfmss  13347  elixx1  13392  elioo2  13424  dfrp2  13432  elioopnf  13481  elicopnf  13483  elfz1  13551  fznn  13632  fzp1nel  13651  fznn0  13659  preduz  13690  prinfzo0  13739  injresinj  13832  nn0opthlem1  14317  faclbnd4lem1  14342  hashfxnn0  14386  hashprdifel  14447  hashgt23el  14474  hashfun  14487  hashf1  14507  fz1isolem  14511  f1oun2prg  14973  brtrclfv  15058  shftdm  15127  rediv  15201  imdiv  15208  rexanre  15417  caubnd  15429  climreu  15626  prodmo  16008  dvdslelem  16384  3dvdsdec  16407  3dvds2dec  16408  bitsval  16499  smueqlem  16565  algcvgblem  16652  lcmfunsnlem2  16715  isprm2  16757  isprm3  16758  isprm4  16759  pythagtriplem2  16894  elgz  17008  hashbc0  17082  0ram  17097  isstruct  17229  issect  17827  isfull2  17987  isfth2  17991  fucinv  18050  eldmcoa  18139  isdrs  18374  submacs  18909  isnsg4  19256  isgim  19355  gaorb  19400  oppgid  19449  oppgsubm  19455  oppgcntz  19457  ispgp  19685  efgsdm  19823  efgcpbllema  19847  iscyg2  19975  isomnd  20216  omndmul2  20226  isrng  20255  isring  20342  isirred2  20528  opprirred  20529  isrnghm  20548  dfrhm2  20581  rimval  20607  isnzr2  20644  opprsubrng  20687  opprsubrg  20721  isdomn3  20842  drngid2  20885  issdrg  20920  islmod  21014  lss1d  21113  islmhm  21177  islmim  21212  lbsextlem2  21312  lidlnz  21405  dfprm2  21652  isphl  21807  elocv  21847  iunocv  21860  isobs  21899  islinds  21988  1mavmul  22734  toprntopon  23111  isbasis3g  23135  fctop  23190  cctop  23192  isclo2  23274  restsn  23356  lmbr  23444  ist0-3  23531  2ndcdisj  23642  1stccnp  23648  islocfin  23703  1stckgenlem  23739  txbas  23753  ptbasin  23763  tx2cn  23796  fbfinnfr  24027  fbasrn  24070  filuni  24071  ufinffr  24115  fin1aufil  24118  rnelfmlem  24138  flimrest  24169  alexsubALTlem3  24235  alexsubALTlem4  24236  tgphaus  24303  istlm  24371  iscusp2  24487  metuel2  24751  isngp2  24783  isnlm  24861  isphtpc  25182  phtpcer  25183  om1elbas  25220  isclm  25252  iscvsp  25316  iscph  25358  iscau3  25466  minveclem3b  25616  elovolm  25663  ioombl1lem4  25749  dyaddisj  25784  vitali  25801  itg1climres  25902  itg2seq  25930  itg2monolem1  25938  itg2mono  25941  limcrcl  26062  lhop1  26202  itgsubst  26237  mdegleb  26250  isuc1p  26327  ismon1p  26329  plydivex  26487  ellogdm  26833  1cubr  27036  atandm2  27071  birthdaylem3  27147  dmarea  27151  dchrelbas2  27430  dchrelbas4  27436  elno3  27848  nosgnn0  27851  nosepon  27858  nocvxminlem  27976  cutcuts  28003  cutbday  28006  dmcuts  28013  cutsf  28014  ltsrec  28023  made0  28085  addsprop  28198  negsproplem2  28251  negsprop  28257  mulsprop  28352  precsexlem10  28438  elzs2  28621  elnnzs  28623  bdayfinbndlem1  28689  recut  28716  axcontlem7  29349  nb3grpr  29761  nb3grpr2  29762  upgrwlkcompim  30021  wlkson  30033  wlkonprop  30035  wksonproplem  30081  ispth  30099  wwlknon  30235  wwlksnextinj  30277  wspthsnwspthsnon  30294  elwspths2spth  30348  rusgrnumwwlkl1  30349  clwwlkccatlem  30369  erclwwlkref  30400  frgr3v  30655  nmoubi  31153  nmobndseqi  31160  nmobndseqiALT  31161  minvecolem1  31255  isch2  31604  hlimreui  31620  isch3  31622  ocsh  31664  dfch2  31788  spanuni  31925  nonbooli  32032  5oalem7  32041  adjsym  32214  elbdop2  32252  dmadjss  32268  nmopub  32289  nmfnleub  32306  nmop0h  32372  pjssposi  32553  pjordi  32554  cvbr2  32664  cvnbtwn2  32668  mdsl2i  32703  cvmdi  32705  elat2  32721  atom1d  32734  chirredi  32775  cdj3i  32822  or3di  32836  opreu2reu1  32859  mo5f  32864  reuxfrdf  32866  rexunirn  32867  difrab2  32873  rabsspr  32876  rabsstp  32877  tpssg  32912  iuninc  32934  disjorf  32953  disjunsn  32968  rabfmpunirn  33027  aciunf1  33037  funcnv5mpt  33041  eliccelico  33151  elicoelioo  33152  isslmd  33545  islinds5  33705  ismxidl  33768  1arithufdlem4  33860  hasheuni  34498  pwsiga  34543  sigainb  34550  issros  34589  2ndmbfm  34675  omssubaddlem  34713  omssubadd  34714  sitgaddlemb  34762  eulerpartlemgvv  34790  eulerpartlemn  34795  probun  34833  ballotlem2  34903  ballotlemodife  34912  bnj252  35116  bnj253  35117  bnj255  35118  bnj345  35127  bnj133  35140  bnj976  35190  bnj1098  35196  bnj121  35282  bnj130  35286  bnj150  35288  bnj581  35320  bnj607  35328  bnj865  35335  bnj917  35346  bnj934  35347  bnj964  35355  bnj983  35363  bnj996  35368  bnj1021  35378  bnj1033  35381  bnj1047  35385  bnj1049  35386  bnj1090  35391  bnj1128  35402  bnj1175  35416  bnj1189  35421  bnj1253  35429  bnj1312  35470  exdifsn  35492  scott0bOLD  35537  fineqvrep  35543  fineqvac  35545  kard0  35583  kardexen  35592  onvf1odlem4  35606  vonf1wev  35608  vonf1owevOLD  35610  vonf1osev  35612  erdszelem9  35704  erdszelem10  35705  pconnconn  35736  cvmliftiota  35806  fmlaomn0  35895  fmla0disjsuc  35903  fmlasucdisj  35904  dmopab3rexdif  35910  elmthm  36081  antnestALT  36199  nepss  36223  xpab  36231  dfso2  36260  elrn3  36267  elpotr  36284  dfon2lem5  36290  dfon2lem7  36292  dfon2lem8  36293  elwlim  36326  wzel  36327  brtxp2  36384  brpprod3a  36389  eltrans  36394  dfon3  36395  dffix2  36408  dffun10  36417  elfuns  36418  brsingle  36420  brimg  36440  funpartfun  36448  funpartfv  36450  cgrxfr  36560  segletr  36619  outsideoftr  36634  naddle  36724  neifg  36915  filnetlem4  36925  df3nandALT1  36943  weiunlem  37007  ttcwf3  37070  bj-consensusALT  37205  bj-df-ifc  37206  bj-exexalal  37232  bj-cbvaew  37299  bj-biexal3  37365  bj-alnnf  37395  bj-nfnnfTEMP  37440  bj-denoteslem  37539  bj-denotesALTV  37540  bj-ralvw  37547  bj-rexvw  37548  bj-rexcom4bv  37550  bj-rexcom4b  37551  bj-sbeq  37569  bj-inrab  37596  bj-rcleqf  37694  bj-dfmpoa  37793  bj-imdirco  37867  topdifinffinlem  38026  topdifinfeq  38029  relowlssretop  38042  relowlpssretop  38043  rdgeqoa  38049  domalom  38083  nlpineqsn  38087  fvineqsneq  38091  wl-ifpimpr  38145  wl-df3xor3  38149  wl-3xorbi  38152  wl-3xorbi2  38153  wl-2xor  38162  wl-2mintru2  38170  wl-dfclab  38273  rabiun  38277  phpreu  38288  fin2solem  38290  matunitlindflem2  38301  ptrest  38303  poimirlem25  38329  poimirlem27  38331  poimirlem30  38334  ismblfin  38345  ovoliunnfl  38346  voliunnfl  38348  volsupnfl  38349  itg2addnclem2  38356  fdc  38429  prdstotbnd  38478  isdrngo1  38640  ispridl  38718  ismaxidl  38724  impor  38765  selconj  38782  tradd  38787  r2alan  38933  inxpss3  39002  idinxpssinxp2  39006  idinxpssinxp3  39007  dfrel5  39028  ineleq  39036  ralmo  39042  ralrnmo  39043  ralrmo3  39046  moantr  39054  dfxrn2  39067  inxpxrn  39100  rnxrnres  39104  dfsuccl4  39156  coss1cnvres  39189  1cossres  39201  cocossss  39208  cossssid4  39242  cossssid5  39243  cosscnvssid5  39250  cossid  39252  dfssr2  39261  cnvrefrelcoss2  39299  cosselcnvrefrels2  39300  eqvrelcoss  39383  eqvrelcoss2  39385  dfcoeleqvrel  39388  refrelredund4  39401  cnvepresdmqs  39420  dfcomember  39439  dfdisjALTV  39480  disjimdmqseq  39491  dfeldisj3  39493  dfeldisj4  39494  dfeldisj5  39495  disjres  39526  prter1  39686  islshp  39786  islshpat  39824  lcvbr2  39829  lcvnbtwn2  39834  cvrnbtwn3  40083  isatl  40106  ishlat1  40159  ishlat2  40160  cvrat4  40250  pmapglbx  40576  lhpexle3  40819  dib1dim  41972  diblsmopel  41978  lcfls1lem  42341  prjsperref  43371  prjspeclsp  43377  euabsn2w  43444  rexrabdioph  43554  dford4  43789  onsupuni  43989  dflim6  44024  tfsconcatlem  44096  naddgeoa  44154  ifpdfor2  44220  ifpdfan2  44222  ifpdfor  44224  ifpdfan  44225  ifpnot23b  44241  ifpnot23c  44243  ifpnot23d  44244  ifpim123g  44259  ifpbibib  44269  clss2lem  44370  imaiun1  44410  coiun1  44411  brfvrcld2  44451  iunrelexp0  44461  brtrclfv2  44486  snhesn  44545  dffrege76  44698  frege97  44719  frege98  44720  frege109  44731  frege110  44732  dffrege115  44737  frege131  44753  frege133  44755  ntrneineine1lem  44843  ntrneiel2  44845  ntrneiiso  44850  gneispace3  44892  ismnuprim  45037  ismnushort  45044  dfuniv2  45045  pm11.52  45130  pm11.58  45133  pm13.192  45153  impexpdcom  45257  sbc3or  45274  opelopab4  45293  uunT12p1  45541  uunT12p2  45542  uunT12p3  45543  uun2221  45554  uun2221p1  45555  uun2221p2  45556  undif3VD  45623  modelaxreplem3  45722  permaxext  45747  permac8prim  45756  ndisj2  45804  rabssf  45870  bothtbothsame  47669  bothfbothsame  47670  aiffbtbat  47678  reuabaiotaiota  47857  2reu8i  47883  2reuimp0  47884  ichn  48238  dfodd2  48434  dfeven5  48464  dfodd7  48465  1nevenALTV  48489  oddprmne2  48513  dfvopnbgr2  48651  isuspgrim0lem  48691  gpg5nbgrvtx03starlem1  48866  gpg5nbgrvtx03starlem2  48867  gpg5nbgrvtx03starlem3  48868  gpg5nbgrvtx13starlem1  48869  gpg5nbgrvtx13starlem2  48870  gpg5nbgrvtx13starlem3  48871  gpg5edgnedg  48928  dfidom2  49141  islindeps2  49296  isldepslvec2  49298  line2xlem  49566  rmotru  49614  reutru  49615  isnrm4  49742  iscnrm4  49765  homf0  49820  fuco2el  50123  isthincd2  50248  thinccic  50282  istermc2  50286  istermc3  50287  dftermc3  50342  setrec1lem3  50500  dfrals2  50601  dfralseu2  50634  aacllem  50654