Theorem bitr4i 279

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

Syntax hints:   ↔ wb 207

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 208

This theorem is referenced by:  3bitr2i  300  3bitr2ri  301  3bitr4i  304  3bitr4ri  305  biluk  386  biancomi  463  dfbi2  475  imdistan  572  pm5.32  578  bianass  648  mpbiran  715  biadaniALT  826  imor  859  imimorb  958  pm5.6  1009  nbi2  1023  casesifp  1083  3ancoma  1103  3ancomb  1104  3anrev  1106  dfnan2  1501  nannan  1504  nanbi  1507  xorcom  1521  xorneg  1530  xorbi12i  1531  norcom  1537  noran  1539  norasslem1  1541  trunortru  1596  trunorfal  1597  cadan  1616  cadcomb  1620  nic-ax  1680  nic-axALT  1681  nf3  1793  19.43  1889  equsv  2010  sbrimvw  2102  sbcom2  2183  sb5  2287  nf5  2293  nf6  2294  sbrim  2315  sbnf  2322  sb6x  2472  2sb5rf  2480  2sb6rf  2481  sb4b  2483  sb5f  2506  sbequ8  2509  sbhb  2529  eu6lem  2577  eu1  2614  iseqsetv-cleq  2804  issettru  2818  iseqsetv-clel  2819  issetlem  2820  cleqh  2869  cleqf  2930  sbabel  2934  necon3bii  2987  neor  3027  neorian  3030  rextru  3071  r19.26m  3099  r19.43  3108  3r19.43  3109  r2allem  3128  r19.23t  3236  ralcom4  3266  moel  3365  rabid2f  3423  eqv  3442  eqvf  3443  ralv  3459  rexv  3460  reuv  3461  rmov  3462  rexcom4b  3464  ceqsex4v  3487  ceqsex8v  3489  ceqsrexv  3600  rexab  3643  ralrab2  3646  rexrab2  3648  reu2  3673  reu3  3675  reueq  3685  2reuswap  3694  2reuswap2  3695  reuind  3701  2reu5lem3  3705  2rmoswap  3709  rmo2  3826  rmoanim  3833  rmoanimALT  3834  dfss3  3911  dfss3f  3914  ssabral  4002  rabss  4008  ssrabeq  4022  uniiunlem  4025  sspsstri  4043  npss  4051  dfdif3OLD  4056  raldifb  4086  uncom  4095  inass  4163  elsymdifxor  4195  nsspssun  4203  dfss4  4204  dfun2  4205  dfin2  4206  indi  4219  reupick3  4265  eq0f  4282  neq0f  4283  eq0ALT  4286  dfnf5  4317  rabn0  4324  csbab  4375  vss  4381  disj  4385  disj3  4389  undisj1  4397  undisj2  4398  inundif  4414  undif  4417  undifr  4418  rabsssn  4607  exsnrex  4619  euabsn2  4664  euabsn  4665  raldifsni  4735  tppreqb  4745  pwpw0  4751  prssg  4757  ssunsn  4766  prneimg2  4793  preqsn  4800  pwpr  4839  dfuni2  4847  unissb  4878  elint2  4891  ssint  4901  uniintab  4923  dfiin2g  4967  iunid  4997  iunn0  5003  iunxun  5030  iunxiun  5033  iinpw  5042  disjor  5061  disjxiun  5076  dftr2  5188  dftr3  5191  dftr4  5192  axrep6OLD  5216  vnexOLD  5247  inuni  5285  eusv2  5332  reusv2lem4  5337  rexxfr  5352  sspwb  5395  opthneg  5428  pwssun  5517  dfid3  5523  dffr6  5581  dffr2  5586  dffr2ALT  5587  opthprc  5689  elxp3  5691  xpiundir  5697  elvv  5700  raliunxp  5788  cnvuni  5835  dmopab2rex  5866  dm0rn0OLD  5874  dfres3  5943  ssdmres  5972  elidinxp  6003  idinxpres  6006  dfima2  6021  args  6051  dffr3  6058  cotrg  6068  intasym  6072  asymref  6073  intirr  6075  xpnz  6117  xp11  6133  ssrnres  6136  xpimasn  6143  coiun  6215  coass  6224  cnvso  6246  elsnxp  6249  dfpo2  6254  imaindm  6257  dffr4  6278  dfse3  6294  frpoind  6300  dflim2  6375  orddif  6415  dffun6  6503  dffun6f  6507  dffun7  6519  dffun9  6521  funfn  6522  svrelfun  6564  mptfnf  6627  dffn2  6664  dffn3  6674  fint  6713  dffn4  6752  dff1o4  6782  brprcneu  6824  brprcneuALT  6825  eqfnfv3  6980  fnreseql  6996  fsn  7084  ftpg  7106  abrexco  7195  imaiun  7196  dff13  7205  isof1oidb  7275  isof1oopb  7276  isocnv2  7282  eloprabga  7472  mpo2eqb  7495  elovmpo  7608  sorpss  7678  abexex  7920  elxp6  7972  elxp7  7973  releldm2  7992  opiota  8008  fnmpo  8018  frxp  8073  frxp2  8091  soseq  8106  cnvimadfsn  8119  mpoxneldm  8159  dftpos4  8192  frrlem9  8241  dfrecs3  8309  tfrlem7  8319  ondif1  8433  oarec  8494  oeeu  8536  brinxper  8670  0er  8679  eroveu  8756  erovlem  8757  elixpconst  8850  domen  8905  brsdom  8918  brdom2  8926  reuen1  8970  sbthlem10  9031  brsdom2  9036  xpf1o  9074  unfi  9102  sbthfilem  9129  onfin2  9148  0sdom1domALT  9154  modom  9158  marypha2lem3  9347  wemapsolem  9462  elom3  9567  dfom5  9569  brttrcl2  9633  ttrcltr  9635  ttrclse  9646  trcl  9647  epfrs  9650  frind  9672  rankf  9716  scottexs  9809  scott0s  9810  cplem1  9811  hta  9819  djuexb  9831  pm54.43lem  9922  alephsuc2  10000  iscard3  10013  aceq0  10038  aceq3lem  10040  dfac3  10041  dfac5lem2  10044  dfac5  10049  dfac7  10053  dfac12a  10069  kmlem12  10082  kmlem14  10084  kmlem15  10085  infmap2  10137  ackbij2  10162  dfacfin7  10319  ituniiun  10342  zorng  10424  brdom7disj  10451  entri2  10478  alephreg  10503  fpwwe2lem11  10562  fpwwe2lem12  10563  pwfseqlem1  10579  grutsk  10743  axgroth4  10753  grothprim  10755  grothtsk  10756  elni2  10798  ltsopi  10809  genpass  10930  psslinpr  10952  ltexprlem4  10960  ltresr  11061  infm3  12113  elnnz  12532  dfz2  12541  2rexuz  12848  nnwos  12863  eluz2b1  12867  qexALT  12912  elxr  13065  dflt2  13097  xrsupss  13259  xrinfmss  13260  elixx1  13305  elioo2  13337  dfrp2  13345  elioopnf  13394  elicopnf  13396  elfz1  13464  fznn  13544  fzp1nel  13563  fznn0  13571  preduz  13602  prinfzo0  13651  injresinj  13744  nn0opthlem1  14228  faclbnd4lem1  14253  hashfxnn0  14297  hashprdifel  14358  hashgt23el  14384  hashfun  14397  hashf1  14417  fz1isolem  14421  f1oun2prg  14877  brtrclfv  14962  shftdm  15031  rediv  15091  imdiv  15098  rexanre  15307  caubnd  15319  climreu  15516  prodmo  15899  dvdslelem  16276  3dvdsdec  16299  3dvds2dec  16300  bitsval  16391  smueqlem  16457  algcvgblem  16544  lcmfunsnlem2  16607  isprm2  16649  isprm3  16650  isprm4  16651  pythagtriplem2  16786  elgz  16900  hashbc0  16974  0ram  16989  isstruct  17120  issect  17718  isfull2  17878  isfth2  17882  fucinv  17941  eldmcoa  18030  isdrs  18265  submacs  18793  isnsg4  19140  isgim  19235  gaorb  19280  oppgid  19329  oppgsubm  19335  oppgcntz  19337  ispgp  19565  efgsdm  19703  efgcpbllema  19727  iscyg2  19855  isomnd  20096  omndmul2  20106  isrng  20133  isring  20216  isirred2  20399  opprirred  20400  isrnghm  20419  dfrhm2  20452  isnzr2  20497  opprsubrng  20538  opprsubrg  20572  isdomn3  20694  drngid2  20731  issdrg  20767  islmod  20861  lss1d  20960  islmhm  21024  islmim  21059  lbsextlem2  21159  lidlnz  21242  dfprm2  21455  isphl  21610  elocv  21650  iunocv  21663  isobs  21702  islinds  21791  1mavmul  22538  toprntopon  22915  isbasis3g  22939  fctop  22994  cctop  22996  isclo2  23078  restsn  23160  lmbr  23248  ist0-3  23335  2ndcdisj  23446  1stccnp  23452  islocfin  23507  1stckgenlem  23543  txbas  23557  ptbasin  23567  tx2cn  23600  fbfinnfr  23831  fbasrn  23874  filuni  23875  ufinffr  23919  fin1aufil  23922  rnelfmlem  23942  flimrest  23973  alexsubALTlem3  24039  alexsubALTlem4  24040  tgphaus  24107  istlm  24175  iscusp2  24291  metuel2  24555  isngp2  24587  isnlm  24665  isphtpc  24986  phtpcer  24987  om1elbas  25024  isclm  25056  iscvsp  25120  iscph  25162  iscau3  25270  minveclem3b  25420  elovolm  25467  ioombl1lem4  25553  dyaddisj  25588  vitali  25605  itg1climres  25706  itg2seq  25734  itg2monolem1  25742  itg2mono  25745  limcrcl  25866  lhop1  26006  itgsubst  26041  mdegleb  26054  isuc1p  26131  ismon1p  26133  plydivex  26288  ellogdm  26628  1cubr  26831  atandm2  26866  birthdaylem3  26942  dmarea  26946  dchrelbas2  27225  dchrelbas4  27231  elno3  27644  nosgnn0  27647  nosepon  27654  nocvxminlem  27771  cutcuts  27798  cutbday  27801  dmcuts  27808  cutsf  27809  ltsrec  27818  made0  27880  addsprop  27993  negsproplem2  28046  negsprop  28052  mulsprop  28147  precsexlem10  28233  elzs2  28416  elnnzs  28418  bdayfinbndlem1  28484  recut  28511  axcontlem7  29064  nb3grpr  29476  nb3grpr2  29477  upgrwlkcompim  29736  wlkson  29748  wlkonprop  29750  wksonproplem  29796  ispth  29814  wwlknon  29950  wwlksnextinj  29992  wspthsnwspthsnon  30009  elwspths2spth  30063  rusgrnumwwlkl1  30064  clwwlkccatlem  30084  erclwwlkref  30115  frgr3v  30370  nmoubi  30868  nmobndseqi  30875  nmobndseqiALT  30876  minvecolem1  30970  isch2  31319  hlimreui  31335  isch3  31337  ocsh  31379  dfch2  31503  spanuni  31640  nonbooli  31747  5oalem7  31756  adjsym  31929  elbdop2  31967  dmadjss  31983  nmopub  32004  nmfnleub  32021  nmop0h  32087  pjssposi  32268  pjordi  32269  cvbr2  32379  cvnbtwn2  32383  mdsl2i  32418  cvmdi  32420  elat2  32436  atom1d  32449  chirredi  32490  cdj3i  32537  or3di  32553  opreu2reu1  32578  mo5f  32583  reuxfrdf  32585  rexunirn  32586  difrab2  32592  rabsspr  32596  rabsstp  32597  tpssg  32632  iuninc  32656  disjorf  32675  disjunsn  32690  rabfmpunirn  32752  aciunf1  32762  funcnv5mpt  32766  eliccelico  32876  elicoelioo  32877  isslmd  33290  islinds5  33457  ismxidl  33552  1arithufdlem4  33637  hasheuni  34276  pwsiga  34321  sigainb  34327  issros  34366  2ndmbfm  34452  omssubaddlem  34490  omssubadd  34491  sitgaddlemb  34539  eulerpartlemgvv  34567  eulerpartlemn  34572  probun  34610  ballotlem2  34680  ballotlemodife  34689  bnj252  34893  bnj253  34894  bnj255  34895  bnj345  34904  bnj133  34917  bnj976  34967  bnj1098  34973  bnj121  35059  bnj130  35063  bnj150  35065  bnj581  35097  bnj607  35105  bnj865  35112  bnj917  35123  bnj934  35124  bnj964  35132  bnj983  35140  bnj996  35145  bnj1021  35155  bnj1033  35158  bnj1047  35162  bnj1049  35163  bnj1090  35168  bnj1128  35179  bnj1175  35193  bnj1189  35198  bnj1253  35206  bnj1312  35247  exdifsn  35268  fineqvrep  35302  fineqvac  35304  onvf1odlem4  35341  vonf1owev  35343  erdszelem9  35434  erdszelem10  35435  pconnconn  35466  cvmliftiota  35536  fmlaomn0  35625  fmla0disjsuc  35633  fmlasucdisj  35634  dmopab3rexdif  35640  elmthm  35811  antnestALT  35929  nepss  35953  xpab  35961  dfso2  35990  elrn3  35997  elpotr  36014  dfon2lem5  36020  dfon2lem7  36022  dfon2lem8  36023  elwlim  36056  wzel  36057  brtxp2  36114  brpprod3a  36119  eltrans  36124  dfon3  36125  dffix2  36138  dffun10  36147  elfuns  36148  brsingle  36150  brimg  36170  funpartfun  36178  funpartfv  36180  cgrxfr  36290  segletr  36349  outsideoftr  36364  neifg  36606  filnetlem4  36616  df3nandALT1  36634  weiunlem  36698  ttcwf3  36761  bj-consensusALT  36897  bj-df-ifc  36898  bj-exexalal  36924  bj-cbvaew  36991  bj-biexal3  37057  bj-alnnf  37087  bj-nfnnfTEMP  37132  bj-denoteslem  37231  bj-denotesALTV  37232  bj-ralvw  37239  bj-rexvw  37240  bj-rexcom4bv  37242  bj-rexcom4b  37243  bj-sbeq  37261  bj-inrab  37287  bj-rcleqf  37385  bj-dfmpoa  37483  bj-imdirco  37557  topdifinffinlem  37716  topdifinfeq  37719  relowlssretop  37732  relowlpssretop  37733  rdgeqoa  37739  domalom  37773  nlpineqsn  37777  fvineqsneq  37781  wl-ifpimpr  37835  wl-df3xor3  37839  wl-3xorbi  37842  wl-3xorbi2  37843  wl-2xor  37852  wl-2mintru2  37860  wl-dfclab  37963  rabiun  37967  phpreu  37978  fin2solem  37980  matunitlindflem2  37991  ptrest  37993  poimirlem25  38019  poimirlem27  38021  poimirlem30  38024  ismblfin  38035  ovoliunnfl  38036  voliunnfl  38038  volsupnfl  38039  itg2addnclem2  38046  fdc  38119  prdstotbnd  38168  isdrngo1  38330  ispridl  38408  ismaxidl  38414  impor  38455  selconj  38474  tradd  38479  scott0f  38543  r2alan  38625  inxpss3  38694  idinxpssinxp2  38698  idinxpssinxp3  38699  dfrel5  38720  ineleq  38728  ralmo  38734  ralrnmo  38735  ralrmo3  38738  moantr  38746  dfxrn2  38759  inxpxrn  38792  rnxrnres  38796  dfsuccl4  38848  coss1cnvres  38881  1cossres  38893  cocossss  38900  cossssid4  38934  cossssid5  38935  cosscnvssid5  38942  cossid  38944  dfssr2  38953  cnvrefrelcoss2  38991  cosselcnvrefrels2  38992  eqvrelcoss  39075  eqvrelcoss2  39077  dfcoeleqvrel  39080  refrelredund4  39093  cnvepresdmqs  39112  dfcomember  39131  dfdisjALTV  39172  disjimdmqseq  39183  dfeldisj3  39185  dfeldisj4  39186  dfeldisj5  39187  disjres  39218  prter1  39378  islshp  39478  islshpat  39516  lcvbr2  39521  lcvnbtwn2  39526  cvrnbtwn3  39775  isatl  39798  ishlat1  39851  ishlat2  39852  cvrat4  39942  pmapglbx  40268  lhpexle3  40511  dib1dim  41664  diblsmopel  41670  lcfls1lem  42033  prjsperref  43063  prjspeclsp  43069  euabsn2w  43136  rexrabdioph  43246  dford4  43481  onsupuni  43681  dflim6  43716  tfsconcatlem  43788  naddgeoa  43846  ifpdfor2  43912  ifpdfan2  43914  ifpdfor  43916  ifpdfan  43917  ifpnot23b  43933  ifpnot23c  43935  ifpnot23d  43936  ifpim123g  43951  ifpbibib  43961  clss2lem  44062  imaiun1  44102  coiun1  44103  brfvrcld2  44143  iunrelexp0  44153  brtrclfv2  44178  snhesn  44237  dffrege76  44390  frege97  44411  frege98  44412  frege109  44423  frege110  44424  dffrege115  44429  frege131  44445  frege133  44447  ntrneineine1lem  44535  ntrneiel2  44537  ntrneiiso  44542  gneispace3  44584  scotteld  44697  ismnuprim  44745  ismnushort  44752  dfuniv2  44753  pm11.52  44838  pm11.58  44841  pm13.192  44861  impexpdcom  44966  sbc3or  44983  opelopab4  45002  uunT12p1  45250  uunT12p2  45251  uunT12p3  45252  uun2221  45263  uun2221p1  45264  uun2221p2  45265  undif3VD  45332  modelaxreplem3  45431  permaxext  45456  permac8prim  45465  ndisj2  45506  nssrex  45540  rabssf  45573  bothtbothsame  47369  bothfbothsame  47370  aiffbtbat  47378  reuabaiotaiota  47557  2reu8i  47583  2reuimp0  47584  ichn  47938  dfodd2  48134  dfeven5  48164  dfodd7  48165  1nevenALTV  48189  oddprmne2  48213  dfvopnbgr2  48351  isuspgrim0lem  48391  gpg5nbgrvtx03starlem1  48566  gpg5nbgrvtx03starlem2  48567  gpg5nbgrvtx03starlem3  48568  gpg5nbgrvtx13starlem1  48569  gpg5nbgrvtx13starlem2  48570  gpg5nbgrvtx13starlem3  48571  gpg5edgnedg  48628  islindeps2  48981  isldepslvec2  48983  line2xlem  49251  rmotru  49300  reutru  49301  isnrm4  49428  iscnrm4  49451  homf0  49506  fuco2el  49809  isthincd2  49934  thinccic  49968  istermc2  49972  istermc3  49973  dftermc3  50028  setrec1lem3  50186  aacllem  50298