Theorem bitr4i 269

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

Syntax hints:   ↔ wb 197

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 198

This theorem is referenced by:  3bitr2i  290  3bitr2ri  291  3bitr4i  294  3bitr4ri  295  dfbi2  462  imdistan  559  pm5.32  565  bianass  625  mpbiran  691  mpbiran2  692  imor  871  imimorb  964  pm5.6  1015  nbi2  1030  biluk  1041  casesifp  1092  3ancoma  1112  3ancomb  1114  3anrev  1119  an3andi  1599  nancom  1604  nanbi  1608  xorneg  1630  cadan  1703  cadcomb  1707  nic-ax  1753  nic-axALT  1754  nf3  1866  nfnbi  1940  19.43  1972  19.3v  2077  sb5  2285  nf5  2291  nf6  2292  sb6x  2543  sb5f  2545  sb3an  2559  sbequ8ALT  2566  sbhb  2600  sbnf2  2601  sbcom2  2605  eu1  2673  cleqh  2908  clelab  2932  necon3bii  3030  neor  3069  neorian  3072  r2allem  3125  r19.23t  3209  r19.26-3  3254  r19.26m  3255  r19.43  3281  rabid2  3307  rabid2f  3308  eqv  3397  eqvf  3398  isset  3401  ralv  3413  rexv  3414  reuv  3415  rmov  3416  rexcom4b  3421  ceqsex4v  3441  ceqsex8v  3443  ceqsrexv  3530  rabtru  3556  ralrab2  3568  rexrab2  3570  reu2  3592  reu3  3594  reueq  3602  2reuswap  3608  reuind  3609  2reu5lem3  3613  sbc3an  3691  rmo2  3721  dfss2  3786  dfss3  3787  dfss3f  3790  ssabral  3870  rabss  3876  ssrabeq  3887  uniiunlem  3889  sspsstri  3907  npss  3915  dfdif3  3919  raldifb  3949  uncom  3956  inass  4020  elsymdifxor  4049  symdifassOLD  4052  nsspssun  4059  dfss4  4060  dfun2  4061  dfin2  4062  indi  4075  indifdir  4085  difin2  4091  reupick3  4113  eq0f  4127  neq0f  4128  rabn0  4158  csbab  4206  vss  4210  disj  4214  disj3  4218  undisj1  4226  undisj2  4227  inundif  4242  undif  4245  absn  4388  rabsssn  4408  exsnrex  4414  euabsn2  4451  euabsn  4452  raldifsni  4516  tppreqb  4526  pwpw0  4534  prssg  4540  ssunsn  4549  preqsn  4583  pwpr  4624  dfuni2  4632  unissb  4663  elint2  4676  ssint  4685  uniintab  4707  iuneq12df  4736  dfiin2g  4745  iunn0  4772  iunxun  4797  iunxiun  4800  iinpw  4809  disjor  4826  disjxiun  4841  dftr2  4948  dftr5  4949  dftr3  4950  dftr4  4951  vnex  4991  inuni  5018  eusv2  5065  reusv2lem4  5070  rexxfr  5085  snelpw  5103  sspwb  5107  opthneg  5139  pwssun  5215  dfid3  5220  dffr2  5276  opthprc  5367  elxp3  5369  xpiundir  5374  elvv  5377  brinxp2OLD  5381  relsnOLD  5428  reliun  5441  inxp  5456  raliunxp  5463  cnvuni  5510  dm0rn0  5543  elrn  5567  dfres3  5602  ssdmres  5623  dfres2  5658  elidinxp  5660  elridOLD  5663  idinxpres  5665  dfima2  5678  args  5703  dffr3  5708  cotrg  5717  intasym  5722  asymref  5723  intirr  5725  cnv0OLD  5747  xpnz  5764  xp11  5780  xpimasn  5790  resco  5853  rnco  5855  coiun  5859  coass  5868  cnvso  5888  elsnxp  5891  dffr4  5909  wfi  5926  dflim2  5994  orddif  6033  dffun2  6111  dffun6f  6115  dffun7  6128  dffun9  6130  funfn  6131  svrelfun  6172  mptfnf  6226  dffn2  6258  dffn3  6267  fint  6299  dffn4  6337  dff1o4  6361  brprcneu  6400  eqfnfv3  6535  fnreseql  6549  fsn  6625  ftpg  6647  abrexco  6726  imaiun  6727  dff13  6736  isof1oidb  6798  isof1oopb  6799  isocnv2  6805  mpt22eqb  6999  elovmpt2  7109  sorpss  7172  abexex  7381  elxp6  7432  elxp7  7433  releldm2  7450  opiota  7461  fnmpt2  7471  frxp  7521  cnvimadfsn  7538  mpt2xneldm  7573  dftpos4  7606  wfrlem8  7658  wfrfun  7661  dfrecs3  7705  tfrlem7  7715  ondif1  7818  oarec  7879  oeeu  7920  0er  8016  eroveu  8078  erovlem  8079  map0eOLD  8131  elixpconst  8153  domen  8205  brsdom  8215  brdom2  8222  reuen1  8261  sbthlem10  8318  brsdom2  8323  xpf1o  8361  onfin2  8391  0sdom1dom  8397  modom  8400  unfi  8466  marypha2lem3  8582  wemapsolem  8694  sucprcreg  8745  elom3  8792  dfom5  8794  trcl  8851  epfrs  8854  rankf  8904  scottexs  8997  scott0s  8998  cplem1  8999  karden  9005  hta  9007  pm54.43lem  9108  alephsuc2  9186  iscard3  9199  aceq0  9224  aceq3lem  9226  dfac3  9227  dfac5lem2  9230  dfac5  9234  dfac7  9239  dfac12a  9255  kmlem12  9268  kmlem14  9270  kmlem15  9271  infmap2  9325  ackbij2  9350  dfacfin7  9506  ituniiun  9529  zorng  9611  brdom7disj  9638  entri2  9665  alephreg  9689  fpwwe2lem12  9748  fpwwe2lem13  9749  pwfseqlem1  9765  grutsk  9929  axgroth4  9939  grothprim  9941  grothtsk  9942  elni2  9984  ltsopi  9995  genpass  10116  psslinpr  10138  ltexprlem4  10146  ltresr  10246  1re  10325  infm3  11267  elnnz  11653  dfz2  11661  2rexuz  11958  nnwos  11974  eluz2b1  11978  qexALT  12022  elxr  12166  dflt2  12197  xrsupss  12357  xrinfmss  12358  elixx1  12402  elioo2  12434  elioopnf  12486  elicopnf  12488  elfz1  12554  fznn  12631  fzp1nel  12647  fznn0  12655  preduz  12685  prinfzo0  12731  injresinj  12813  nn0opthlem1  13275  faclbnd4lem1  13300  hashfxnn0  13344  hashfOLD  13346  hashprdifel  13403  hashfun  13441  hashf1  13458  fz1isolem  13462  f1oun2prg  13886  brtrclfv  13966  shftdm  14034  rediv  14094  imdiv  14101  rexanre  14309  caubnd  14321  climreu  14510  prodmo  14887  dvdslelem  15254  3dvdsdec  15276  3dvds2dec  15277  bitsval  15365  smueqlem  15431  algcvgblem  15509  lcmfunsnlem2  15572  isprm2  15613  isprm3  15614  isprm4  15615  pythagtriplem2  15739  elgz  15852  hashbc0  15926  0ram  15941  isstruct  16081  issect  16617  isfull2  16775  isfth2  16779  fucinv  16837  eldmcoa  16919  isdrs  17139  fpwipodrs  17369  submacs  17570  isnsg4  17839  isgim  17906  gaorb  17941  oppgid  17987  oppgsubm  17993  oppgcntz  17995  ispgp  18208  efgsdm  18344  efgcpbllema  18368  iscyg2  18485  isring  18753  isirred2  18903  opprirred  18904  dfrhm2  18921  drngid2  18967  opprsubrg  19005  islmod  19071  lss1d  19170  islmhm  19234  islmim  19269  lbsextlem2  19368  lidlnz  19437  lidldvgen  19464  isnzr2  19472  isassa  19524  dfprm2  20050  isphl  20183  elocv  20222  iunocv  20235  isobs  20274  islinds  20358  1mavmul  20565  isbasis3g  20967  fctop  21022  cctop  21024  isclo2  21106  restsn  21188  lmbr  21276  ist0-3  21363  2ndcdisj  21473  1stccnp  21479  islocfin  21534  1stckgenlem  21570  txbas  21584  ptbasin  21594  tx2cn  21627  fbfinnfr  21858  fbasrn  21901  filuni  21902  ufinffr  21946  fin1aufil  21949  rnelfmlem  21969  flimrest  22000  alexsubALTlem3  22066  alexsubALTlem4  22067  tgphaus  22133  istlm  22201  iscusp2  22319  metuel2  22583  isngp2  22614  isnlm  22692  elcncf1di  22911  isphtpc  23006  phtpcer  23007  om1elbas  23044  isclm  23076  iscvsp  23140  iscph  23182  iscau3  23288  minveclem3b  23411  elovolm  23456  ioombl1lem4  23542  dyaddisj  23577  vitali  23594  itg1climres  23695  itg2seq  23723  itg2monolem1  23731  itg2mono  23734  limcrcl  23852  lhop1  23991  itgsubst  24026  mdegleb  24038  isuc1p  24114  ismon1p  24116  plydivex  24266  ellogdm  24599  1cubr  24783  atandm2  24818  birthdaylem3  24894  dmarea  24898  dchrelbas2  25176  dchrelbas4  25182  axcontlem7  26064  nb3grpr  26500  nb3grpr2  26501  upgrwlkcompim  26767  wlkson  26780  wlkonprop  26782  wksonproplem  26829  ispth  26847  wwlknon  26981  wwlknonOLD  26983  wwlksnextinj  27036  wspthsnwspthsnon  27054  elwspths2spth  27109  rusgrnumwwlkl1  27110  clwwlkccatlem  27132  erclwwlkref  27163  frgr3v  27450  nmoubi  27955  nmobndseqi  27962  nmobndseqiALT  27963  minvecolem1  28058  isch2  28408  hlimreui  28424  isch3  28426  ocsh  28470  dfch2  28594  spanuni  28731  nonbooli  28838  5oalem7  28847  adjsym  29020  elbdop2  29058  dmadjss  29074  nmopub  29095  nmfnleub  29112  nmop0h  29178  pjssposi  29359  pjordi  29360  cvbr2  29470  cvnbtwn2  29474  mdsl2i  29509  cvmdi  29511  elat2  29527  atom1d  29540  chirredi  29581  cdj3i  29628  or3di  29635  moel  29651  mo5f  29652  2reuswap2  29654  rexunirn  29657  difrab2  29664  difininv  29679  iuneq12daf  29698  iuninc  29704  disjorf  29717  disjunsn  29732  rabfmpunirn  29780  aciunf1  29790  funcnv5mpt  29796  dfrp2  29859  eliccelico  29866  elicoelioo  29867  isomnd  30026  omndmul2  30037  isslmd  30080  hasheuni  30472  pwsiga  30518  sigainb  30524  issros  30563  2ndmbfm  30648  omssubaddlem  30686  omssubadd  30687  sitgaddlemb  30735  eulerpartlemgvv  30763  eulerpartlemn  30768  probun  30806  ballotlem2  30875  ballotlemodife  30884  bnj252  31094  bnj253  31095  bnj255  31096  bnj345  31105  bnj133  31118  bnj976  31171  bnj1098  31177  bnj121  31263  bnj130  31267  bnj150  31269  bnj581  31301  bnj607  31309  bnj865  31316  bnj917  31327  bnj934  31328  bnj964  31336  bnj983  31344  bnj996  31348  bnj1021  31357  bnj1033  31360  bnj1047  31364  bnj1049  31365  bnj1090  31370  bnj1128  31381  bnj1175  31395  bnj1189  31400  bnj1253  31408  bnj1312  31449  erdszelem9  31504  erdszelem10  31505  pconnconn  31536  cvmliftiota  31606  elmthm  31796  nepss  31921  dfso2  31966  dfpo2  31967  elrn3  31974  imaindm  32002  elpotr  32006  dfon2lem5  32012  dfon2lem7  32014  dfon2lem8  32015  frpoind  32061  frind  32064  soseq  32075  elwlim  32089  wzel  32090  frrlem5c  32107  elno3  32129  nosgnn0  32132  nosepon  32139  nocvxminlem  32214  scutcut  32233  scutbday  32234  dmscut  32239  scutf  32240  sltrec  32245  brtxp2  32309  brpprod3a  32314  eltrans  32319  dfon3  32320  dffix2  32333  dffun10  32342  elfuns  32343  brsingle  32345  brimg  32365  funpartfun  32371  funpartfv  32373  cgrxfr  32483  segletr  32542  outsideoftr  32557  neifg  32687  filnetlem4  32697  df3nandALT1  32715  bj-consensusALT  32878  bj-biexal3  33013  bj-sb5  33082  bj-ralvw  33173  bj-rexvwv  33174  bj-rexcom4bv  33179  bj-rexcom4b  33180  bj-sbeq  33204  bj-inrab  33234  bj-xpima1snALT  33254  bj-dfmpt2a  33382  topdifinffinlem  33511  topdifinfeq  33514  relowlssretop  33527  relowlpssretop  33528  rdgeqoa  33534  wl-dfnan2  33612  wl-nannan  33614  rabiun  33695  phpreu  33706  fin2solem  33708  matunitlindflem2  33719  ptrest  33721  poimirlem25  33747  poimirlem27  33749  poimirlem30  33752  ismblfin  33763  ovoliunnfl  33764  voliunnfl  33766  volsupnfl  33767  itg2addnclem2  33774  fdc  33852  prdstotbnd  33904  isdrngo1  34066  ispridl  34144  ismaxidl  34150  impor  34191  selconj  34213  tradd  34218  scott0f  34287  biancom  34315  inxpss3  34400  idinxpssinxp2  34404  idinxpssinxp3  34405  dfrel5  34427  ineleq  34432  moantr  34440  dfxrn2  34451  inxpxrn  34466  rnxrnres  34470  1cossres  34497  cocossss  34504  cossssid4  34533  cossssid5  34534  cosscnvssid5  34541  cossid  34543  dfssr2  34562  cnvrefrelcoss2  34596  cosselcnvrefrels2  34597  prter1  34658  islshp  34759  islshpat  34797  lcvbr2  34802  lcvnbtwn2  34807  cvrnbtwn3  35056  isatl  35079  ishlat1  35132  ishlat2  35133  cvrat4  35223  pmapglbx  35549  lhpexle3  35792  dib1dim  36946  diblsmopel  36952  lcfls1lem  37315  rexrabdioph  37860  dford4  38097  issdrg  38268  isdomn3  38283  ifpdfor2  38305  ifpdfan2  38307  ifpdfor  38309  ifpdfan  38310  ifpdfbi  38318  ifpnot23b  38327  ifpnot23c  38329  ifpnot23d  38330  ifpim123g  38345  ifpbibib  38355  clss2lem  38418  imaiun1  38443  coiun1  38444  brfvrcld2  38484  iunrelexp0  38494  brtrclfv2  38519  snhesn  38580  dffrege76  38733  frege97  38754  frege98  38755  frege109  38766  frege110  38767  dffrege115  38772  frege131  38788  frege133  38790  ntrneineine1lem  38882  ntrneiel2  38884  ntrneiiso  38889  gneispace3  38931  pm11.52  39086  pm11.58  39090  pm13.192  39110  impexpdcom  39219  sbc3or  39236  opelopab4  39265  uunT12p1  39524  uunT12p2  39525  uunT12p3  39526  uun2221  39537  uun2221p1  39538  uun2221p2  39539  undif3VD  39612  ndisj2  39711  nssrex  39753  rabssf  39794  bothtbothsame  41548  bothfbothsame  41549  aiffbtbat  41557  reuabaiotaiota  41671  rmoanim  41691  2rmoswap  41696  dfodd2  42124  dfeven5  42153  dfodd7  42154  1nevenALTV  42177  oddprmne2  42199  isrng  42444  isrnghm  42460  islindeps2  42840  isldepslvec2  42842  setrec1lem3  43004  aacllem  43118