Theorem bitr4i 278

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

Syntax hints:   ↔ wb 206

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 207

This theorem is referenced by:  3bitr2i  299  3bitr2ri  300  3bitr4i  303  3bitr4ri  304  biluk  385  biancomi  462  dfbi2  474  imdistan  567  pm5.32  573  bianass  642  mpbiran  709  biadaniALT  820  imor  853  imimorb  952  pm5.6  1003  nbi2  1017  casesifp  1077  3ancoma  1097  3ancomb  1098  3anrev  1100  dfnan2  1494  nannan  1497  nanbi  1500  xorcom  1514  xorneg  1523  xorbi12i  1524  norcom  1530  noran  1532  norasslem1  1534  trunortru  1589  trunorfal  1590  cadan  1609  cadcomb  1613  nic-ax  1673  nic-axALT  1674  nf3  1786  19.43  1882  equsv  2002  sbrimvw  2091  sbcom2  2173  sb5  2276  nf5  2282  nf6  2283  sbrim  2304  sbnf  2312  sb6x  2468  2sb5rf  2476  2sb6rf  2477  sb4b  2479  sb5f  2502  sbequ8  2505  sbhb  2525  eu6lem  2572  eu1  2609  iseqsetv-cleq  2799  issettru  2812  iseqsetv-clel  2813  issetlem  2814  cleqh  2864  cleqf  2927  sbabel  2931  necon3bii  2984  neor  3024  neorian  3027  rextru  3067  r19.26m  3097  r19.43  3108  3r19.43  3109  r2allem  3128  r19.23t  3238  ralcom4  3268  rexcomOLD  3272  moel  3381  moelOLD  3384  rabid2f  3447  rabid2OLD  3450  eqv  3469  eqvf  3470  ralv  3487  rexv  3488  reuv  3489  rmov  3490  rexcom4b  3492  ceqsex4v  3517  ceqsex8v  3519  ceqsrexv  3634  rexab  3678  ralrab2  3681  rexrab2  3683  reu2  3708  reu3  3710  reueq  3720  2reuswap  3729  2reuswap2  3730  reuind  3736  2reu5lem3  3740  2rmoswap  3744  rmo2  3862  rmoanim  3869  rmoanimALT  3870  dfss3  3947  dfss3f  3950  ssabral  4040  rabss  4047  ssrabeq  4059  uniiunlem  4062  sspsstri  4080  npss  4088  dfdif3OLD  4093  raldifb  4124  uncom  4133  inass  4203  elsymdifxor  4235  nsspssun  4243  dfss4  4244  dfun2  4245  dfin2  4246  indi  4259  reupick3  4305  eq0f  4322  neq0f  4323  eq0  4325  eq0ALT  4326  dfnf5  4357  rabn0  4364  csbab  4415  vss  4421  disj  4425  disj3  4429  undisj1  4437  undisj2  4438  inundif  4454  undif  4457  undifr  4458  rabsssn  4644  exsnrex  4656  euabsn2  4701  euabsn  4702  raldifsni  4771  tppreqb  4781  pwpw0  4789  prssg  4795  ssunsn  4804  prneimg2  4831  preqsn  4838  pwpr  4877  dfuni2  4885  unissb  4915  unissbOLD  4916  elint2  4929  ssint  4940  uniintab  4962  dfiin2g  5008  iunid  5036  iunn0  5043  iunxun  5070  iunxiun  5073  iinpw  5082  disjor  5101  disjxiun  5116  dftr2  5231  dftr5OLD  5234  dftr3  5235  dftr4  5236  axrep6OLD  5259  vnex  5284  inuni  5320  eusv2  5366  reusv2lem4  5371  rexxfr  5386  sspwb  5424  opthneg  5456  pwssun  5545  dfid3  5551  dffr6  5609  dffr2  5615  dffr2ALT  5616  opthprc  5718  elxp3  5720  xpiundir  5726  elvv  5729  reliun  5795  inxpOLD  5812  raliunxp  5819  cnvuni  5866  dmopab2rex  5897  dm0rn0  5904  dfres3  5971  ssdmres  6000  elidinxp  6031  idinxpres  6034  dfima2  6049  args  6079  dffr3  6086  cotrg  6096  cotrgOLD  6097  cotrgOLDOLD  6098  intasym  6104  asymref  6105  intirr  6107  xpnz  6148  xp11  6164  ssrnres  6167  xpimasn  6174  coiun  6245  coass  6254  cnvso  6277  elsnxp  6280  dfpo2  6285  imaindm  6288  dffr4  6309  dfse3  6325  frpoind  6331  wfiOLD  6340  dflim2  6410  orddif  6449  dffun2OLDOLD  6542  dffun6  6543  dffun6f  6548  dffun7  6562  dffun9  6564  funfn  6565  svrelfun  6607  mptfnf  6672  dffn2  6707  dffn3  6717  fint  6756  dffn4  6795  dff1o4  6825  brprcneu  6865  brprcneuALT  6866  eqfnfv3  7022  fnreseql  7037  fsn  7124  ftpg  7145  abrexco  7235  imaiun  7236  dff13  7246  isof1oidb  7316  isof1oopb  7317  isocnv2  7323  eloprabga  7514  mpo2eqb  7537  elovmpo  7650  sorpss  7720  abexex  7968  elxp6  8020  elxp7  8021  releldm2  8040  opiota  8056  fnmpo  8066  frxp  8123  frxp2  8141  soseq  8156  cnvimadfsn  8169  mpoxneldm  8209  dftpos4  8242  frrlem9  8291  wfrlem8OLD  8328  wfrfunOLD  8331  dfrecs3  8384  dfrecs3OLD  8385  tfrlem7  8395  ondif1  8511  oarec  8572  oeeu  8613  brinxper  8746  0er  8755  eroveu  8824  erovlem  8825  elixpconst  8917  domen  8974  brsdom  8987  brdom2  8994  reuen1  9038  sbthlem10  9104  brsdom2  9109  xpf1o  9151  unfi  9183  sbthfilem  9210  onfin2  9238  0sdom1domALT  9245  modom  9250  marypha2lem3  9447  wemapsolem  9562  elom3  9660  dfom5  9662  brttrcl2  9726  ttrcltr  9728  ttrclse  9739  trcl  9740  epfrs  9743  frind  9762  rankf  9806  scottexs  9899  scott0s  9900  cplem1  9901  hta  9909  djuexb  9921  pm54.43lem  10012  alephsuc2  10092  iscard3  10105  aceq0  10130  aceq3lem  10132  dfac3  10133  dfac5lem2  10136  dfac5  10141  dfac7  10145  dfac12a  10161  kmlem12  10174  kmlem14  10176  kmlem15  10177  infmap2  10229  ackbij2  10254  dfacfin7  10411  ituniiun  10434  zorng  10516  brdom7disj  10543  entri2  10570  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  1re  11233  infm3  12199  elnnz  12596  dfz2  12605  2rexuz  12914  nnwos  12929  eluz2b1  12933  qexALT  12978  elxr  13130  dflt2  13162  xrsupss  13323  xrinfmss  13324  elixx1  13369  elioo2  13401  dfrp2  13409  elioopnf  13458  elicopnf  13460  elfz1  13527  fznn  13607  fzp1nel  13626  fznn0  13634  preduz  13665  prinfzo0  13713  injresinj  13802  nn0opthlem1  14284  faclbnd4lem1  14309  hashfxnn0  14353  hashprdifel  14414  hashgt23el  14440  hashfun  14453  hashf1  14473  fz1isolem  14477  f1oun2prg  14934  brtrclfv  15019  shftdm  15088  rediv  15148  imdiv  15155  rexanre  15363  caubnd  15375  climreu  15570  prodmo  15950  dvdslelem  16326  3dvdsdec  16349  3dvds2dec  16350  bitsval  16441  smueqlem  16507  algcvgblem  16594  lcmfunsnlem2  16657  isprm2  16699  isprm3  16700  isprm4  16701  pythagtriplem2  16835  elgz  16949  hashbc0  17023  0ram  17038  isstruct  17169  issect  17764  isfull2  17924  isfth2  17928  fucinv  17987  eldmcoa  18076  isdrs  18311  submacs  18803  isnsg4  19148  isgim  19243  gaorb  19288  oppgid  19337  oppgsubm  19343  oppgcntz  19345  ispgp  19571  efgsdm  19709  efgcpbllema  19733  iscyg2  19861  isrng  20112  isring  20195  isirred2  20379  opprirred  20380  isrnghm  20399  dfrhm2  20432  isnzr2  20476  opprsubrng  20517  opprsubrg  20551  isdomn3  20673  drngid2  20710  issdrg  20746  islmod  20819  lss1d  20918  islmhm  20983  islmim  21018  lbsextlem2  21118  lidlnz  21201  dfprm2  21432  isphl  21586  elocv  21626  iunocv  21639  isobs  21678  islinds  21767  1mavmul  22484  toprntopon  22861  isbasis3g  22885  fctop  22940  cctop  22942  isclo2  23024  restsn  23106  lmbr  23194  ist0-3  23281  2ndcdisj  23392  1stccnp  23398  islocfin  23453  1stckgenlem  23489  txbas  23503  ptbasin  23513  tx2cn  23546  fbfinnfr  23777  fbasrn  23820  filuni  23821  ufinffr  23865  fin1aufil  23868  rnelfmlem  23888  flimrest  23919  alexsubALTlem3  23985  alexsubALTlem4  23986  tgphaus  24053  istlm  24121  iscusp2  24238  metuel2  24502  isngp2  24534  isnlm  24612  isphtpc  24942  phtpcer  24943  om1elbas  24981  isclm  25013  iscvsp  25077  iscph  25120  iscau3  25228  minveclem3b  25378  elovolm  25426  ioombl1lem4  25512  dyaddisj  25547  vitali  25564  itg1climres  25665  itg2seq  25693  itg2monolem1  25701  itg2mono  25704  limcrcl  25825  lhop1  25969  itgsubst  26006  mdegleb  26019  isuc1p  26096  ismon1p  26098  plydivex  26255  ellogdm  26598  1cubr  26802  atandm2  26837  birthdaylem3  26913  dmarea  26917  dchrelbas2  27198  dchrelbas4  27204  elno3  27617  nosgnn0  27620  nosepon  27627  nocvxminlem  27739  scutcut  27763  scutbday  27766  dmscut  27773  scutf  27774  sltrec  27782  made0  27829  addsprop  27926  negsproplem2  27978  negsprop  27984  mulsprop  28073  precsexlem10  28157  elzs2  28302  elnnzs  28304  recut  28345  0reno  28346  axcontlem7  28895  nb3grpr  29307  nb3grpr2  29308  upgrwlkcompim  29569  wlkson  29582  wlkonprop  29584  wksonproplem  29630  wksonproplemOLD  29631  ispth  29649  wwlknon  29785  wwlksnextinj  29827  wspthsnwspthsnon  29844  elwspths2spth  29895  rusgrnumwwlkl1  29896  clwwlkccatlem  29916  erclwwlkref  29947  frgr3v  30202  nmoubi  30699  nmobndseqi  30706  nmobndseqiALT  30707  minvecolem1  30801  isch2  31150  hlimreui  31166  isch3  31168  ocsh  31210  dfch2  31334  spanuni  31471  nonbooli  31578  5oalem7  31587  adjsym  31760  elbdop2  31798  dmadjss  31814  nmopub  31835  nmfnleub  31852  nmop0h  31918  pjssposi  32099  pjordi  32100  cvbr2  32210  cvnbtwn2  32214  mdsl2i  32249  cvmdi  32251  elat2  32267  atom1d  32280  chirredi  32321  cdj3i  32368  or3di  32386  opreu2reu1  32411  mo5f  32416  reuxfrdf  32418  rexunirn  32419  difrab2  32425  rabsspr  32428  rabsstp  32429  tpssg  32464  iuninc  32487  disjorf  32506  disjunsn  32521  rabfmpunirn  32577  aciunf1  32587  funcnv5mpt  32592  eliccelico  32700  elicoelioo  32701  isomnd  33015  omndmul2  33026  isslmd  33145  islinds5  33328  ismxidl  33423  1arithufdlem4  33508  hasheuni  34062  pwsiga  34107  sigainb  34113  issros  34152  2ndmbfm  34239  omssubaddlem  34277  omssubadd  34278  sitgaddlemb  34326  eulerpartlemgvv  34354  eulerpartlemn  34359  probun  34397  ballotlem2  34467  ballotlemodife  34476  bnj252  34680  bnj253  34681  bnj255  34682  bnj345  34691  bnj133  34704  bnj976  34754  bnj1098  34760  bnj121  34847  bnj130  34851  bnj150  34853  bnj581  34885  bnj607  34893  bnj865  34900  bnj917  34911  bnj934  34912  bnj964  34920  bnj983  34928  bnj996  34933  bnj1021  34943  bnj1033  34946  bnj1047  34950  bnj1049  34951  bnj1090  34956  bnj1128  34967  bnj1175  34981  bnj1189  34986  bnj1253  34994  bnj1312  35035  exdifsn  35056  fineqvrep  35072  fineqvac  35074  erdszelem9  35167  erdszelem10  35168  pconnconn  35199  cvmliftiota  35269  fmlaomn0  35358  fmla0disjsuc  35366  fmlasucdisj  35367  dmopab3rexdif  35373  elmthm  35544  nepss  35681  xpab  35689  dfso2  35718  elrn3  35725  elpotr  35745  dfon2lem5  35751  dfon2lem7  35753  dfon2lem8  35754  elwlim  35787  wzel  35788  brtxp2  35845  brpprod3a  35850  eltrans  35855  dfon3  35856  dffix2  35869  dffun10  35878  elfuns  35879  brsingle  35881  brimg  35901  funpartfun  35907  funpartfv  35909  cgrxfr  36019  segletr  36078  outsideoftr  36093  neifg  36335  filnetlem4  36345  df3nandALT1  36363  weiunlem2  36427  bj-consensusALT  36543  bj-df-ifc  36544  bj-biexal3  36671  bj-nfnnfTEMP  36722  bj-denoteslem  36835  bj-denotesALTV  36836  bj-ralvw  36843  bj-rexvw  36844  bj-rexcom4bv  36846  bj-rexcom4b  36847  bj-sbeq  36865  bj-inrab  36891  bj-rcleqf  36989  bj-dfmpoa  37082  bj-imdirco  37154  topdifinffinlem  37311  topdifinfeq  37314  relowlssretop  37327  relowlpssretop  37328  rdgeqoa  37334  domalom  37368  nlpineqsn  37372  fvineqsneq  37376  wl-ifpimpr  37430  wl-df3xor3  37434  wl-3xorbi  37437  wl-3xorbi2  37438  wl-2xor  37447  wl-2mintru2  37455  wl-dfclab  37560  rabiun  37563  phpreu  37574  fin2solem  37576  matunitlindflem2  37587  ptrest  37589  poimirlem25  37615  poimirlem27  37617  poimirlem30  37620  ismblfin  37631  ovoliunnfl  37632  voliunnfl  37634  volsupnfl  37635  itg2addnclem2  37642  fdc  37715  prdstotbnd  37764  isdrngo1  37926  ispridl  38004  ismaxidl  38010  impor  38051  selconj  38070  tradd  38075  scott0f  38139  r2alan  38213  inxpss3  38278  idinxpssinxp2  38282  idinxpssinxp3  38283  dfrel5  38310  ineleq  38318  moantr  38328  dfxrn2  38340  inxpxrn  38359  rnxrnres  38363  coss1cnvres  38381  1cossres  38393  cocossss  38400  cossssid4  38434  cossssid5  38435  cosscnvssid5  38442  cossid  38444  dfssr2  38463  cnvrefrelcoss2  38501  cosselcnvrefrels2  38502  eqvrelcoss  38581  eqvrelcoss2  38583  dfcoeleqvrel  38586  refrelredund4  38599  cnvepresdmqs  38617  dfcomember  38636  dfdisjALTV  38677  dfeldisj3  38683  dfeldisj4  38684  dfeldisj5  38685  disjres  38708  prter1  38843  islshp  38943  islshpat  38981  lcvbr2  38986  lcvnbtwn2  38991  cvrnbtwn3  39240  isatl  39263  ishlat1  39316  ishlat2  39317  cvrat4  39408  pmapglbx  39734  lhpexle3  39977  dib1dim  41130  diblsmopel  41136  lcfls1lem  41499  prjsperref  42576  prjspeclsp  42582  euabsn2w  42649  rexrabdioph  42764  dford4  43000  onsupuni  43200  dflim6  43235  tfsconcatlem  43307  naddgeoa  43365  ifpdfor2  43432  ifpdfan2  43434  ifpdfor  43436  ifpdfan  43437  ifpnot23b  43453  ifpnot23c  43455  ifpnot23d  43456  ifpim123g  43471  ifpbibib  43481  clss2lem  43582  imaiun1  43622  coiun1  43623  brfvrcld2  43663  iunrelexp0  43673  brtrclfv2  43698  snhesn  43757  dffrege76  43910  frege97  43931  frege98  43932  frege109  43943  frege110  43944  dffrege115  43949  frege131  43965  frege133  43967  ntrneineine1lem  44055  ntrneiel2  44057  ntrneiiso  44062  gneispace3  44104  scotteld  44218  ismnuprim  44266  ismnushort  44273  dfuniv2  44274  pm11.52  44359  pm11.58  44362  pm13.192  44382  impexpdcom  44488  sbc3or  44505  opelopab4  44524  uunT12p1  44772  uunT12p2  44773  uunT12p3  44774  uun2221  44785  uun2221p1  44786  uun2221p2  44787  undif3VD  44854  modelaxreplem3  44953  permaxext  44978  ndisj2  45023  nssrex  45058  rabssf  45091  bothtbothsame  46876  bothfbothsame  46877  aiffbtbat  46885  reuabaiotaiota  47064  2reu8i  47090  2reuimp0  47091  ichn  47418  dfodd2  47598  dfeven5  47628  dfodd7  47629  1nevenALTV  47653  oddprmne2  47677  dfvopnbgr2  47814  isuspgrim0lem  47854  gpg5nbgrvtx03starlem1  48018  gpg5nbgrvtx03starlem2  48019  gpg5nbgrvtx03starlem3  48020  gpg5nbgrvtx13starlem1  48021  gpg5nbgrvtx13starlem2  48022  gpg5nbgrvtx13starlem3  48023  islindeps2  48407  isldepslvec2  48409  line2xlem  48681  rmotru  48730  reutru  48731  isnrm4  48853  iscnrm4  48876  homf0  48932  fuco2el  49171  isthincd2  49271  thinccic  49305  istermc2  49309  istermc3  49310  dftermc3  49364  setrec1lem3  49501  aacllem  49613