Theorem 3bitr4g 314

Description: More general version of 3bitr4i 303. Useful for converting definitions in a formula. (Contributed by NM, 11-May-1993.)

Hypotheses

Ref	Expression
3bitr4g.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
3bitr4g.2	⊢ (𝜃 ↔ 𝜓)
3bitr4g.3	⊢ (𝜏 ↔ 𝜒)

Assertion

Ref	Expression
3bitr4g	⊢ (𝜑 → (𝜃 ↔ 𝜏))

Proof of Theorem 3bitr4g

Step	Hyp	Ref	Expression
1		3bitr4g.2	. . 3 ⊢ (𝜃 ↔ 𝜓)
2		3bitr4g.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	bitrid 283	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
4		3bitr4g.3	. 2 ⊢ (𝜏 ↔ 𝜒)
5	3, 4	bitr4di 289	1 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  bibi1d  343  pm5.32rd  578  orbi2d  916  orbi1d  917  ifpbi123d  1079  3orbi123d  1437  3anbi123d  1438  nanbi1  1501  nanbi2  1502  xorbi12d  1525  hadbi123d  1595  had0  1604  cadbi123d  1610  nfbiit  1851  nfbidv  1922  sbequ  2083  nfbidf  2224  drex1v  2374  drnf1v  2375  drnf1vOLD  2376  drex1  2446  drnf1  2448  sb4b  2480  drsb1  2500  eujustALT  2572  eubi  2584  eleq1ab  2716  eqeq1d  2739  eqeq1dALT  2740  eqeq2d  2748  abbi  2807  eleq1w  2824  eleq2w  2825  eleq1d  2826  eleq2d  2827  eleq2dALT  2828  eqabdv  2875  nfceqdf  2901  drnfc1  2925  drnfc2  2926  neleq12d  3051  ralrexbidOLD  3107  ralbidv2  3174  rexbidv2  3175  r19.21t  3253  r19.23t  3255  ralbidaOLD  3271  rexbida  3272  rexeq  3322  raleqbidvvOLD  3335  cbvraldva2  3348  cbvrexdva2OLD  3350  raleqf  3353  rexeqfOLD  3355  ralcom2  3377  rmobidva  3395  reubidva  3396  rmobida  3406  reubida  3407  rmoeq1  3416  reueq1  3417  rmoeq1OLD  3418  reueq1OLD  3419  reueqbidv  3423  rmoeq1f  3424  reueq1f  3425  dfsbcq  3790  sbceqbid  3795  sbcbid  3844  sbcbi2  3848  eqsbc2  3854  sbcrext  3873  sbcabel  3878  ralss  4058  rexss  4059  psseq1  4090  psseq2  4091  ssconb  4142  uneq1  4161  difin2  4301  rcompleq  4305  reuun2  4325  sbcnel12g  4414  sbnfc2  4439  reldisj  4453  undif4  4467  disjssun  4468  pssdifcom1  4490  pssdifcom2  4491  sbcssg  4520  eltpg  4686  raltpg  4698  rextpg  4699  r19.12sn  4720  intmin4  4977  dfiun2g  5030  dfiun2gOLD  5031  iindif1  5075  iindif2  5077  iinin2  5078  disjprg  5139  disjxun  5141  breq  5145  breq1  5146  breq2  5147  treq  5267  reusv2lem5  5402  rexxfrd  5409  rexxfr2d  5411  rexxfrd2  5413  rabxfrd  5417  opthg2  5484  oteqex2  5504  oteqex  5505  poeq1  5595  soeq1  5613  freq1  5652  weeq1  5672  weeq2  5673  opthprc  5749  wesn  5774  releq  5786  sbcrel  5790  eqrel  5794  eqrelrel  5807  xpiindi  5846  dmopab2rex  5928  dfres3  6002  brres  6004  resieq  6008  dmsnopg  6233  dfco2a  6266  dfpo2  6316  ordeq  6391  limeq  6396  ordunisssuc  6490  iotaeq  6526  sniota  6552  sbcfung  6590  imadif  6650  fneq1  6659  fneq2  6660  feq1  6716  feq2  6717  feq3  6718  sbcfng  6733  sbcfg  6734  f1eq1  6799  f1eq2  6800  f1eq3  6801  foeq1  6816  foeq2  6817  foeq3  6818  f1oeq1  6836  f1oeq2  6837  f1oeq3  6838  mpteqb  7035  rexrnmptw  7115  rexrnmpt  7117  dffo3  7122  dffo3f  7126  fmptco  7149  rexima  7258  dff13  7275  f1imaeq  7285  f1imapss  7286  cbvexfo  7310  f1eqcocnv  7321  fliftcnv  7331  isoeq1  7337  isoeq2  7338  isoeq3  7339  isoeq4  7340  isoeq5  7341  isomin  7357  isowe  7369  eqfunresadj  7380  imaeqsalvOLD  7384  nfriotadw  7396  mpoeq123  7505  rexrnmpo  7573  iunpw  7791  tfinds  7881  resf1extb  7956  fiun  7967  f1iun  7968  opiota  8084  xpord3pred  8177  ottpos  8261  dmtpos  8263  onoviun  8383  smoeq  8390  smoiso2  8409  tfr2b  8436  oarec  8600  oeeui  8640  nnacan  8666  nnmcan  8672  ereq1  8752  ereq2  8753  elecg  8789  ereldm  8795  ixpiin  8964  boxriin  8980  boxcutc  8981  omxpenlem  9113  enfiALT  9228  nnsdomo  9270  isfinite2  9334  ixpfi2  9390  elfi2  9454  fipwss  9469  ttrclse  9767  ennum  9987  cardsdom2  10028  aleph11  10124  alephiso  10138  fin23lem26  10365  compssiso  10414  isf34lem4  10417  isfin5-2  10431  fin1a2lem5  10444  brdom7disj  10571  brdom6disj  10572  fpwwe2lem7  10677  fpwwe2lem11  10681  fpwwe2lem12  10682  genpass  11049  ltasr  11140  axpre-lttri  11205  infm3  12227  creur  12260  eqreznegel  12976  rpneg  13067  ltxr  13157  icoshftf1o  13514  elfzm11  13635  elfzomelpfzo  13810  nn0ennn  14020  nnesq  14266  hashbclem  14491  hashf1lem1  14494  leiso  14498  fz1isolem  14500  pr2pwpr  14518  repsdf2  14816  dfrtrclrec2  15097  rexfiuz  15386  cau4  15395  ello1mpt2  15558  o1lo1  15573  fsumcom2  15810  incexc2  15874  fprodcom2  16020  dvdsflip  16354  bitsmod  16473  bitscmp  16475  smueqlem  16527  divgcdcoprm0  16702  hashdvds  16812  prmreclem2  16955  vdwapun  17012  vdwmc2  17017  imasaddfnlem  17573  comfeq  17749  oppcsect  17822  funcres2b  17942  funcpropd  17947  fullpropd  17967  fthpropd  17968  fthres2b  17977  fthres2c  17978  fullres2c  17986  ffthres2c  17987  fucsect  18020  fucinv  18021  setcsect  18134  pospropd  18372  tosso  18464  odulatb  18479  oduclatb  18552  odudlatb  18570  isipodrs  18582  mgmhmpropd  18711  issgrpv  18734  issgrpn0  18735  mndpropd  18772  mhmpropd  18805  issubm2  18817  efmnd1bas  18906  grppropd  18969  grpinvcnv  19024  conjghm  19267  conjnmzb  19271  ghmpropd  19274  gapm  19324  symg1bas  19408  pmtrfrn  19476  cmnpropd  19809  ablpropd  19810  eqgabl  19852  gsumcom2  19993  dmdprd  20018  dprdw  20030  subgdmdprd  20054  pgpfac1lem2  20095  pgpfac1lem4  20098  rngpropd  20171  ringpropd  20285  crngpropd  20286  crngunit  20378  unitpropd  20417  isnirred  20420  nzrpropd  20520  issubrng  20547  subrngpropd  20568  resrhm2b  20602  subrgpropd  20608  rhmpropd  20609  rngcsect  20636  ringcsect  20670  isdomn3  20715  drngpropd  20769  fldpropd  20770  fiidomfld  20775  acsfn1p  20800  abvpropd  20836  lmodprop2d  20922  lsspropd  21016  lmhmpropd  21072  lbspropd  21098  lmhmlvec  21109  lvecprop2d  21168  lvecpropd  21169  df2idl2rng  21266  pzriprnglem10  21501  phlpropd  21673  assapropd  21892  psrbagconf1o  21949  mplmonmul  22054  ismhp3  22146  mat1dimbas  22478  tpspropd  22944  tgss2  22994  lmbr2  23267  ist1-2  23355  ist1-3  23357  subislly  23489  dissnlocfin  23537  iskgen3  23557  txcnmpt  23632  hausdiag  23653  hauseqlcld  23654  xkococnlem  23667  tgqtop  23720  txhmeo  23811  uffix2  23932  ufildr  23939  txflf  24014  tgphaus  24125  qustgplem  24129  qustgphaus  24131  xpsdsval  24391  blin  24431  blres  24441  xmeterval  24442  xmspropd  24483  mspropd  24484  setsms  24492  metequiv  24522  metustsym  24568  restmetu  24583  ngppropd  24650  xrtgioo  24828  metdsge  24871  icopnfcnv  24973  iccpnfcnv  24975  lmhmclm  25120  lmmbr  25292  equivcmet  25351  cmspropd  25383  iunmbl2  25592  ioombl1lem4  25596  mbfaddlem  25695  i1fmullem  25729  itg1mulc  25739  iblcnlem1  25823  iblrelem  25826  iblre  25829  iblcn  25834  limcun  25930  mvth  26031  ofmulrt  26323  resinf1o  26578  quad2  26882  1cubr  26885  dcubic  26889  wilthlem2  27112  dvdsflf1o  27230  dvdsflsumcom  27231  fsumvma  27257  vmasum  27260  logfac2  27261  logfaclbnd  27266  dchrelbas3  27282  lgsquadlem1  27424  lgsquadlem2  27425  eqscut2  27851  mulsrid  28139  readdscl  28431  ax5seg  28953  ushgredgedg  29246  ushgredgedgloop  29248  nbumgrvtx  29363  upgriswlk  29659  wspniunwspnon  29943  rusgrnumwwlkb0  29991  isclwwlknx  30055  clwwlknscsh  30081  clwwlknonel  30114  0trl  30141  0spth  30145  0clwlk  30149  0crct  30152  0cycl  30153  eupth2lem2  30238  eucrct2eupth  30264  fusgr2wsp2nb  30353  ocin  31315  chpsscon3  31522  chscllem2  31657  adjval  31909  pjimai  32195  mdsldmd1i  32350  elat2  32359  mdsymi  32430  sbceqbidf  32506  rmoxfrd  32512  rmounid  32514  disjxun0  32587  disjrdx  32604  eqrelrd2  32628  fmptcof2  32667  ofpreima  32675  funcnv5mpt  32678  ressupprn  32699  1stpreima  32716  2ndpreima  32717  fpwrelmapffslem  32743  domnpropd  33280  idompropd  33281  qsxpid  33390  grplsm0l  33431  opprlidlabs  33513  ressply1mon1p  33593  algextdeglem6  33763  smatrcl  33795  locfinreflem  33839  zarcls  33873  zhmnrg  33966  qqhval2  33983  ismntop  34027  reprsuc  34630  reprdifc  34642  bnj919  34781  bnj956  34790  bnj976  34791  bnj1366  34843  bnj916  34947  satfvsucsuc  35370  satfdm  35374  dmopab3rexdif  35410  rexxfr3dALT  35644  sscoid  35914  dfrdg4  35952  altopthbg  35969  broutsideof3  36127  rmoeqbidv  36214  sbequbidv  36215  disjeq12dv  36216  ixpeq12dv  36217  cbvmodavw  36251  cbveudavw  36252  cbvrmodavw  36253  cbvreudavw  36254  cbvsbdavw  36255  cbvsbdavw2  36256  cbvabdavw  36257  cbvsbcdavw  36258  cbvsbcdavw2  36259  cbvdisjdavw  36269  cbvrmodavw2  36284  cbvreudavw2  36285  cbvdisjdavw2  36290  bj-nnfbi  36726  bj-cbvexdv  36801  bj-sbievw  36848  mobidvALT  36858  bj-restuni  37098  bj-elid6  37171  cbveud  37373  cbvreud  37374  exrecfnlem  37380  wl-ifp-ncond2  37466  wl-ifpimpr  37467  wl-3xorbi123d  37476  wl-sb8eut  37579  wl-sb8eutv  37580  wl-sb8mot  37581  wl-sb8motv  37582  wl-clabtv  37598  wl-clabt  37599  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem25  37652  ftc1anclem5  37704  istotbnd3  37778  sstotbnd  37782  heibor  37828  isass  37853  isidlc  38022  smprngopr  38059  brvvdif  38264  elecALTV  38267  eqrel2  38300  dmecd  38305  relcnveq2  38324  elrelscnveq2  38494  extssr  38510  elrefrelsrel  38521  refreleq  38522  elcnvrefrelsrel  38537  elsymrelsrel  38558  symreleq  38559  eltrrelsrel  38582  trreleq  38583  eleqvrelsrel  38595  eqvreleq  38603  redundpim3  38631  erALTVeq1  38670  elfunsALTVfunALTV  38698  eldisjsdisj  38728  eldisjeq  38742  disjsuc  38760  parteq1  38775  parteq2  38776  islshpsm  38981  lcvexchlem1  39035  opcon1b  39199  isat3  39308  glbconN  39378  glbconNOLD  39379  cdleme32fva  40439  cdlemg2cex  40593  dibelval3  41149  dib1dim  41167  doch11  41375  dochsordN  41376  mapdordlem1a  41636  mapd11  41641  mapdsord  41657  mapdcnv11N  41661  mapd0  41667  sn-iotalem  42260  ricfld  42540  fimgmcyc  42544  fsuppind  42600  mrefg2  42718  jm2.23  43008  wepwsolem  43054  dnwech  43060  islssfg2  43083  gicabl  43111  onsupmaxb  43251  onsupeqnmax  43259  orddif0suc  43281  oadif1lem  43392  oadif1  43393  fzunt  43468  fzuntd  43469  fzunt1d  43470  fzuntgd  43471  ifpbi2  43480  ifpbi3  43481  ifpbi1  43490  ifpbi12  43501  ifpbi13  43502  ontric3g  43535  pwinfig  43574  inintabd  43592  cnvcnvintabd  43613  cnvintabd  43616  intimag  43669  briunov2  43695  heeq12  43789  sbcheg  43792  uneqsn  44038  ntrneineine0lem  44096  ntrneineine1lem  44097  ntrneik2  44105  ntrneix2  44106  ntrneik13  44111  ntrneix13  44112  ralbidar  44464  rexbidar  44465  trsbc  44560  relpeq1  44965  relpeq2  44966  relpeq3  44967  relpeq4  44968  relpeq5  44969  n0abso  44993  modelaxreplem3  44997  iindif2f  45165  rnmptpr  45182  iccintsng  45536  xlimres  45836  fsetsniunop  47061  fsetsnprcnex  47067  fcoresf1ob  47085  f1cof1b  47089  f1ocof1ob  47093  dfateq12d  47138  aov0nbovbi  47207  fnotaovb  47210  ichbidv  47440  sprsymrelf  47482  prprsprreu  47506  prprreueq  47507  edgusgrclnbfin  47828  dfclnbgr6  47842  dfnbgr6  47843  isubgredg  47852  gpgnbgrvtx0  48030  gpgnbgrvtx1  48031  rngcsectALTV  48191  ringcsectALTV  48225  lindslinindsimp2lem5  48379  opndisj  48800  i0oii  48817  io1ii  48818  iscnrm3lem2  48832  thincpropd  49091  termcpropd  49135