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

Syntax hints:   ↔ wb 205

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 206

This theorem is referenced by:  3bitr2i  299  3bitr2ri  300  3bitr4i  303  3bitr4ri  304  biluk  387  biancomi  464  dfbi2  476  imdistan  569  pm5.32  575  bianass  641  mpbiran  708  biadaniALT  820  imor  852  imimorb  950  pm5.6  1001  nbi2  1015  casesifp  1078  3ancoma  1099  3ancomb  1100  3anrev  1102  an3andi  1483  dfnan2  1493  nannan  1496  nanbi  1499  xorcom  1513  xorneg  1523  xorbi12i  1524  norcom  1531  noran  1534  norasslem1  1536  trunortru  1591  trunorfal  1592  cadan  1611  cadcomb  1615  nic-ax  1676  nic-axALT  1677  nf3  1789  nfnbiOLD  1859  19.43  1886  equsv  2007  sbrimvw  2095  sbcom2  2162  sb5  2268  nf5  2279  nf6  2280  sbrim  2301  sb6x  2464  2sb5rf  2472  2sb6rf  2473  sb4b  2475  sb5f  2498  sbequ8  2501  sbhb  2521  eu6lem  2568  eu1  2607  issetlem  2814  cleqh  2864  clelabOLD  2881  cleqf  2935  sbabel  2939  necon3bii  2994  neor  3035  neorian  3038  rextru  3078  r19.26m  3111  r19.26-3  3113  r19.43  3123  r2allem  3143  r19.23t  3253  ralcom4  3284  rexcomOLD  3289  moel  3399  moelOLD  3402  rabid2f  3464  rabid2OLD  3466  eqv  3484  eqvf  3485  ralv  3499  rexv  3500  reuv  3501  rmov  3502  rexcom4b  3504  ceqsex4v  3533  ceqsex8v  3535  ceqsrexv  3643  rexab  3690  ralrab2  3694  rexrab2  3696  reu2  3721  reu3  3723  reueq  3733  2reuswap  3742  2reuswap2  3743  reuind  3749  2reu5lem3  3753  2rmoswap  3757  sbc3an  3847  rmo2  3881  rmoanim  3888  rmoanimALT  3889  dfss2  3968  dfss2OLD  3969  dfss3  3970  dfss3f  3973  ssabral  4059  rabss  4069  ssrabeq  4082  uniiunlem  4084  sspsstri  4102  npss  4110  dfdif3  4114  raldifb  4144  uncom  4153  inass  4219  elsymdifxor  4249  nsspssun  4257  dfss4  4258  dfun2  4259  dfin2  4260  indi  4273  indifdirOLD  4285  difin2  4291  reupick3  4319  eq0f  4340  neq0f  4341  eq0  4343  eq0ALT  4344  dfnf5  4377  rabn0  4385  csbab  4437  vss  4443  disj  4447  disjOLD  4448  disj3  4453  undisj1  4461  undisj2  4462  inundif  4478  undif  4481  undifr  4482  rabsssn  4670  exsnrex  4684  euabsn2  4729  euabsn  4730  raldifsni  4798  tppreqb  4808  pwpw0  4816  prssg  4822  ssunsn  4831  preqsn  4862  pwpr  4902  dfuni2  4910  unissb  4943  unissbOLD  4944  elint2  4957  ssint  4968  uniintab  4992  dfiin2g  5035  iunid  5063  iunn0  5070  iunxun  5097  iunxiun  5100  iinpw  5109  disjor  5128  disjxiun  5145  dftr2  5267  dftr5OLD  5270  dftr3  5271  dftr4  5272  axrep6  5292  vnex  5314  inuni  5343  eusv2  5394  reusv2lem4  5399  rexxfr  5414  sspwb  5449  opthneg  5481  pwssun  5571  dfid3  5577  dffr6  5634  dffr2  5640  dffr2ALT  5641  opthprc  5739  elxp3  5741  xpiundir  5746  elvv  5749  reliun  5815  inxp  5831  raliunxp  5838  cnvuni  5885  dmopab2rex  5916  dm0rn0  5923  dfres3  5985  ssdmres  6003  elidinxp  6042  idinxpres  6045  dfima2  6060  args  6089  dffr3  6096  cotrg  6106  cotrgOLD  6107  cotrgOLDOLD  6108  intasym  6114  asymref  6115  intirr  6117  xpnz  6156  xp11  6172  ssrnres  6175  xpimasn  6182  coiun  6253  coass  6262  cnvso  6285  elsnxp  6288  dfpo2  6293  imaindm  6296  dffr4  6318  dfse3  6335  frpoind  6341  wfiOLD  6350  dflim2  6419  orddif  6458  dffun2OLDOLD  6553  dffun6  6554  dffun6f  6559  dffun7  6573  dffun9  6575  funfn  6576  svrelfun  6618  mptfnf  6683  dffn2  6717  dffn3  6728  fint  6768  dffn4  6809  dff1o4  6839  brprcneu  6879  brprcneuALT  6880  eqfnfv3  7032  fnreseql  7047  fsn  7130  ftpg  7151  abrexco  7240  imaiun  7241  dff13  7251  isof1oidb  7318  isof1oopb  7319  isocnv2  7325  eloprabga  7513  mpo2eqb  7538  elovmpo  7648  sorpss  7715  abexex  7955  elxp6  8006  elxp7  8007  releldm2  8026  opiota  8042  fnmpo  8052  frxp  8109  frxp2  8127  soseq  8142  cnvimadfsn  8154  mpoxneldm  8194  dftpos4  8227  frrlem9  8276  wfrlem8OLD  8313  wfrfunOLD  8316  dfrecs3  8369  dfrecs3OLD  8370  tfrlem7  8380  ondif1  8498  oarec  8559  oeeu  8600  0er  8737  eroveu  8803  erovlem  8804  elixpconst  8896  domen  8954  brsdom  8968  brdom2  8975  reuen1  9022  sbthlem10  9089  brsdom2  9094  xpf1o  9136  unfi  9169  sbthfilem  9198  onfin2  9228  0sdom1domALT  9236  modom  9241  unfiOLD  9310  marypha2lem3  9429  wemapsolem  9542  elom3  9640  dfom5  9642  brttrcl2  9706  ttrcltr  9708  ttrclse  9719  trcl  9720  epfrs  9723  frind  9742  rankf  9786  scottexs  9879  scott0s  9880  cplem1  9881  hta  9889  djuexb  9901  pm54.43lem  9992  alephsuc2  10072  iscard3  10085  aceq0  10110  aceq3lem  10112  dfac3  10113  dfac5lem2  10116  dfac5  10120  dfac7  10124  dfac12a  10140  kmlem12  10153  kmlem14  10155  kmlem15  10156  infmap2  10210  ackbij2  10235  dfacfin7  10391  ituniiun  10414  zorng  10496  brdom7disj  10523  entri2  10550  alephreg  10574  fpwwe2lem11  10633  fpwwe2lem12  10634  pwfseqlem1  10650  grutsk  10814  axgroth4  10824  grothprim  10826  grothtsk  10827  elni2  10869  ltsopi  10880  genpass  11001  psslinpr  11023  ltexprlem4  11031  ltresr  11132  1re  11211  infm3  12170  elnnz  12565  dfz2  12574  2rexuz  12881  nnwos  12896  eluz2b1  12900  qexALT  12945  elxr  13093  dflt2  13124  xrsupss  13285  xrinfmss  13286  elixx1  13330  elioo2  13362  dfrp2  13370  elioopnf  13417  elicopnf  13419  elfz1  13486  fznn  13566  fzp1nel  13582  fznn0  13590  preduz  13620  prinfzo0  13668  injresinj  13750  nn0opthlem1  14225  faclbnd4lem1  14250  hashfxnn0  14294  hashprdifel  14355  hashgt23el  14381  hashfun  14394  hashf1  14415  fz1isolem  14419  f1oun2prg  14865  brtrclfv  14946  shftdm  15015  rediv  15075  imdiv  15082  rexanre  15290  caubnd  15302  climreu  15497  prodmo  15877  dvdslelem  16249  3dvdsdec  16272  3dvds2dec  16273  bitsval  16362  smueqlem  16428  algcvgblem  16511  lcmfunsnlem2  16574  isprm2  16616  isprm3  16617  isprm4  16618  pythagtriplem2  16747  elgz  16861  hashbc0  16935  0ram  16950  isstruct  17082  issect  17697  isfull2  17859  isfth2  17863  fucinv  17923  eldmcoa  18012  isdrs  18251  submacs  18705  isnsg4  19042  isgim  19131  gaorb  19166  oppgid  19218  oppgsubm  19224  oppgcntz  19226  ispgp  19455  efgsdm  19593  efgcpbllema  19617  iscyg2  19745  isring  20054  isirred2  20228  opprirred  20229  dfrhm2  20246  isnzr2  20290  drngid2  20329  opprsubrg  20377  issdrg  20397  islmod  20468  lss1d  20567  islmhm  20631  islmim  20666  lbsextlem2  20765  lidlnz  20846  dfprm2  21035  isphl  21173  elocv  21213  iunocv  21226  isobs  21267  islinds  21356  1mavmul  22042  toprntopon  22419  isbasis3g  22444  fctop  22499  cctop  22501  isclo2  22584  restsn  22666  lmbr  22754  ist0-3  22841  2ndcdisj  22952  1stccnp  22958  islocfin  23013  1stckgenlem  23049  txbas  23063  ptbasin  23073  tx2cn  23106  fbfinnfr  23337  fbasrn  23380  filuni  23381  ufinffr  23425  fin1aufil  23428  rnelfmlem  23448  flimrest  23479  alexsubALTlem3  23545  alexsubALTlem4  23546  tgphaus  23613  istlm  23681  iscusp2  23799  metuel2  24066  isngp2  24098  isnlm  24184  isphtpc  24502  phtpcer  24503  om1elbas  24540  isclm  24572  iscvsp  24636  iscph  24679  iscau3  24787  minveclem3b  24937  elovolm  24984  ioombl1lem4  25070  dyaddisj  25105  vitali  25122  itg1climres  25224  itg2seq  25252  itg2monolem1  25260  itg2mono  25263  limcrcl  25383  lhop1  25523  itgsubst  25558  mdegleb  25574  isuc1p  25650  ismon1p  25652  plydivex  25802  ellogdm  26139  1cubr  26337  atandm2  26372  birthdaylem3  26448  dmarea  26452  dchrelbas2  26730  dchrelbas4  26736  elno3  27148  nosgnn0  27151  nosepon  27158  nocvxminlem  27269  scutcut  27292  scutbday  27295  dmscut  27302  scutf  27303  sltrec  27311  made0  27358  addsprop  27450  negsproplem2  27493  negsprop  27499  mulsprop  27576  precsexlem10  27652  axcontlem7  28218  nb3grpr  28629  nb3grpr2  28630  upgrwlkcompim  28890  wlkson  28903  wlkonprop  28905  wksonproplem  28951  wksonproplemOLD  28952  ispth  28970  wwlknon  29101  wwlksnextinj  29143  wspthsnwspthsnon  29160  elwspths2spth  29211  rusgrnumwwlkl1  29212  clwwlkccatlem  29232  erclwwlkref  29263  frgr3v  29518  nmoubi  30013  nmobndseqi  30020  nmobndseqiALT  30021  minvecolem1  30115  isch2  30464  hlimreui  30480  isch3  30482  ocsh  30524  dfch2  30648  spanuni  30785  nonbooli  30892  5oalem7  30901  adjsym  31074  elbdop2  31112  dmadjss  31128  nmopub  31149  nmfnleub  31166  nmop0h  31232  pjssposi  31413  pjordi  31414  cvbr2  31524  cvnbtwn2  31528  mdsl2i  31563  cvmdi  31565  elat2  31581  atom1d  31594  chirredi  31635  cdj3i  31682  or3di  31689  opreu2reu1  31712  mo5f  31717  reuxfrdf  31719  rexunirn  31720  difrab2  31726  iuninc  31780  disjorf  31798  disjunsn  31813  rabfmpunirn  31866  aciunf1  31876  funcnv5mpt  31881  eliccelico  31976  elicoelioo  31977  isomnd  32207  omndmul2  32218  isslmd  32335  islinds5  32469  ismxidl  32567  hasheuni  33072  pwsiga  33117  sigainb  33123  issros  33162  2ndmbfm  33249  omssubaddlem  33287  omssubadd  33288  sitgaddlemb  33336  eulerpartlemgvv  33364  eulerpartlemn  33369  probun  33407  ballotlem2  33476  ballotlemodife  33485  bnj252  33703  bnj253  33704  bnj255  33705  bnj345  33714  bnj133  33727  bnj976  33777  bnj1098  33783  bnj121  33870  bnj130  33874  bnj150  33876  bnj581  33908  bnj607  33916  bnj865  33923  bnj917  33934  bnj934  33935  bnj964  33943  bnj983  33951  bnj996  33956  bnj1021  33966  bnj1033  33969  bnj1047  33973  bnj1049  33974  bnj1090  33979  bnj1128  33990  bnj1175  34004  bnj1189  34009  bnj1253  34017  bnj1312  34058  exdifsn  34073  fineqvrep  34084  fineqvac  34086  erdszelem9  34179  erdszelem10  34180  pconnconn  34211  cvmliftiota  34281  fmlaomn0  34370  fmla0disjsuc  34378  fmlasucdisj  34379  dmopab3rexdif  34385  elmthm  34556  nepss  34676  xpab  34684  dfso2  34714  elrn3  34721  elpotr  34742  dfon2lem5  34748  dfon2lem7  34750  dfon2lem8  34751  elwlim  34784  wzel  34785  brtxp2  34842  brpprod3a  34847  eltrans  34852  dfon3  34853  dffix2  34866  dffun10  34875  elfuns  34876  brsingle  34878  brimg  34898  funpartfun  34904  funpartfv  34906  cgrxfr  35016  segletr  35075  outsideoftr  35090  neifg  35245  filnetlem4  35255  df3nandALT1  35273  bj-consensusALT  35445  bj-df-ifc  35446  bj-biexal3  35574  bj-nfnnfTEMP  35625  bj-denoteslem  35739  bj-denotes  35740  bj-ralvw  35748  bj-rexvw  35749  bj-rexcom4bv  35751  bj-rexcom4b  35752  bj-sbeq  35770  bj-inrab  35796  bj-rcleqf  35895  bj-dfmpoa  35988  bj-imdirco  36060  topdifinffinlem  36217  topdifinfeq  36220  relowlssretop  36233  relowlpssretop  36234  rdgeqoa  36240  domalom  36274  nlpineqsn  36278  fvineqsneq  36282  wl-ifpimpr  36336  wl-df3xor3  36340  wl-3xorbi  36343  wl-3xorbi2  36344  wl-2xor  36353  wl-2mintru2  36361  wl-dfclab  36447  rabiun  36450  phpreu  36461  fin2solem  36463  matunitlindflem2  36474  ptrest  36476  poimirlem25  36502  poimirlem27  36504  poimirlem30  36507  ismblfin  36518  ovoliunnfl  36519  voliunnfl  36521  volsupnfl  36522  itg2addnclem2  36529  fdc  36602  prdstotbnd  36651  isdrngo1  36813  ispridl  36891  ismaxidl  36897  impor  36938  selconj  36957  tradd  36962  scott0f  37026  r2alan  37105  inxpss3  37172  idinxpssinxp2  37176  idinxpssinxp3  37177  dfrel5  37204  ineleq  37212  moantr  37222  dfxrn2  37235  inxpxrn  37254  rnxrnres  37258  coss1cnvres  37276  1cossres  37288  cocossss  37295  cossssid4  37329  cossssid5  37330  cosscnvssid5  37337  cossid  37339  dfssr2  37358  cnvrefrelcoss2  37396  cosselcnvrefrels2  37397  eqvrelcoss  37476  eqvrelcoss2  37478  dfcoeleqvrel  37481  refrelredund4  37494  cnvepresdmqs  37512  dfcomember  37531  dfdisjALTV  37572  dfeldisj3  37578  dfeldisj4  37579  dfeldisj5  37580  disjres  37603  prter1  37738  islshp  37838  islshpat  37876  lcvbr2  37881  lcvnbtwn2  37886  cvrnbtwn3  38135  isatl  38158  ishlat1  38211  ishlat2  38212  cvrat4  38303  pmapglbx  38629  lhpexle3  38872  dib1dim  40025  diblsmopel  40031  lcfls1lem  40394  prjsperref  41345  prjspeclsp  41351  rexrabdioph  41518  dford4  41754  isdomn3  41932  onsupuni  41964  dflim6  42000  tfsconcatlem  42072  naddgeoa  42131  ifpdfor2  42198  ifpdfan2  42200  ifpdfor  42202  ifpdfan  42203  ifpnot23b  42219  ifpnot23c  42221  ifpnot23d  42222  ifpim123g  42237  ifpbibib  42247  clss2lem  42348  imaiun1  42388  coiun1  42389  brfvrcld2  42429  iunrelexp0  42439  brtrclfv2  42464  snhesn  42523  dffrege76  42676  frege97  42697  frege98  42698  frege109  42709  frege110  42710  dffrege115  42715  frege131  42731  frege133  42733  ntrneineine1lem  42821  ntrneiel2  42823  ntrneiiso  42828  gneispace3  42870  scotteld  42991  ismnuprim  43039  ismnushort  43046  dfuniv2  43047  pm11.52  43132  pm11.58  43135  pm13.192  43155  impexpdcom  43262  sbc3or  43279  opelopab4  43298  uunT12p1  43547  uunT12p2  43548  uunT12p3  43549  uun2221  43560  uun2221p1  43561  uun2221p2  43562  undif3VD  43629  ndisj2  43724  nssrex  43761  rabssf  43794  bothtbothsame  45596  bothfbothsame  45597  aiffbtbat  45605  reuabaiotaiota  45782  2reu8i  45808  2reuimp0  45809  ichn  46111  dfodd2  46291  dfeven5  46321  dfodd7  46322  1nevenALTV  46346  oddprmne2  46370  isrng  46637  isrnghm  46676  opprsubrng  46723  islindeps2  47118  isldepslvec2  47120  line2xlem  47393  rmotru  47443  reutru  47444  isnrm4  47517  iscnrm4  47541  isthincd2  47612  thinccic  47635  setrec1lem3  47688  aacllem  47802