Theorem 3bitr4i 302

Description: A chained inference from transitive law for logical equivalence. This inference is frequently used to apply a definition to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.)

Hypotheses

Ref	Expression
3bitr4i.1	⊢ (𝜑 ↔ 𝜓)
3bitr4i.2	⊢ (𝜒 ↔ 𝜑)
3bitr4i.3	⊢ (𝜃 ↔ 𝜓)

Assertion

Ref	Expression
3bitr4i	⊢ (𝜒 ↔ 𝜃)

Proof of Theorem 3bitr4i

Step	Hyp	Ref	Expression
1		3bitr4i.2	. 2 ⊢ (𝜒 ↔ 𝜑)
2		3bitr4i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3		3bitr4i.3	. . 3 ⊢ (𝜃 ↔ 𝜓)
4	2, 3	bitr4i 277	. 2 ⊢ (𝜑 ↔ 𝜃)
5	1, 4	bitri 274	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:  bibi2d  342  pm4.71  558  pm5.32ri  576  an31  645  pm4.14  804  or4  924  orimdi  928  orbidi  950  ordi  1003  ordir  1004  andir  1006  dfbi3  1047  dfifp7  1067  ifpdfbi  1068  ifpn  1071  ifpnOLD  1072  3orrot  1091  3orcoma  1092  3ioran  1105  3ianor  1106  3anbi123i  1154  3orbi123i  1155  an6  1444  3or6  1446  an33rean  1482  an33reanOLD  1483  nancom  1493  xorcomOLD  1512  xorass  1513  xorbi12iOLD  1523  anxordi  1525  norcomOLD  1530  norass  1537  hadbi  1598  hadcoma  1599  hadcomb  1600  hadnot  1602  cador  1608  cadan  1609  cadcoma  1612  cadnot  1615  nic-axALT  1675  nfnbiOLD  1857  19.26-3an  1874  19.43OLD  1885  19.32v  1942  19.31v  1943  19.42v  1956  4exdistr  1964  cbvexvw  2039  exexw  2053  sb3an  2083  sbcom4  2091  sbcom3vv  2097  sbal  2158  excom  2161  19.32  2225  19.31  2226  19.42  2228  equsalv  2258  sbex  2277  sbrim  2300  sbor  2303  sbbi  2304  cbvex2v  2341  eeeanv  2347  sbnf2  2355  sbievg  2360  cbvex2  2411  equsal  2416  dfsb3  2497  mo4  2565  eu6  2573  eubii  2584  dfeu  2594  sb8eulem  2597  sb8mo  2600  cbvmovw  2601  cbvmow  2602  cbvmowOLD  2603  cbveuvw  2605  cbveuw  2606  cbveuALT  2609  eu1  2611  sbmo  2615  cbvabv  2810  cbvabw  2811  cbvabwOLD  2812  cbvab  2813  abeq1  2872  nfceqi  2902  sbabelOLD  2940  ralbii2  3089  rexbii2  3090  r19.43  3122  r2allem  3136  r19.21vOLD  3174  r19.41v  3182  r19.42v  3184  r19.32v  3185  reeanlem  3213  3reeanv  3215  2ralorOLD  3217  cbvralvw  3222  cbvrexvw  3223  r19.41  3243  ralcom4OLD  3267  ralcom  3269  ralcomf  3282  rexcomf  3283  cbvralfw  3284  cbvralfwOLD  3301  cbvralf  3330  cbvrexf  3331  reu5  3352  rmobiia  3356  reubiia  3357  rmoanidOLD  3362  reuanidOLD  3363  rmo5  3370  cbvrmovw  3373  cbvreuvw  3374  moelOLD  3375  cbvrmow  3379  cbvreuw  3380  cbvrmowOLD  3385  cbvreuwOLD  3386  cbvreu  3396  cbvrmo  3397  rabbi  3428  rabid2f  3431  rabid2OLD  3433  abv  3452  abvALT  3453  cgsex4g  3485  ceqsex3v  3493  ceqsex4v  3494  ceqsex8v  3496  eueq  3653  reu2  3670  reu6  3671  reu3  3672  rmo4  3675  rmo3f  3679  2reu5  3703  cbvsbcw  3760  cbvsbcvw  3761  cbvsbc  3762  sbccomlem  3813  rmo3  3832  rmoanim  3837  rmoanimALT  3838  cbvralcsf  3887  cbvrexcsf  3888  cbvreucsf  3889  dfss2  3917  eqss  3946  uniiunlem  4030  sspsstri  4048  compleq  4093  ssequn1  4125  unss  4129  rexun  4135  ralunb  4136  elin3  4145  inass  4164  ssin  4175  elsymdif  4192  nssinpss  4201  dfun2  4204  difin  4206  indi  4218  indifdi  4228  indifdirOLD  4230  ssdif0  4308  inssdif0  4314  abn0  4325  rabeq0w  4328  rabeq0  4329  disj  4392  disj3  4398  ssundif  4430  ralidmw  4450  dfif2  4473  eldifpr  4603  rexsns  4615  snprc  4663  reusn  4673  difsnpss  4752  tpss  4780  pwpr  4844  eluni2  4854  elunirab  4866  uniun  4876  unissb  4885  unissbOLD  4886  elintrab  4904  ssintrab  4915  intun  4924  intprOLD  4927  iuncom  4944  iuncom4  4945  iunab  4994  ssiinf  4997  iunn0  5009  iinab  5010  iunin2  5013  iinun2  5015  iundif2  5016  iunun  5035  iunxun  5036  iunxiun  5039  sspwuni  5042  iinpw  5048  cbvdisj  5062  disjor  5067  brun  5138  brin  5139  brdif  5140  dftr2  5206  dftr5  5208  intexrab  5279  inuni  5282  ssext  5389  pweqb  5391  otth2  5417  propeqop  5440  vopelopabsb  5462  eqopab2bw  5481  eqopab2b  5485  pwin  5503  pwun  5505  dffr6  5566  elxp2  5632  xpiundi  5676  xpiundir  5677  poinxp  5686  soinxp  5687  frinxp  5688  seinxp  5689  weinxp  5690  inopab  5759  difopab  5760  difopabOLD  5761  raliunxp  5769  rexiunxp  5770  rexxpf  5777  iunxpf  5778  cnvco  5815  dmiun  5843  dmuni  5844  dm0rn0  5854  dmres  5933  restidsing  5980  cnvsymOLDOLD  6042  asymref  6044  codir  6048  qfto  6049  cnvopab  6065  cnvdif  6070  rniun  6074  dminss  6079  imainss  6080  difxp  6090  xpdifid  6094  dmsnn0  6133  cnvcnvsn  6145  cnvresima  6156  resco  6176  imaco  6177  rnco  6178  coiun  6182  coass  6191  ressn  6211  cnviin  6212  cnvpo  6213  cnvso  6214  xpco  6215  opreu2reurex  6220  dfpo2  6222  dflim2  6345  funcnv  6540  funcnv3  6541  fncnv  6544  fun11  6545  imadif  6555  fnres  6598  dfmpt3  6605  mptfnf  6606  fnopabg  6608  fint  6691  fin  6692  fores  6736  dff1o3  6760  f1ompt  7025  fsn  7047  imaiun  7158  isocnv2  7242  isocnv3  7243  isores2  7244  isomin  7248  eqoprab2bw  7387  eqoprab2b  7388  elpwpwel  7659  sucexb  7696  sucelon  7709  dflim4  7741  fiun  7832  f1iun  7833  f11o  7836  opabex3d  7855  opabex3rd  7856  opabex3  7857  dfopab2  7939  dfoprab3s  7940  fmpox  7954  fparlem1  7999  fparlem2  8000  suppvalbr  8030  tpostpos  8111  frrlem9  8159  wfrlem8OLD  8196  wfrfunOLD  8199  dfsmo2  8227  brwitnlem  8387  oarec  8443  qsid  8622  uniinqs  8636  mapval2  8710  mapsncnv  8731  elixp2  8739  ixpin  8761  brsdom  8815  brdom2  8822  xpassen  8910  brsdom2  8941  dif1enOLD  9006  unfilem1  9154  fiint  9168  dfsup2  9280  supmo  9288  eqinf  9320  infmo  9331  brttrcl2  9550  rankc1  9706  cp  9727  isinfcard  9928  aceq1  9953  aceq2  9955  dfac5lem3  9961  dfac10b  9975  dfac12a  9984  dffin7-2  10234  dfacfin7  10235  fin1a2lem6  10241  iunfo  10375  konigthlem  10404  axgroth6  10664  axgroth3  10667  sstskm  10678  ltexprlem1  10872  gt0srpr  10914  ltpsrpr  10945  map2psrpr  10946  ltresr  10976  fimaxre3  12001  sup3  12012  supaddc  12022  supmul1  12024  elnn0z  12412  elznn0nn  12413  zmin  12764  xrnemnf  12933  xrnepnf  12934  dfrp2  13208  elioomnf  13256  elxrge0  13269  elfzuzb  13330  fzass4  13374  elfz2nn0  13427  elfzo2  13470  elfzo3  13484  lbfzo0  13507  fzind2  13585  nn0opthlem1  14062  hashgt23el  14218  cotr2g  14766  rexfiuz  15138  fsumcom2  15565  prodmo  15725  fprodcom2  15773  sinltx  15977  divalglem4  16184  divalglem10  16190  4sqlem12  16734  imasleval  17329  xpsfrnel  17350  xpscf  17353  isssc  17609  isffth2  17709  ispos2  18110  ismhm  18509  issubmndb  18521  nsgacs  18866  isgim  18954  oppgcntz  19047  f1omvdco3  19133  pmtrprfvalrn  19172  efgrelexlemb  19431  pgpfac1  19758  pgpfac  19762  issrg  19818  opprsubg  19953  opprunit  19978  isirred2  20018  opprirred  20019  drngprop  20084  opprdrng  20097  issdrg2  20148  islss  20279  islbs  20421  isdomn2  20653  unocv  20968  iunocv  20969  isbasis2g  22181  tgval2  22189  ntreq0  22311  isclo2  22322  cmpcov2  22624  is1stc2  22676  1stcelcls  22695  llyi  22708  unisngl  22761  txuni2  22799  xkobval  22820  hausdiag  22879  isfbas2  23069  elfg  23105  fbasrn  23118  fmfnfmlem3  23190  isfcls  23243  alexsubALTlem2  23282  istmd  23308  istgp  23311  istrg  23398  istdrg  23400  istdrg2  23412  isms2  23686  metuel2  23804  restmetu  23809  isngp  23835  isngp2  23836  isngp3  23837  elii1  24181  isncvsngp  24396  iscph  24417  isbn  24585  pmltpc  24697  ovolfcl  24713  finiunmbl  24791  iundisj  24795  dyaddisj  24843  vitalilem1  24855  ellimc3  25126  ig1pval3  25422  plyun0  25441  plydivex  25540  aannenlem2  25572  ellogrn  25798  atandm  26109  atandm3  26111  atans2  26164  elno3  26886  tgjustf  26970  colinearalg  27414  axeuclid  27467  nbgrsym  27866  upgrtrls  28205  upgristrl  28206  usgr2pth0  28269  iswwlks  28337  isclwwlk  28484  clwwlkneq0  28529  h2hlm  29478  issh  29706  chcon2i  29962  chcon1i  29963  chcon3i  29964  chnlei  29983  cmcm2i  30091  cmcm3i  30092  3oalem3  30162  pjdifnormii  30181  pjneli  30221  dfadj2  30383  cnvadj  30390  hhcno  30402  hhcnf  30403  eleigvec  30455  eleigvec2  30456  pjimai  30674  isst  30711  ishst  30712  cvnbtwn4  30787  chrelat4i  30871  2reucom  30964  reuxfrdf  30975  difrab2  30981  inpr0  31015  iunin1f  31032  disjnf  31044  cbvdisjf  31045  disjorf  31053  iundisjf  31063  disjexc  31067  xrdifh  31236  iundisjfi  31252  hashxpe  31262  pmtrprfv2  31492  xrnarchi  31573  isorng  31640  prmidl0  31765  ccfldextdgrr  31882  cmpcref  31940  ordtconnlem1  32014  isrrext  32090  cntnevol  32336  ddemeas  32344  omssubaddlem  32406  omssubadd  32407  eulerpartleme  32470  eulerpartlemv  32471  eulerpartlemt0  32476  eulerpartlemgvv  32483  eulerpartlemn  32488  ballotlem2  32595  ballotlemodife  32604  oddprm2  32775  bnj257  32826  bnj268  32828  bnj290  32829  bnj312  32831  bnj89  32840  bnj887  32884  bnj976  32896  bnj1019  32898  bnj1146  32910  bnj1385  32951  bnj110  32977  bnj121  32989  bnj130  32993  bnj153  32999  bnj543  33012  bnj580  33032  bnj607  33035  bnj849  33044  bnj882  33045  bnj916  33052  bnj985v  33072  bnj985  33073  bnj1033  33088  bnj1083  33097  bnj1090  33098  bnj1128  33109  bnj1174  33122  bnj1228  33130  erdszelem1  33292  cvmliftlem15  33399  snmlval  33432  satfvsuclem2  33461  satfdm  33470  elmpst  33637  mpstrcl  33642  untuni  33789  dfso3  33801  reurab  33809  xpab  33812  ot2elxp  33814  otthne  33817  dftr6  33852  coep  33853  coepr  33854  dffr5  33855  dfso2  33856  cnvco1  33860  cnvco2  33861  eldm3  33862  dfdm5  33878  dfrn5  33879  imaindm  33884  conway  34067  eqscut2  34074  madeval2  34111  brsset  34265  idsset  34266  dfon3  34268  dfbigcup2  34275  dfom5b  34288  dffun10  34290  dfiota3  34299  fnimage  34305  brdomain  34309  brrange  34310  brimg  34313  brapply  34314  brcup  34315  brcap  34316  brsuccf  34317  funpartlem  34318  brrestrict  34325  dfrecs2  34326  brub  34330  altopelaltxp  34352  trer  34579  filnetlem4  34644  df3nandALT1  34662  imnand2  34665  bj-dfbi5  34829  bj-bixor  34847  bj-nnfnt  34996  bj-sbnf  35097  bj-csbsnlem  35161  bj-rcleqf  35287  bj-sscon  35291  bj-pw0ALT  35294  bj-restpw  35335  bj-opelidb1  35396  bj-imdiridlem  35428  bj-imdirco  35433  wl-df3xor2  35712  wl-3xorrot  35720  wl-3xorcoma  35721  wl-3xornot  35724  wl-df2-3mintru2  35728  wl-df3-3mintru2  35729  wl-df4-3mintru2  35730  wl-equsalvw  35769  iundif1  35823  poimirlem25  35874  poimirlem26  35875  poimirlem30  35879  ismblfin  35890  mbfposadd  35896  itg2addnclem2  35901  ftc1anc  35930  inixp  35958  prdstotbnd  36024  heibor1lem  36039  isrngohom  36195  isidl  36244  isfldidl2  36299  isdmn3  36304  sbccom2lem  36354  triantru3  36457  vvdifopab  36492  brres2  36500  eldmqsres  36519  inxpss  36544  ref5  36546  n0el2  36566  trcoss2  36718  dfeqvrel2  36824  dfeqvrel3  36825  redundeq1  36863  redundpbi1  36865  refrelredund4  36869  funALTVfun  36932  dfeldisj3  36953  dfeldisj5  36955  pet0  37049  petid  37051  petidres  37053  petinidres  37055  petxrnidres  37057  mpet  37073  petincnvepres  37083  pet  37085  pmapglbx  38004  lhpexle3  38247  cdleme25cv  38593  dicelval3  39415  diclspsn  39429  lcfls1c  39771  sn-axrep5v  40409  sn-iotalem  40414  psspwb  40422  moxfr  40730  fphpd  40854  ifpim1  41310  ifpnot  41311  ifpid2  41312  ifpim2  41313  ifpxorcor  41317  ifpnot23  41319  ifpananb  41347  ifpnannanb  41348  ifpxorxorb  41352  rp-fakeinunass  41356  snen1g  41365  pren2  41394  alephiso2  41399  undmrnresiss  41446  cnvssco  41448  cotrintab  41456  cnviun  41492  imaiun1  41493  coiun1  41494  elintima  41495  frege133d  41607  frege54cor0a  41705  or3or  41865  andi3or  41866  ntrneik4w  41944  k0004lem1  41991  ismnuprim  42146  ismnushort  42153  undisjrab  42158  nzss  42169  pm10.541  42219  compab  42294  onfrALTlem5  42396  onfrALTlem5VD  42739  inn0f  42855  eluni2f  42887  euabsneu  44787  aiotaexb  44846  aiotavb  44847  r19.32  44855  3an4ancom24  45026  ichn  45173  ichcom  45176  ichbi12i  45177  prproropf1olem0  45219  pairreueq  45227  issubmgm  45608  sgrp2sgrp  45687  islindeps  46059  elbigo  46162  reutruALT  46417  isthincd2  46584  setrec1lem3  46660  elpg  46684