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 282	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
4		3bitr4g.3	. 2 ⊢ (𝜏 ↔ 𝜒)
5	3, 4	bitr4di 289	1 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ 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:  bibi1d  344  pm5.32rd  578  orbi2d  913  orbi1d  914  ifpbi123d  1077  ifpbi123dOLD  1078  3orbi123d  1434  3anbi123d  1435  nanbi1  1496  nanbi2  1497  xorbi12d  1522  hadbi123d  1596  had0  1606  cadbi123d  1612  nfbiit  1854  nfbidv  1926  sbequ  2087  nfbidf  2218  drex1v  2370  drnf1v  2371  drnf1vOLD  2372  drex1  2442  drnf1  2444  sb4b  2476  sb4bOLD  2477  drsb1  2500  eujustALT  2573  eubi  2585  eleq1ab  2718  eqeq1d  2741  eqeq1dALT  2742  eqeq2d  2750  abbi1  2807  eleq1w  2822  eleq2w  2823  eleq1d  2824  eleq2d  2825  eleq2dALT  2826  abbi2dv  2878  nfceqdf  2903  nfceqdfOLD  2904  drnfc1  2927  drnfc1OLD  2928  drnfc2  2929  drnfc2OLD  2930  neleq12d  3054  ralbidv2  3111  r19.21t  3140  ralbidaOLD  3161  rexbidv2  3225  r19.23t  3247  rexbida  3252  ralrexbidOLD  3257  ralcom2  3291  reubida  3322  reubidva  3323  rmobida  3327  rmobidva  3328  raleqf  3333  rexeqf  3334  reueq1f  3335  rmoeq1f  3336  raleqbidvv  3339  reueq1  3345  rmoeq1  3346  cbvraldva2  3393  cbvrexdva2  3394  dfsbcq  3719  sbceqbid  3724  sbcbid  3775  sbcbi2  3779  eqsbc2  3786  sbcrext  3807  sbcabel  3812  ss2abdv  3998  psseq1  4023  psseq2  4024  ssconb  4073  uneq1  4091  difin2  4226  rcompleq  4230  reuun2  4249  sbcnel12g  4346  sbnfc2  4371  reldisj  4386  reldisjOLD  4387  undif4  4401  disjssun  4402  pssdifcom1  4421  pssdifcom2  4422  sbcssg  4455  eltpg  4622  raltpg  4635  rextpg  4636  r19.12sn  4657  intmin4  4909  dfiun2g  4961  dfiun2gOLD  4962  iindif1  5005  iindif2  5007  iinin2  5008  disjprgw  5070  disjprg  5071  disjxun  5073  breq  5077  breq1  5078  breq2  5079  treq  5198  reusv2lem5  5326  rexxfrd  5333  rexxfr2d  5335  rexxfrd2  5337  rabxfrd  5341  opthg2  5395  oteqex2  5414  oteqex  5415  poeq1  5507  soeq1  5525  freq1  5560  weeq1  5578  weeq2  5579  opthprc  5652  wesn  5676  releq  5688  sbcrel  5692  eqrel  5696  eqrelrel  5709  xpiindi  5747  dmopab2rex  5829  dfres3  5899  brres  5901  resieq  5905  dmsnopg  6121  dfco2a  6154  dfpo2  6203  ordeq  6277  limeq  6282  ordunisssuc  6372  iotaeq  6408  sniota  6428  sbcfung  6465  imadif  6525  fneq1  6533  fneq2  6534  feq1  6590  feq2  6591  feq3  6592  sbcfng  6606  sbcfg  6607  f1eq1  6674  f1eq2  6675  f1eq3  6676  foeq1  6693  foeq2  6694  foeq3  6695  f1oeq1  6713  f1oeq2  6714  f1oeq3  6715  mpteqb  6903  rexrnmptw  6980  rexrnmpt  6982  dffo3  6987  fmptco  7010  dff13  7137  f1imaeq  7147  f1imapss  7148  cbvexfo  7171  f1eqcocnv  7182  f1eqcocnvOLD  7183  fliftcnv  7191  isoeq1  7197  isoeq2  7198  isoeq3  7199  isoeq4  7200  isoeq5  7201  isomin  7217  isowe  7229  nfriotadw  7249  mpoeq123  7356  rexrnmpo  7422  iunpw  7630  tfinds  7715  fiun  7794  f1iun  7795  opiota  7908  ottpos  8061  dmtpos  8063  onoviun  8183  smoeq  8190  smoiso2  8209  tfr2b  8236  oarec  8402  oeeui  8442  nnacan  8468  nnmcan  8474  ereq1  8514  ereq2  8515  elecg  8550  ereldm  8555  ixpiin  8721  boxriin  8737  boxcutc  8738  omxpenlem  8869  enfiALT  8983  nnsdomo  9026  isfinite2  9081  ixpfi2  9126  elfi2  9182  fipwss  9197  ttrclse  9494  ennum  9714  cardsdom2  9755  aleph11  9849  alephiso  9863  fin23lem26  10090  compssiso  10139  isf34lem4  10142  isfin5-2  10156  fin1a2lem5  10169  brdom7disj  10296  brdom6disj  10297  fpwwe2lem7  10402  fpwwe2lem11  10406  fpwwe2lem12  10407  genpass  10774  ltasr  10865  axpre-lttri  10930  infm3  11943  creur  11976  eqreznegel  12683  rpneg  12771  ltxr  12860  icoshftf1o  13215  elfzm11  13336  elfzomelpfzo  13500  nn0ennn  13708  nnesq  13951  hashbclem  14173  hashf1lem1  14177  hashf1lem1OLD  14178  leiso  14182  fz1isolem  14184  pr2pwpr  14202  repsdf2  14500  dfrtrclrec2  14778  rexfiuz  15068  cau4  15077  ello1mpt2  15240  o1lo1  15255  fsumcom2  15495  incexc2  15559  fprodcom2  15703  dvdsflip  16035  bitsmod  16152  bitscmp  16154  smueqlem  16206  divgcdcoprm0  16379  hashdvds  16485  prmreclem2  16627  vdwapun  16684  vdwmc2  16689  imasaddfnlem  17248  comfeq  17424  oppcsect  17499  funcres2b  17621  funcpropd  17625  fullpropd  17645  fthpropd  17646  fthres2b  17655  fthres2c  17656  fullres2c  17664  ffthres2c  17665  fucsect  17699  fucinv  17700  setcsect  17813  pospropd  18054  tosso  18146  odulatb  18161  oduclatb  18234  odudlatb  18252  isipodrs  18264  issgrpv  18386  issgrpn0  18387  mndpropd  18419  mhmpropd  18445  issubm2  18452  efmnd1bas  18541  grppropd  18603  grpinvcnv  18652  conjghm  18874  conjnmzb  18878  ghmpropd  18881  gapm  18921  symg1bas  19007  pmtrfrn  19075  cmnpropd  19405  ablpropd  19406  eqgabl  19445  gsumcom2  19585  dmdprd  19610  dprdw  19622  subgdmdprd  19646  pgpfac1lem2  19687  pgpfac1lem4  19690  ringpropd  19830  crngpropd  19831  crngunit  19913  unitpropd  19948  isnirred  19951  drngpropd  20027  fldpropd  20028  subrgpropd  20068  rhmpropd  20069  acsfn1p  20076  abvpropd  20111  lmodprop2d  20194  lsspropd  20288  lmhmpropd  20344  lbspropd  20370  lvecprop2d  20437  lvecpropd  20438  opprdomn  20581  fiidomfld  20589  phlpropd  20869  assapropd  21085  psrbagconf1o  21148  psrbagconf1oOLD  21149  mplmonmul  21246  ismhp3  21342  mat1dimbas  21630  tpspropd  22096  tgss2  22146  lmbr2  22419  ist1-2  22507  ist1-3  22509  subislly  22641  dissnlocfin  22689  iskgen3  22709  txcnmpt  22784  hausdiag  22805  hauseqlcld  22806  xkococnlem  22819  tgqtop  22872  txhmeo  22963  uffix2  23084  ufildr  23091  txflf  23166  tgphaus  23277  qustgplem  23281  qustgphaus  23283  xpsdsval  23543  blin  23583  blres  23593  xmeterval  23594  xmspropd  23635  mspropd  23636  setsms  23644  metequiv  23674  metustsym  23720  restmetu  23735  ngppropd  23802  xrtgioo  23978  metdsge  24021  icopnfcnv  24114  iccpnfcnv  24116  lmhmclm  24259  lmmbr  24431  equivcmet  24490  cmspropd  24522  iunmbl2  24730  ioombl1lem4  24734  mbfaddlem  24833  i1fmullem  24867  itg1mulc  24878  iblcnlem1  24961  iblrelem  24964  iblre  24967  iblcn  24972  limcun  25068  mvth  25165  ofmulrt  25451  resinf1o  25701  quad2  25998  1cubr  26001  dcubic  26005  wilthlem2  26227  dvdsflf1o  26345  dvdsflsumcom  26346  fsumvma  26370  vmasum  26373  logfac2  26374  logfaclbnd  26379  dchrelbas3  26395  lgsquadlem1  26537  lgsquadlem2  26538  ax5seg  27315  ushgredgedg  27605  ushgredgedgloop  27607  nbumgrvtx  27722  upgriswlk  28017  wspniunwspnon  28297  rusgrnumwwlkb0  28345  isclwwlknx  28409  clwwlknscsh  28435  clwwlknonel  28468  0trl  28495  0spth  28499  0clwlk  28503  0crct  28506  0cycl  28507  eupth2lem2  28592  eucrct2eupth  28618  fusgr2wsp2nb  28707  ocin  29667  chpsscon3  29874  chscllem2  30009  adjval  30261  pjimai  30547  mdsldmd1i  30702  elat2  30711  mdsymi  30782  sbceqbidf  30844  rmoxfrd  30850  rmounid  30852  disjxun0  30922  disjrdx  30939  eqrelrd2  30965  fmptcof2  31003  ofpreima  31011  funcnv5mpt  31014  ressupprn  31033  1stpreima  31048  2ndpreima  31049  fpwrelmapffslem  31076  qsxpid  31567  grplsm0l  31600  smatrcl  31755  locfinreflem  31799  zarcls  31833  zhmnrg  31926  qqhval2  31941  ismntop  31985  reprsuc  32604  reprdifc  32616  bnj919  32756  bnj956  32765  bnj976  32766  bnj1366  32818  bnj916  32922  satfvsucsuc  33336  satfdm  33340  dmopab3rexdif  33376  imaeqsalv  33700  eqfunresadj  33744  xpord3pred  33807  eqscut2  34009  sscoid  34224  dfrdg4  34262  altopthbg  34279  broutsideof3  34437  bj-nnfbi  34916  bj-cbvexdv  34991  bj-sbievw  35040  mobidvALT  35050  bj-restuni  35277  bj-elid6  35350  cbveud  35552  cbvreud  35553  exrecfnlem  35559  wl-ifp-ncond2  35645  wl-ifpimpr  35646  wl-3xorbi123d  35655  wl-sb8eut  35741  wl-sb8mot  35742  wl-clabtv  35757  wl-clabt  35758  poimirlem17  35803  poimirlem19  35805  poimirlem20  35806  poimirlem25  35811  ftc1anclem5  35863  istotbnd3  35938  sstotbnd  35942  heibor  35988  isass  36013  isidlc  36182  smprngopr  36219  brvvdif  36410  elecALTV  36413  eqrel2  36442  dmecd  36447  relcnveq2  36465  elrelscnveq2  36618  extssr  36634  elrefrelsrel  36644  refreleq  36645  elcnvrefrelsrel  36657  elsymrelsrel  36678  symreleq  36679  eltrrelsrel  36702  trreleq  36703  eleqvrelsrel  36714  eqvreleq  36722  redundpim3  36750  erALTVeq1  36788  elfunsALTVfunALTV  36815  eldisjsdisj  36845  eldisjeq  36859  islshpsm  37001  lcvexchlem1  37055  opcon1b  37219  isat3  37328  glbconN  37398  cdleme32fva  38458  cdlemg2cex  38612  dibelval3  39168  dib1dim  39186  doch11  39394  dochsordN  39395  mapdordlem1a  39655  mapd11  39660  mapdsord  39676  mapdcnv11N  39680  mapd0  39686  sn-iotalem  40196  lmhmlvec  40268  fsuppind  40286  mrefg2  40536  jm2.23  40825  wepwsolem  40874  dnwech  40880  islssfg2  40903  gicabl  40931  isdomn3  41036  fzunt  41069  fzuntd  41070  fzunt1d  41071  fzuntgd  41072  ifpbi2  41081  ifpbi3  41082  ifpbi23  41087  ifpbi1  41091  ifpbi12  41102  ifpbi13  41103  ontric3g  41136  pwinfig  41175  inintabd  41194  cnvcnvintabd  41215  cnvintabd  41218  intimag  41271  briunov2  41297  heeq12  41391  sbcheg  41394  uneqsn  41640  ntrneineine0lem  41700  ntrneineine1lem  41701  ntrneik2  41709  ntrneix2  41710  ntrneik13  41715  ntrneix13  41716  ralbidar  42070  rexbidar  42071  trsbc  42167  rnmptpr  42720  dffo3f  42724  iccintsng  43068  xlimres  43369  fsetsniunop  44554  fsetsnprcnex  44560  fcoresf1ob  44578  f1cof1b  44580  f1ocof1ob  44584  dfateq12d  44629  aov0nbovbi  44698  fnotaovb  44701  ichbidv  44916  sprsymrelf  44958  prprsprreu  44982  prprreueq  44983  mgmhmpropd  45350  rngcsect  45549  rngcsectALTV  45561  ringcsect  45600  ringcsectALTV  45624  lindslinindsimp2lem5  45814  opndisj  46207  i0oii  46224  io1ii  46225  iscnrm3lem2  46239