Theorem bitr4i 280

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

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  3bitr2i  301  3bitr2ri  302  3bitr4i  305  3bitr4ri  306  biluk  389  biancomi  465  dfbi2  477  imdistan  570  pm5.32  576  bianass  640  mpbiran  707  biadaniALT  819  imor  849  imimorb  947  pm5.6  998  nbi2  1012  casesifp  1071  3ancoma  1094  3ancomb  1095  3anrev  1097  an3andi  1478  nanimn  1484  nannan  1487  nanbi  1490  xorcom  1504  xorneg  1514  xorbi12i  1515  norcom  1522  noran  1526  norasslem1  1530  norassOLD  1534  trunortru  1586  trunorfal  1588  cadan  1610  cadcomb  1614  nic-ax  1674  nic-axALT  1675  nf3  1787  nfnbi  1855  19.43  1883  19.3vOLD  1989  equsv  2009  sb3an  2087  sbrimvlem  2101  sbcom2  2168  sb5OLD  2281  nf5  2290  nf6  2291  sb6x  2487  2sb5rf  2496  2sb6rf  2497  sb4b  2499  sb4bOLD  2500  sb5f  2538  sbequ8  2543  sbhb  2563  sb5ALT2  2586  sb5fALT  2603  eu6lem  2658  eu1  2694  cleqh  2938  clelab  2960  cleqf  3012  necon3bii  3070  neor  3110  neorian  3113  r19.26-3  3174  r19.26m  3175  r2allem  3202  r19.23t  3315  r19.43  3353  rexcom  3357  rabid2  3383  rabid2f  3384  eqv  3504  eqvf  3505  isset  3508  ralv  3521  rexv  3522  reuv  3523  rmov  3524  rexcom4b  3526  ceqsex4v  3548  ceqsex8v  3550  ceqsrexv  3651  ralrab2  3692  rexrab2  3695  reu2  3718  reu3  3720  reueq  3730  2reuswap  3739  2reuswap2  3740  reuind  3746  2reu5lem3  3750  2rmoswap  3754  sbc3an  3840  rmo2  3872  rmoanim  3880  rmoanimALT  3881  dfss2  3957  dfss3  3958  dfss3f  3961  ssabral  4044  rabss  4050  ssrabeq  4061  uniiunlem  4063  sspsstri  4081  npss  4089  dfdif3  4093  raldifb  4123  uncom  4131  inass  4198  elsymdifxor  4228  nsspssun  4236  dfss4  4237  dfun2  4238  dfin2  4239  indi  4252  indifdir  4262  difin2  4268  reupick3  4290  eq0f  4307  neq0f  4308  dfnf5  4336  rabn0  4341  csbab  4391  vss  4397  disj  4401  disj3  4405  undisj1  4413  undisj2  4414  inundif  4429  undif  4432  absn  4587  rabsssn  4609  exsnrex  4620  euabsn2  4663  euabsn  4664  raldifsni  4730  tppreqb  4740  pwpw0  4748  prssg  4754  ssunsn  4763  preqsn  4794  pwpr  4834  dfuni2  4842  unissb  4872  elint2  4885  ssint  4894  uniintab  4916  dfiin2g  4959  iunn0  4991  iunxun  5018  iunxiun  5021  iinpw  5030  disjor  5048  disjxiun  5065  dftr2  5176  dftr5  5177  dftr3  5178  dftr4  5179  axrep6  5199  vnex  5220  inuni  5248  eusv2  5299  reusv2lem4  5304  rexxfr  5319  snelpw  5340  sspwb  5344  opthneg  5375  pwssun  5458  dfid3  5464  dffr2  5522  opthprc  5618  elxp3  5620  xpiundir  5625  elvv  5628  reliun  5691  inxp  5705  raliunxp  5712  cnvuni  5759  dmopab2rex  5788  dm0rn0  5797  elrn  5824  dfres3  5860  ssdmres  5878  elidinxp  5913  idinxpres  5916  dfima2  5933  args  5959  dffr3  5964  cotrg  5973  intasym  5977  asymref  5978  intirr  5980  xpnz  6018  xp11  6034  ssrnres  6037  xpimasn  6044  coiun  6111  coass  6120  cnvso  6141  elsnxp  6144  dffr4  6166  wfi  6183  dflim2  6249  orddif  6286  dffun2  6367  dffun6f  6371  dffun7  6384  dffun9  6386  funfn  6387  svrelfun  6428  mptfnf  6485  dffn2  6518  dffn3  6527  fint  6560  dffn4  6598  dff1o4  6625  brprcneu  6664  eqfnfv3  6806  fnreseql  6820  fsn  6899  ftpg  6920  abrexco  7005  imaiun  7006  dff13  7015  isof1oidb  7079  isof1oopb  7080  isocnv2  7086  mpo2eqb  7285  elovmpo  7392  sorpss  7456  abexex  7674  elxp6  7725  elxp7  7726  releldm2  7744  opiota  7759  fnmpo  7769  frxp  7822  cnvimadfsn  7841  mpoxneldm  7880  dftpos4  7913  wfrlem8  7964  wfrfun  7967  dfrecs3  8011  tfrlem7  8021  ondif1  8128  oarec  8190  oeeu  8231  0er  8328  eroveu  8394  erovlem  8395  elixpconst  8471  domen  8524  brsdom  8534  brdom2  8541  reuen1  8580  sbthlem10  8638  brsdom2  8643  xpf1o  8681  onfin2  8712  0sdom1dom  8718  modom  8721  unfi  8787  marypha2lem3  8903  wemapsolem  9016  elom3  9113  dfom5  9115  trcl  9172  epfrs  9175  rankf  9225  scottexs  9318  scott0s  9319  cplem1  9320  karden  9326  hta  9328  djuexb  9340  pm54.43lem  9430  alephsuc2  9508  iscard3  9521  aceq0  9546  aceq3lem  9548  dfac3  9549  dfac5lem2  9552  dfac5  9556  dfac7  9560  dfac12a  9576  kmlem12  9589  kmlem14  9591  kmlem15  9592  infmap2  9642  ackbij2  9667  dfacfin7  9823  ituniiun  9846  zorng  9928  brdom7disj  9955  entri2  9982  alephreg  10006  fpwwe2lem12  10065  fpwwe2lem13  10066  pwfseqlem1  10082  grutsk  10246  axgroth4  10256  grothprim  10258  grothtsk  10259  elni2  10301  ltsopi  10312  genpass  10433  psslinpr  10455  ltexprlem4  10463  ltresr  10564  1re  10643  infm3  11602  elnnz  11994  dfz2  12003  2rexuz  12303  nnwos  12318  eluz2b1  12322  qexALT  12366  elxr  12514  dflt2  12544  xrsupss  12705  xrinfmss  12706  elixx1  12750  elioo2  12782  elioopnf  12834  elicopnf  12836  elfz1  12900  fznn  12978  fzp1nel  12994  fznn0  13002  preduz  13032  prinfzo0  13079  injresinj  13161  nn0opthlem1  13631  faclbnd4lem1  13656  hashfxnn0  13700  hashprdifel  13762  hashgt23el  13788  hashfun  13801  hashf1  13818  fz1isolem  13822  f1oun2prg  14281  brtrclfv  14364  shftdm  14432  rediv  14492  imdiv  14499  rexanre  14708  caubnd  14720  climreu  14915  prodmo  15292  dvdslelem  15661  3dvdsdec  15683  3dvds2dec  15684  bitsval  15775  smueqlem  15841  algcvgblem  15923  lcmfunsnlem2  15986  isprm2  16028  isprm3  16029  isprm4  16030  pythagtriplem2  16156  elgz  16269  hashbc0  16343  0ram  16358  isstruct  16498  issect  17025  isfull2  17183  isfth2  17187  fucinv  17245  eldmcoa  17327  isdrs  17546  submacs  17993  isnsg4  18321  isgim  18404  gaorb  18439  oppgid  18486  oppgsubm  18492  oppgcntz  18494  ispgp  18719  efgsdm  18858  efgcpbllema  18882  iscyg2  19003  isring  19303  isirred2  19453  opprirred  19454  dfrhm2  19471  drngid2  19520  opprsubrg  19558  issdrg  19576  islmod  19640  lss1d  19737  islmhm  19801  islmim  19836  lbsextlem2  19933  lidlnz  20003  isnzr2  20038  isassa  20090  dfprm2  20643  isphl  20774  elocv  20814  iunocv  20827  isobs  20866  islinds  20955  1mavmul  21159  toprntopon  21535  isbasis3g  21559  fctop  21614  cctop  21616  isclo2  21698  restsn  21780  lmbr  21868  ist0-3  21955  2ndcdisj  22066  1stccnp  22072  islocfin  22127  1stckgenlem  22163  txbas  22177  ptbasin  22187  tx2cn  22220  fbfinnfr  22451  fbasrn  22494  filuni  22495  ufinffr  22539  fin1aufil  22542  rnelfmlem  22562  flimrest  22593  alexsubALTlem3  22659  alexsubALTlem4  22660  tgphaus  22727  istlm  22795  iscusp2  22913  metuel2  23177  isngp2  23208  isnlm  23286  isphtpc  23600  phtpcer  23601  om1elbas  23638  isclm  23670  iscvsp  23734  iscph  23776  iscau3  23883  minveclem3b  24033  elovolm  24078  ioombl1lem4  24164  dyaddisj  24199  vitali  24216  itg1climres  24317  itg2seq  24345  itg2monolem1  24353  itg2mono  24356  limcrcl  24474  lhop1  24613  itgsubst  24648  mdegleb  24660  isuc1p  24736  ismon1p  24738  plydivex  24888  ellogdm  25224  1cubr  25422  atandm2  25457  birthdaylem3  25533  dmarea  25537  dchrelbas2  25815  dchrelbas4  25821  axcontlem7  26758  nb3grpr  27166  nb3grpr2  27167  upgrwlkcompim  27426  wlkson  27440  wlkonprop  27442  wksonproplem  27488  ispth  27506  wwlknon  27637  wwlksnextinj  27679  wspthsnwspthsnon  27697  elwspths2spth  27748  rusgrnumwwlkl1  27749  clwwlkccatlem  27769  erclwwlkref  27800  frgr3v  28056  nmoubi  28551  nmobndseqi  28558  nmobndseqiALT  28559  minvecolem1  28653  isch2  29002  hlimreui  29018  isch3  29020  ocsh  29062  dfch2  29186  spanuni  29323  nonbooli  29430  5oalem7  29439  adjsym  29612  elbdop2  29650  dmadjss  29666  nmopub  29687  nmfnleub  29704  nmop0h  29770  pjssposi  29951  pjordi  29952  cvbr2  30062  cvnbtwn2  30066  mdsl2i  30101  cvmdi  30103  elat2  30119  atom1d  30132  chirredi  30173  cdj3i  30220  or3di  30227  opreu2reu1  30249  moel  30254  mo5f  30255  reuxfrdf  30257  rexunirn  30258  difrab2  30263  iuninc  30314  disjorf  30331  disjunsn  30346  rabfmpunirn  30400  aciunf1  30410  funcnv5mpt  30415  dfrp2  30493  eliccelico  30502  elicoelioo  30503  isomnd  30704  omndmul2  30715  isslmd  30832  islinds5  30934  ismxidl  30973  hasheuni  31346  pwsiga  31391  sigainb  31397  issros  31436  2ndmbfm  31521  omssubaddlem  31559  omssubadd  31560  sitgaddlemb  31608  eulerpartlemgvv  31636  eulerpartlemn  31641  probun  31679  ballotlem2  31748  ballotlemodife  31757  bnj252  31975  bnj253  31976  bnj255  31977  bnj345  31986  bnj133  31999  bnj976  32051  bnj1098  32057  bnj121  32144  bnj130  32148  bnj150  32150  bnj581  32182  bnj607  32190  bnj865  32197  bnj917  32208  bnj934  32209  bnj964  32217  bnj983  32225  bnj996  32230  bnj1021  32240  bnj1033  32243  bnj1047  32247  bnj1049  32248  bnj1090  32253  bnj1128  32264  bnj1175  32278  bnj1189  32283  bnj1253  32291  bnj1312  32332  exdifsn  32347  erdszelem9  32448  erdszelem10  32449  pconnconn  32480  cvmliftiota  32550  fmlaomn0  32639  fmla0disjsuc  32647  fmlasucdisj  32648  dmopab3rexdif  32654  elmthm  32825  nepss  32950  dfso2  32992  dfpo2  32993  elrn3  33000  imaindm  33024  elpotr  33028  dfon2lem5  33034  dfon2lem7  33036  dfon2lem8  33037  frpoind  33082  frind  33087  soseq  33098  elwlim  33112  wzel  33113  frrlem9  33133  elno3  33164  nosgnn0  33167  nosepon  33174  nocvxminlem  33249  scutcut  33268  scutbday  33269  dmscut  33274  scutf  33275  sltrec  33280  brtxp2  33344  brpprod3a  33349  eltrans  33354  dfon3  33355  dffix2  33368  dffun10  33377  elfuns  33378  brsingle  33380  brimg  33400  funpartfun  33406  funpartfv  33408  cgrxfr  33518  segletr  33577  outsideoftr  33592  neifg  33721  filnetlem4  33731  df3nandALT1  33749  bj-consensusALT  33914  bj-df-ifc  33915  bj-biexal3  34043  bj-nfnnfTEMP  34089  bj-ralvw  34197  bj-rexvw  34198  bj-rexcom4bv  34200  bj-rexcom4b  34201  bj-sbeq  34220  bj-inrab  34247  bj-rcleqf  34339  bj-dfmpoa  34412  topdifinffinlem  34630  topdifinfeq  34633  relowlssretop  34646  relowlpssretop  34647  rdgeqoa  34653  domalom  34687  nlpineqsn  34691  fvineqsneq  34695  wl-dfclab  34830  wl-dfralsb  34839  wl-dfrexsb  34853  wl-dfrmosb  34855  wl-dfrmov  34856  wl-dfrabv  34864  rabiun  34867  phpreu  34878  fin2solem  34880  matunitlindflem2  34891  ptrest  34893  poimirlem25  34919  poimirlem27  34921  poimirlem30  34924  ismblfin  34935  ovoliunnfl  34936  voliunnfl  34938  volsupnfl  34939  itg2addnclem2  34946  fdc  35022  prdstotbnd  35074  isdrngo1  35236  ispridl  35314  ismaxidl  35320  impor  35361  selconj  35380  tradd  35385  scott0f  35449  inxpss3  35573  idinxpssinxp2  35577  idinxpssinxp3  35578  dfrel5  35605  ineleq  35610  moantr  35618  dfxrn2  35630  inxpxrn  35645  rnxrnres  35649  1cossres  35676  cocossss  35683  cossssid4  35712  cossssid5  35713  cosscnvssid5  35720  cossid  35722  dfssr2  35741  cnvrefrelcoss2  35775  cosselcnvrefrels2  35776  eqvrelcoss  35854  eqvrelcoss2  35856  dfcoeleqvrel  35859  refrelredund4  35872  cnvepresdmqs  35889  dfmember  35908  dfdisjALTV  35948  dfeldisj3  35954  dfeldisj4  35955  dfeldisj5  35956  prter1  36017  islshp  36117  islshpat  36155  lcvbr2  36160  lcvnbtwn2  36165  cvrnbtwn3  36414  isatl  36437  ishlat1  36490  ishlat2  36491  cvrat4  36581  pmapglbx  36907  lhpexle3  37150  dib1dim  38303  diblsmopel  38309  lcfls1lem  38672  prjsperref  39263  prjspeclsp  39269  rexrabdioph  39398  dford4  39633  isdomn3  39811  ifpdfor2  39833  ifpdfan2  39835  ifpdfor  39837  ifpdfan  39838  ifpdfbi  39846  ifpnot23b  39855  ifpnot23c  39857  ifpnot23d  39858  ifpim123g  39873  ifpbibib  39883  clss2lem  39978  imaiun1  40003  coiun1  40004  brfvrcld2  40044  iunrelexp0  40054  brtrclfv2  40079  snhesn  40139  dffrege76  40292  frege97  40313  frege98  40314  frege109  40325  frege110  40326  dffrege115  40331  frege131  40347  frege133  40349  ntrneineine1lem  40441  ntrneiel2  40443  ntrneiiso  40448  gneispace3  40490  scotteld  40589  ismnuprim  40637  pm11.52  40726  pm11.58  40729  pm13.192  40749  impexpdcom  40856  sbc3or  40873  opelopab4  40892  uunT12p1  41141  uunT12p2  41142  uunT12p3  41143  uun2221  41154  uun2221p1  41155  uun2221p2  41156  undif3VD  41223  ndisj2  41320  nssrex  41358  rabssf  41392  bothtbothsame  43142  bothfbothsame  43143  aiffbtbat  43151  reuabaiotaiota  43294  2reu8i  43319  2reuimp0  43320  ichn  43633  dfodd2  43808  dfeven5  43838  dfodd7  43839  1nevenALTV  43863  oddprmne2  43887  isrng  44154  isrnghm  44170  islindeps2  44545  isldepslvec2  44547  line2xlem  44747  setrec1lem3  44799  aacllem  44909