Theorem bitr4i 270

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

Syntax hints:   ↔ wb 198

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 199

This theorem is referenced by:  3bitr2i  291  3bitr2ri  292  3bitr4i  295  3bitr4ri  296  biluk  378  biancomi  455  dfbi2  467  imdistan  560  pm5.32  566  bianass  630  mpbiran  697  mpbiran2  698  biadanOLD  808  biadaniALT  810  imor  840  imimorb  934  pm5.6  985  nbi2  999  casesifp  1058  3ancoma  1080  3ancomb  1081  3anrev  1083  an3andi  1462  nanimn  1467  nancomOLD  1470  nannan  1471  nanbi  1476  xorneg  1501  cadan  1573  cadcomb  1577  nic-ax  1637  nic-axALT  1638  nf3  1750  nfnbi  1818  19.43  1846  19.3v  1940  equsv  1961  sb3an  2033  sb5OLD  2210  nf5  2217  nf6  2218  sb6x  2403  sbcom2  2411  sbcom2OLD  2412  2sb5rf  2419  2sb6rf  2420  sb4b  2424  sb5f  2460  sbequ8  2468  sbhb  2488  sb5ALT2  2514  sb5fALT  2531  eu6lem  2590  eu1  2642  eu1OLD  2643  euaeOLD  2694  cleqh  2884  clelab  2908  cleqf  2956  necon3bii  3014  neor  3054  neorian  3057  r19.26-3  3117  r19.26m  3118  r2allem  3145  r19.23t  3251  r19.43  3287  rexcom  3291  rabid2  3315  rabid2f  3316  eqv  3418  eqvf  3419  isset  3422  ralv  3435  rexv  3436  reuv  3437  rmov  3438  rexcom4b  3440  ceqsex4v  3462  ceqsex8v  3464  ceqsrexv  3558  ralrab2  3600  rexrab2  3602  reu2  3623  reu3  3625  reueq  3635  2reuswap  3644  2reuswap2  3645  reuind  3648  2reu5lem3  3652  2rmoswap  3656  sbc3an  3736  rmo2  3768  rmoanim  3776  rmoanimALT  3777  dfss2  3841  dfss3  3842  dfss3f  3845  ssabral  3927  rabss  3933  ssrabeq  3944  uniiunlem  3946  sspsstri  3964  npss  3972  dfdif3  3976  raldifb  4006  uncom  4013  inass  4078  elsymdifxor  4108  nsspssun  4116  dfss4  4117  dfun2  4118  dfin2  4119  indi  4132  indifdir  4142  difin2  4148  reupick3  4170  eq0f  4186  neq0f  4187  dfnf5  4215  rabn0  4220  csbab  4268  vss  4273  disj  4277  disj3  4281  undisj1  4289  undisj2  4290  inundif  4305  undif  4308  absn  4454  rabsssn  4476  exsnrex  4489  euabsn2  4532  euabsn  4533  raldifsni  4599  tppreqb  4609  pwpw0  4617  prssg  4623  ssunsn  4632  preqsn  4663  pwpr  4703  dfuni2  4711  unissb  4740  elint2  4753  ssint  4762  uniintab  4784  dfiin2g  4824  iunn0  4852  iunxun  4879  iunxiun  4882  iinpw  4891  disjor  4908  disjxiun  4923  dftr2  5029  dftr5  5030  dftr3  5031  dftr4  5032  vnex  5072  inuni  5099  eusv2  5147  reusv2lem4  5152  rexxfr  5167  snelpw  5191  sspwb  5195  opthneg  5227  pwssun  5305  dfid3  5310  dffr2  5369  opthprc  5463  elxp3  5465  xpiundir  5470  elvv  5473  reliun  5536  inxp  5550  raliunxp  5557  cnvuni  5604  dm0rn0  5638  elrn  5663  dfres3  5698  ssdmres  5719  elidinxp  5754  idinxpres  5757  dfima2  5770  args  5795  dffr3  5800  cotrg  5809  intasym  5813  asymref  5814  intirr  5816  xpnz  5854  xp11  5870  ssrnres  5873  xpimasn  5880  coiun  5946  coass  5955  cnvso  5975  elsnxp  5978  dffr4  6000  wfi  6017  dflim2  6083  orddif  6120  dffun2  6196  dffun6f  6200  dffun7  6213  dffun9  6215  funfn  6216  svrelfun  6257  mptfnf  6311  dffn2  6344  dffn3  6353  fint  6385  dffn4  6423  dff1o4  6450  brprcneu  6489  eqfnfv3  6628  fnreseql  6642  fsn  6719  ftpg  6740  abrexco  6827  imaiun  6828  dff13  6837  isof1oidb  6899  isof1oopb  6900  isocnv2  6906  mpo2eqb  7098  elovmpo  7208  sorpss  7271  abexex  7483  elxp6  7534  elxp7  7535  releldm2  7553  opiota  7564  fnmpo  7574  frxp  7624  cnvimadfsn  7641  mpoxneldm  7680  dftpos4  7713  wfrlem8  7765  wfrfun  7768  dfrecs3  7812  tfrlem7  7822  ondif1  7927  oarec  7988  oeeu  8029  0er  8125  eroveu  8191  erovlem  8192  elixpconst  8266  domen  8318  brsdom  8328  brdom2  8335  reuen1  8374  sbthlem10  8431  brsdom2  8436  xpf1o  8474  onfin2  8504  0sdom1dom  8510  modom  8513  unfi  8579  marypha2lem3  8695  wemapsolem  8808  elom3  8904  dfom5  8906  trcl  8963  epfrs  8966  rankf  9016  scottexs  9109  scott0s  9110  cplem1  9111  karden  9117  hta  9119  djuexb  9131  pm54.43lem  9221  alephsuc2  9299  iscard3  9312  aceq0  9337  aceq3lem  9339  dfac3  9340  dfac5lem2  9343  dfac5  9347  dfac7  9351  dfac12a  9367  kmlem12  9380  kmlem14  9382  kmlem15  9383  infmap2  9437  ackbij2  9462  dfacfin7  9618  ituniiun  9641  zorng  9723  brdom7disj  9750  entri2  9777  alephreg  9801  fpwwe2lem12  9860  fpwwe2lem13  9861  pwfseqlem1  9877  grutsk  10041  axgroth4  10051  grothprim  10053  grothtsk  10054  elni2  10096  ltsopi  10107  genpass  10228  psslinpr  10250  ltexprlem4  10258  ltresr  10359  1re  10438  infm3  11400  elnnz  11802  dfz2  11811  2rexuz  12113  nnwos  12128  eluz2b1  12132  qexALT  12177  elxr  12327  dflt2  12357  xrsupss  12517  xrinfmss  12518  elixx1  12562  elioo2  12594  elioopnf  12646  elicopnf  12648  elfz1  12712  fznn  12790  fzp1nel  12806  fznn0  12814  preduz  12844  prinfzo0  12890  injresinj  12972  nn0opthlem1  13442  faclbnd4lem1  13467  hashfxnn0  13511  hashprdifel  13571  hashgt23el  13597  hashfun  13610  hashf1  13627  fz1isolem  13631  f1oun2prg  14140  brtrclfv  14222  shftdm  14290  rediv  14350  imdiv  14357  rexanre  14566  caubnd  14578  climreu  14773  prodmo  15149  dvdslelem  15518  3dvdsdec  15540  3dvds2dec  15541  bitsval  15632  smueqlem  15698  algcvgblem  15776  lcmfunsnlem2  15839  isprm2  15881  isprm3  15882  isprm4  15883  pythagtriplem2  16009  elgz  16122  hashbc0  16196  0ram  16211  isstruct  16351  issect  16894  isfull2  17052  isfth2  17056  fucinv  17114  eldmcoa  17196  isdrs  17415  fpwipodrs  17645  submacs  17846  isnsg4  18119  isgim  18186  gaorb  18221  oppgid  18268  oppgsubm  18274  oppgcntz  18276  ispgp  18491  efgsdm  18627  efgcpbllema  18653  iscyg2  18770  isring  19037  isirred2  19187  opprirred  19188  dfrhm2  19205  drngid2  19254  opprsubrg  19292  issdrg  19309  islmod  19373  lss1d  19470  islmhm  19534  islmim  19569  lbsextlem2  19666  lidlnz  19735  isnzr2  19770  isassa  19822  dfprm2  20359  isphl  20490  elocv  20530  iunocv  20543  isobs  20582  islinds  20671  1mavmul  20877  toprntopon  21253  isbasis3g  21277  fctop  21332  cctop  21334  isclo2  21416  restsn  21498  lmbr  21586  ist0-3  21673  2ndcdisj  21784  1stccnp  21790  islocfin  21845  1stckgenlem  21881  txbas  21895  ptbasin  21905  tx2cn  21938  fbfinnfr  22169  fbasrn  22212  filuni  22213  ufinffr  22257  fin1aufil  22260  rnelfmlem  22280  flimrest  22311  alexsubALTlem3  22377  alexsubALTlem4  22378  tgphaus  22444  istlm  22512  iscusp2  22630  metuel2  22894  isngp2  22925  isnlm  23003  isphtpc  23317  phtpcer  23318  om1elbas  23355  isclm  23387  iscvsp  23451  iscph  23493  iscau3  23600  minveclem3b  23750  elovolm  23795  ioombl1lem4  23881  dyaddisj  23916  vitali  23933  itg1climres  24034  itg2seq  24062  itg2monolem1  24070  itg2mono  24073  limcrcl  24191  lhop1  24330  itgsubst  24365  mdegleb  24377  isuc1p  24453  ismon1p  24455  plydivex  24605  ellogdm  24939  1cubr  25137  atandm2  25172  birthdaylem3  25249  dmarea  25253  dchrelbas2  25531  dchrelbas4  25537  axcontlem7  26475  nb3grpr  26883  nb3grpr2  26884  upgrwlkcompim  27143  wlkson  27156  wlkonprop  27158  wksonproplem  27210  ispth  27228  wwlknon  27359  wwlksnextinj  27406  wwlksnextinjOLD  27411  wspthsnwspthsnon  27438  elwspths2spth  27489  rusgrnumwwlkl1  27490  clwwlkccatlem  27511  erclwwlkref  27551  frgr3v  27825  nmoubi  28342  nmobndseqi  28349  nmobndseqiALT  28350  minvecolem1  28445  isch2  28795  hlimreui  28811  isch3  28813  ocsh  28857  dfch2  28981  spanuni  29118  nonbooli  29225  5oalem7  29234  adjsym  29407  elbdop2  29445  dmadjss  29461  nmopub  29482  nmfnleub  29499  nmop0h  29565  pjssposi  29746  pjordi  29747  cvbr2  29857  cvnbtwn2  29861  mdsl2i  29896  cvmdi  29898  elat2  29914  atom1d  29927  chirredi  29968  cdj3i  30015  or3di  30022  opreu2reu1  30045  moel  30050  mo5f  30051  rexunirn  30053  difrab2  30056  iuninc  30099  disjorf  30113  disjunsn  30128  rabfmpunirn  30178  aciunf1  30188  funcnv5mpt  30193  dfrp2  30268  eliccelico  30277  elicoelioo  30278  isomnd  30447  omndmul2  30458  isslmd  30529  islinds5  30638  hasheuni  31021  pwsiga  31067  sigainb  31073  issros  31112  2ndmbfm  31197  omssubaddlem  31235  omssubadd  31236  sitgaddlemb  31284  eulerpartlemgvv  31312  eulerpartlemn  31317  probun  31356  ballotlem2  31425  ballotlemodife  31434  bnj252  31654  bnj253  31655  bnj255  31656  bnj345  31665  bnj133  31678  bnj976  31730  bnj1098  31736  bnj121  31822  bnj130  31826  bnj150  31828  bnj581  31860  bnj607  31868  bnj865  31875  bnj917  31886  bnj934  31887  bnj964  31895  bnj983  31903  bnj996  31907  bnj1021  31916  bnj1033  31919  bnj1047  31923  bnj1049  31924  bnj1090  31929  bnj1128  31940  bnj1175  31954  bnj1189  31959  bnj1253  31967  bnj1312  32008  exdifsn  32023  erdszelem9  32064  erdszelem10  32065  pconnconn  32096  cvmliftiota  32166  elmthm  32376  nepss  32501  dfso2  32543  dfpo2  32544  elrn3  32551  imaindm  32575  elpotr  32579  dfon2lem5  32585  dfon2lem7  32587  dfon2lem8  32588  frpoind  32634  frind  32639  soseq  32650  elwlim  32664  wzel  32665  frrlem9  32685  elno3  32716  nosgnn0  32719  nosepon  32726  nocvxminlem  32801  scutcut  32820  scutbday  32821  dmscut  32826  scutf  32827  sltrec  32832  brtxp2  32896  brpprod3a  32901  eltrans  32906  dfon3  32907  dffix2  32920  dffun10  32929  elfuns  32930  brsingle  32932  brimg  32952  funpartfun  32958  funpartfv  32960  cgrxfr  33070  segletr  33129  outsideoftr  33144  neifg  33273  filnetlem4  33283  df3nandALT1  33301  bj-consensusALT  33462  bj-biexal3  33584  bj-ralvw  33721  bj-rexvw  33722  bj-rexcom4bv  33724  bj-rexcom4b  33725  bj-sbeq  33743  bj-inrab  33773  bj-nfnnfTEMP  33815  bj-dfmpoa  33952  topdifinffinlem  34103  topdifinfeq  34106  relowlssretop  34119  relowlpssretop  34120  rdgeqoa  34126  domalom  34159  nlpineqsn  34163  fvineqsneq  34167  wl-dfclab  34302  wl-dfralsb  34311  wl-dfrexsb  34325  wl-dfrmosb  34327  wl-dfrmov  34328  wl-dfrabv  34336  rabiun  34339  phpreu  34350  fin2solem  34352  matunitlindflem2  34363  ptrest  34365  poimirlem25  34391  poimirlem27  34393  poimirlem30  34396  ismblfin  34407  ovoliunnfl  34408  voliunnfl  34410  volsupnfl  34411  itg2addnclem2  34418  fdc  34495  prdstotbnd  34547  isdrngo1  34709  ispridl  34787  ismaxidl  34793  impor  34834  selconj  34855  tradd  34860  scott0f  34924  inxpss3  35048  idinxpssinxp2  35052  idinxpssinxp3  35053  dfrel5  35082  ineleq  35087  moantr  35095  dfxrn2  35106  inxpxrn  35121  rnxrnres  35125  1cossres  35152  cocossss  35159  cossssid4  35188  cossssid5  35189  cosscnvssid5  35196  cossid  35198  dfssr2  35217  cnvrefrelcoss2  35251  cosselcnvrefrels2  35252  eqvrelcoss  35330  eqvrelcoss2  35332  dfcoeleqvrel  35335  refrelredund4  35348  cnvepresdmqs  35365  dfmember  35384  dfdisjALTV  35424  dfeldisj3  35430  dfeldisj4  35431  dfeldisj5  35432  prter1  35493  islshp  35593  islshpat  35631  lcvbr2  35636  lcvnbtwn2  35641  cvrnbtwn3  35890  isatl  35913  ishlat1  35966  ishlat2  35967  cvrat4  36057  pmapglbx  36383  lhpexle3  36626  dib1dim  37779  diblsmopel  37785  lcfls1lem  38148  sn-axrep  38585  prjsperref  38697  prjspeclsp  38703  rexrabdioph  38821  dford4  39056  isdomn3  39234  ifpdfor2  39256  ifpdfan2  39258  ifpdfor  39260  ifpdfan  39261  ifpdfbi  39269  ifpnot23b  39278  ifpnot23c  39280  ifpnot23d  39281  ifpim123g  39296  ifpbibib  39306  clss2lem  39368  imaiun1  39393  coiun1  39394  brfvrcld2  39434  iunrelexp0  39444  brtrclfv2  39469  snhesn  39529  dffrege76  39682  frege97  39703  frege98  39704  frege109  39715  frege110  39716  dffrege115  39721  frege131  39737  frege133  39739  ntrneineine1lem  39831  ntrneiel2  39833  ntrneiiso  39838  gneispace3  39880  scotteld  39991  ismnuprim  40039  pm11.52  40169  pm11.58  40173  pm13.192  40193  impexpdcom  40302  sbc3or  40319  opelopab4  40338  uunT12p1  40587  uunT12p2  40588  uunT12p3  40589  uun2221  40600  uun2221p1  40601  uun2221p2  40602  undif3VD  40669  ndisj2  40766  nssrex  40804  rabssf  40840  bothtbothsame  42595  bothfbothsame  42596  aiffbtbat  42604  reuabaiotaiota  42723  2reu8i  42748  2reuimp0  42749  ichn  43026  dfodd2  43199  dfeven5  43229  dfodd7  43230  1nevenALTV  43254  oddprmne2  43278  isrng  43541  isrnghm  43557  islindeps2  43935  isldepslvec2  43937  line2xlem  44138  setrec1lem3  44189  aacllem  44299