Theorem bitr4i 281

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

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3bitr2i  302  3bitr2ri  303  3bitr4i  306  3bitr4ri  307  biluk  390  biancomi  468  dfbi2  480  imdistan  578  pm5.32  584  bianass  655  mpbiran  722  biadaniALT  833  imor  867  imimorb  965  pm5.6  1017  nbi2  1033  ifpdfbi  1086  casesifp  1094  3ancoma  1115  3ancomb  1116  3anrev  1118  4anpull2  1382  dfnan2  1523  nannan  1526  nanbi  1529  xorcom  1543  xorneg  1552  xorbi12i  1553  norcom  1559  noran  1561  norasslem1  1563  trunortru  1618  trunorfal  1619  cadan  1641  cadcomb  1645  nic-ax  1705  nic-axALT  1706  nf3  1818  19.43  1914  equsv  2035  sbrimvwOLD  2128  sbcom2  2208  sb5  2309  nf5  2315  nf6  2316  sbrim  2337  sbnf  2344  sb6x  2493  2sb5rf  2501  2sb6rf  2502  sb4b  2504  sb5f  2527  sbequ8  2530  sbhb  2550  eu6lem  2598  eu1  2635  iseqsetv-cleq  2824  issettru  2838  iseqsetv-clel  2839  issetlem  2840  cleqh  2889  cleqf  2950  sbabel  2954  necon3bii  3007  neor  3047  neorian  3050  rextru  3093  r19.26m  3121  r19.43  3130  3r19.43  3131  r2allem  3150  r19.23t  3258  ralcom4  3288  moel  3385  rabid2f  3442  eqv  3460  eqvf  3461  ralv  3476  rexv  3477  reuv  3478  rmov  3479  rexcom4b  3481  ceqsex4v  3503  ceqsex8v  3505  ceqsrexv  3608  rexab  3652  ralrab2  3655  rexrab2  3657  reu2  3682  reu3  3684  reueq  3694  2reuswap  3703  2reuswap2  3704  reuind  3710  2reu5lem3  3714  2rmoswap  3718  rmo2  3833  rmoanim  3841  rmoanimALT  3842  dfss3  3897  dfss3f  3900  nssrex  3973  ssabral  3989  rabss  3995  ssrabeq  4009  uniiunlem  4012  sspsstri  4033  npss  4041  raldifb  4085  inass  4124  uncom  4157  elsymdifxor  4205  nsspssun  4213  dfss4  4214  dfun2  4215  dfin2  4216  indi  4229  reupick3  4275  eq0f  4293  neq0f  4294  eq0ALT  4297  inssdif0  4321  dfnf5  4330  rabn0  4338  vss  4357  csbab  4397  disj  4402  disj3  4406  undisj1  4414  undisj2  4415  inundif  4434  undif  4437  undifr  4438  rabsssn  4625  exsnrex  4637  euabsn2  4682  euabsn  4683  raldifsni  4754  tppreqb  4764  prssg  4774  ssunsn  4783  prneimg2  4809  preqsn  4816  pwpr  4827  pwpw0  4830  dfuni2  4868  unissb  4900  elint2  4913  ssint  4923  uniintab  4945  dfiin2g  4988  iunid  5018  iunn0  5024  iunxun  5053  iunxiun  5056  iinpw  5065  disjor  5084  disjxiun  5099  dftr2  5213  dftr3  5216  dftr4  5217  vnexOLD  5271  inuni  5310  eusv2  5357  reusv2lem4  5362  rexxfr  5377  sspwb  5416  opthneg  5449  pwssun  5542  dfid3  5548  dffr6  5606  dffr2  5611  dffr2ALT  5612  opthprc  5714  elxp3  5716  xpiundir  5722  elvv  5725  raliunxp  5815  cnvuni  5867  dmopab2rex  5898  dm0rn0OLD  5906  dfres3  5974  ssdmres  6003  elidinxp  6035  idinxpres  6038  dfima2  6057  args  6089  dffr3  6096  cotrg  6104  intasym  6108  asymref  6109  intirr  6111  xpnz  6149  xp11  6166  ssrnres  6169  xpimasn  6176  coiun  6258  coass  6267  cnvso  6291  elsnxp  6294  dfpo2  6299  imaindm  6302  dffr4  6323  dfse3  6339  frpoind  6345  dflim2  6421  orddif  6461  dffun6  6550  dffun6f  6554  dffun7  6568  dffun9  6570  funfn  6571  svrelfun  6613  mptfnf  6675  dffn2  6712  dffn3  6723  fint  6762  dffn4  6803  dff1o4  6834  brprcneu  6876  brprcneuALT  6877  eqfnfv3  7032  fnreseql  7048  fsn  7137  ftpg  7161  abrexco  7249  imaiun  7250  dff13  7259  isof1oidb  7333  isof1oopb  7334  isocnv2  7340  eloprabga  7530  mpo2eqb  7553  elovmpo  7667  mpt3eqdv  7687  funmpt3  7688  mpt3fvd  7689  sorpss  7745  abexex  7984  elxp6  8036  elxp7  8037  releldm2  8055  opiota  8071  fnmpo  8081  frxp  8141  frxp2  8164  soseq  8179  cnvimadfsn  8193  mpoxneldm  8233  dftpos4  8266  frrlem9  8316  dfrecs3  8384  tfrlem7  8395  ondif1  8513  oarec  8574  oeeu  8616  brinxper  8751  0er  8760  eroveu  8837  erovlem  8838  elixpconst  8937  domen  8992  brsdom  9005  brdom2  9013  reuen1  9057  sbthlem10  9119  brsdom2  9124  xpf1o  9162  unfi  9190  sbthfilem  9217  onfin2  9236  0sdom1domALT  9242  modom  9246  marypha2lem3  9433  wemapsolem  9548  elom3  9653  dfom5  9655  brttrcl2  9719  ttrcltr  9721  ttrclse  9732  trcl  9733  epfrs  9736  frind  9758  rankf  9806  elhf3  9917  scottexsOLD  9947  scott0bsOLD  9949  cplem1OLD  9955  hta  9966  htaOLD  9967  setrec1lem3  9973  djuexb  9994  pm54.43lem  10085  alephsuc2  10163  iscard3  10176  aceq0  10201  aceq3lem  10203  dfac3  10204  dfac5lem2  10207  dfac5  10211  dfac7  10215  dfac12a  10231  kmlem12  10244  kmlem14  10246  kmlem15  10247  infmap2  10299  ackbij2  10324  dfacfin7  10481  ituniiun  10504  zorng  10586  brdom7disj  10614  entri2  10646  alephreg  10671  fpwwe2lem11  10730  fpwwe2lem12  10731  pwfseqlem1  10747  grutsk  10911  axgroth4  10921  grothprim  10923  grothtsk  10924  elni2  10966  ltsopi  10977  genpass  11098  psslinpr  11120  ltexprlem4  11128  ltresr  11229  infm3  12280  elnnz  12707  dfz2  12716  2rexuz  13031  nnwos  13046  eluz2b1  13050  qexALT  13095  elxr  13249  dflt2  13281  xrsupss  13443  xrinfmss  13444  elixx1  13489  elioo2  13521  dfrp2  13529  elioopnf  13578  elicopnf  13580  elfz1  13648  fznn  13730  fzp1nel  13749  fznn0  13757  preduz  13788  prinfzo0  13837  injresinj  13930  nn0opthlem1  14416  faclbnd4lem1  14441  hashfxnn0  14485  hashprdifel  14546  hashgt23el  14573  hashfun  14586  hashf1  14606  fz1isolem  14610  f1oun2prg  15074  brtrclfv  15161  shftdm  15230  rediv  15304  imdiv  15311  rexanre  15520  caubnd  15532  climreu  15729  prodmo  16109  dvdslelem  16485  3dvdsdec  16508  3dvds2dec  16509  bitsval  16600  smueqlem  16666  algcvgblem  16758  lcmfunsnlem2  16821  isprm2  16863  isprm3  16864  isprm4  16865  pythagtriplem2  17001  elgz  17115  hashbc0  17189  0ram  17204  isstruct  17336  issect  17934  isfull2  18094  isfth2  18098  fucinv  18157  eldmcoa  18246  isdrs  18481  submacs  19029  isnsg4  19383  isgim  19482  gaorb  19527  oppgid  19576  oppgsubm  19582  oppgcntz  19584  ispgp  19812  efgsdm  19950  efgcpbllema  19974  iscyg2  20102  isomnd  20343  omndmul2  20353  isrng  20382  isring  20469  isirred2  20657  opprirred  20658  isrnghm  20677  dfrhm2  20710  rimval  20736  isnzr2  20774  opprsubrng  20817  opprsubrg  20851  isdomn3  20972  drngid2  21016  issdrg  21051  islmod  21145  lss1d  21244  islmhm  21308  islmim  21343  lbsextlem2  21443  lidlnz  21536  dfprm2  21785  isphl  21940  elocv  21980  iunocv  21993  isobs  22032  islinds  22121  1mavmul  22869  matunitlindflem2  23001  toprntopon  23249  isbasis3g  23273  fctop  23328  cctop  23330  isclo2  23412  restsn  23494  lmbr  23582  ist0-3  23669  2ndcdisj  23781  1stccnp  23787  islocfin  23842  1stckgenlem  23878  txbas  23892  ptbasin  23902  tx2cn  23935  fbfinnfr  24166  fbasrn  24209  filuni  24210  ufinffr  24254  fin1aufil  24257  rnelfmlem  24277  flimrest  24308  alexsubALTlem3  24374  alexsubALTlem4  24375  tgphaus  24442  istlm  24510  iscusp2  24626  metuel2  24890  isngp2  24922  isnlm  25000  isphtpc  25321  phtpcer  25322  om1elbas  25359  isclm  25391  iscvsp  25455  iscph  25497  iscau3  25605  minveclem3b  25755  elovolm  25802  ioombl1lem4  25888  dyaddisj  25923  vitali  25940  itg1climres  26041  itg2seq  26069  itg2monolem1  26077  itg2mono  26080  limcrcl  26200  lhop1  26340  itgsubst  26375  mdegleb  26388  isuc1p  26465  ismon1p  26467  plydivex  26624  ellogdm  26973  1cubr  27176  atandm2  27211  birthdaylem3  27287  dmarea  27291  dchrelbas2  27570  dchrelbas4  27576  elno3  28018  nosgnn0  28021  nosepon  28028  nocvxminlem  28146  cutcuts  28173  cutbday  28176  dmcuts  28183  cutsf  28184  ltsrec  28193  made0  28255  addsprop  28368  negsproplem2  28421  negsprop  28427  mulsprop  28522  precsexlem10  28608  elzs2  28791  elnnzs  28793  bdayfinbndlem1  28859  recut  28886  axcontlem7  29554  nb3grpr  29969  nb3grpr2  29970  upgrwlkcompim  30229  wlkson  30241  wlkonprop  30243  wksonproplem  30293  ispth  30312  wwlknon  30452  wwlksnextinj  30494  wspthsnwspthsnon  30511  elwspths2spth  30565  rusgrnumwwlkl1  30566  clwwlkccatlem  30586  erclwwlkref  30617  frgr3v  30882  nmoubi  31380  nmobndseqi  31387  nmobndseqiALT  31388  minvecolem1  31482  isch2  31831  hlimreui  31847  isch3  31849  ocsh  31891  dfch2  32015  spanuni  32152  nonbooli  32259  5oalem7  32268  adjsym  32441  elbdop2  32479  dmadjss  32495  nmopub  32516  nmfnleub  32533  nmop0h  32599  pjssposi  32780  pjordi  32781  cvbr2  32891  cvnbtwn2  32895  mdsl2i  32930  cvmdi  32932  elat2  32948  atom1d  32961  chirredi  33002  cdj3i  33049  or3di  33105  opreu2reu1  33128  mo5f  33133  reuxfrdf  33135  rexunirn  33136  difrab2  33142  rabsspr  33145  rabsstp  33146  tpssg  33181  iuninc  33203  disjorf  33221  disjunsn  33236  rabfmpunirn  33295  aciunf1  33305  funcnv5mpt  33309  eliccelico  33416  elicoelioo  33417  isslmd  33810  islinds5  33970  ismxidl  34034  1arithufdlem4  34126  hasheuni  34764  pwsiga  34809  sigainb  34816  issros  34855  2ndmbfm  34940  omssubaddlem  34978  omssubadd  34979  sitgaddlemb  35027  eulerpartlemgvv  35055  eulerpartlemn  35060  probun  35098  ballotlem2  35168  ballotlemodife  35177  bnj252  35381  bnj253  35382  bnj255  35383  bnj345  35392  bnj133  35405  bnj976  35455  bnj1098  35461  bnj121  35547  bnj130  35551  bnj150  35553  bnj581  35585  bnj607  35593  bnj865  35600  bnj917  35611  bnj934  35612  bnj964  35620  bnj983  35628  bnj996  35633  bnj1021  35643  bnj1033  35646  bnj1047  35650  bnj1049  35651  bnj1090  35656  bnj1128  35667  bnj1175  35681  bnj1189  35686  bnj1253  35694  bnj1312  35735  rmo6  35757  exdifsn  35760  scott0bOLD  35806  fineqvrep  35839  fineqvac  35841  kard0  35879  kardexen  35888  onvf1odlem4  35954  vonf1wev  35956  vonf1owevOLD  35958  vonf1osev  35960  onprcf1acwevdlem1  35965  erdszelem9  36051  erdszelem10  36052  pconnconn  36083  cvmliftiota  36153  fmlaomn0  36242  fmla0disjsuc  36250  fmlasucdisj  36251  dmopab3rexdif  36257  elmthm  36428  antnestALT  36546  nepss  36576  xpab  36584  dfso2  36613  elrn3  36620  elpotr  36636  dfon2lem5  36642  dfon2lem7  36644  dfon2lem8  36645  elwlim  36678  wzel  36679  brtxp2  36736  brpprod3a  36741  eltrans  36746  dfon3  36747  dffix2  36760  dffun10  36769  elfuns  36770  brsingle  36772  brimg  36792  funpartfun  36800  funpartfv  36802  cgrxfr  36913  segletr  36972  outsideoftr  36987  naddle  37061  neifg  37252  filnetlem4  37262  df3nandALT1  37280  weiunlem  37344  ttcwf3  37407  bj-consensusALT  37542  bj-df-ifc  37543  bj-exexalal  37569  bj-cbvaew  37636  bj-biexal3  37702  bj-alnnf  37732  bj-nfnnfTEMP  37777  bj-denoteslem  37876  bj-denotesALTV  37877  bj-ralvw  37884  bj-rexvw  37885  bj-rexcom4bv  37887  bj-rexcom4b  37888  bj-sbeq  37906  bj-inrab  37933  bj-rcleqf  38031  bj-dfmpoa  38133  bj-imdirco  38205  topdifinffinlem  38364  topdifinfeq  38367  relowlssretop  38380  relowlpssretop  38381  rdgeqoa  38387  domalom  38421  nlpineqsn  38425  fvineqsneq  38429  wl-ifpimpr  38483  wl-df3xor3  38487  wl-3xorbi  38490  wl-3xorbi2  38491  wl-2xor  38500  wl-2mintru2  38508  wl-dfclab  38611  rabiun  38615  phpreu  38621  fin2solem  38623  ptrest  38631  poimirlem25  38657  poimirlem27  38659  poimirlem30  38662  ismblfin  38673  ovoliunnfl  38674  voliunnfl  38676  volsupnfl  38677  itg2addnclem2  38684  dfprop1  38739  fdc  38773  prdstotbnd  38822  isdrngo1  38984  ispridl  39062  ismaxidl  39068  impor  39109  selconj  39126  tradd  39131  r2alan  39277  inxpss3  39346  idinxpssinxp2  39350  idinxpssinxp3  39351  dfrel5  39372  ineleq  39380  ralmo  39386  ralrnmo  39387  ralrmo3  39390  moantr  39398  dfxrn2  39411  inxpxrn  39444  rnxrnres  39448  dfsuccl4  39500  coss1cnvres  39533  1cossres  39545  cocossss  39552  cossssid4  39586  cossssid5  39587  cosscnvssid5  39594  cossid  39596  dfssr2  39605  cnvrefrelcoss2  39643  cosselcnvrefrels2  39644  eqvrelcoss  39727  eqvrelcoss2  39729  dfcoeleqvrel  39732  refrelredund4  39745  cnvepresdmqs  39764  dfcomember  39783  dfdisjALTV  39824  disjimdmqseq  39835  dfeldisj3  39837  dfeldisj4  39838  dfeldisj5  39839  disjres  39870  prter1  40030  islshp  40130  islshpat  40168  lcvbr2  40173  lcvnbtwn2  40178  cvrnbtwn3  40427  isatl  40450  ishlat1  40503  ishlat2  40504  cvrat4  40594  pmapglbx  40920  lhpexle3  41163  dib1dim  42316  diblsmopel  42322  lcfls1lem  42685  prjsperref  43728  prjspeclsp  43734  euabsn2w  43784  rexrabdioph  43895  dford4  44130  onsupuni  44325  dflim6  44360  tfsconcatlem  44432  naddgeoa  44490  ifpdfor2  44556  ifpdfan2  44558  ifpdfor  44560  ifpdfan  44561  ifpnot23b  44577  ifpnot23c  44579  ifpnot23d  44580  ifpim123g  44595  ifpbibib  44605  clss2lem  44705  imaiun1  44745  coiun1  44746  brfvrcld2  44786  iunrelexp0  44796  brtrclfv2  44821  snhesn  44880  dffrege76  45033  frege97  45054  frege98  45055  frege109  45066  frege110  45067  dffrege115  45072  frege131  45088  frege133  45090  ntrneineine1lem  45178  ntrneiel2  45180  ntrneiiso  45185  gneispace3  45227  ismnuprim  45372  ismnushort  45379  dfuniv2  45380  pm11.52  45465  pm11.58  45468  pm13.192  45488  impexpdcom  45592  sbc3or  45609  opelopab4  45628  uunT12p1  45876  uunT12p2  45877  uunT12p3  45878  uun2221  45889  uun2221p1  45890  uun2221p2  45891  undif3VD  45958  modelaxreplem3  46064  permaxext  46089  permac8prim  46098  ndisj2  46162  rabssf  46228  wrddin2  47992  chndin2  47997  chnrin2  48002  bothtbothsame  48063  bothfbothsame  48064  aiffbtbat  48072  reuabaiotaiota  48251  2reu8i  48277  2reuimp0  48278  ichn  48632  dfodd2  48828  dfeven5  48858  dfodd7  48859  1nevenALTV  48883  oddprmne2  48907  dfvopnbgr2  49045  isuspgrim0lem  49085  gpg5nbgrvtx03starlem1  49260  gpg5nbgrvtx03starlem2  49261  gpg5nbgrvtx03starlem3  49262  gpg5nbgrvtx13starlem1  49263  gpg5nbgrvtx13starlem2  49264  gpg5nbgrvtx13starlem3  49265  gpg5edgnedg  49322  dfidom2  49534  islindeps2  49689  isldepslvec2  49691  line2xlem  49959  rmotru  50007  reutru  50008  elif0  50016  isnrm4  50139  iscnrm4  50162  homf0  50217  fuco2el  50528  isthincd2  50666  thinccic  50700  istermc2  50704  istermc3  50705  dftermc3  50760  dfrals2  51055  dfralseu2  51088  aacllem  51108