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 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  343  pm5.32rd  577  orbi2d  912  orbi1d  913  ifpbi123d  1076  3orbi123d  1431  3anbi123d  1432  nanbi1  1494  nanbi2  1495  xorbi12d  1518  hadbi123d  1588  had0  1597  cadbi123d  1603  nfbiit  1845  nfbidv  1917  sbequ  2078  nfbidf  2209  drex1v  2360  drnf1v  2361  drnf1vOLD  2362  drex1  2432  drnf1  2434  sb4b  2466  drsb1  2486  eujustALT  2558  eubi  2570  eleq1ab  2703  eqeq1d  2726  eqeq1dALT  2727  eqeq2d  2735  abbi  2792  eleq1w  2808  eleq2w  2809  eleq1d  2810  eleq2d  2811  eleq2dALT  2812  eqabdv  2859  nfceqdf  2890  nfceqdfOLD  2891  drnfc1  2914  drnfc1OLD  2915  drnfc2  2916  drnfc2OLD  2917  neleq12d  3043  ralrexbidOLD  3099  ralbidv2  3165  rexbidv2  3166  r19.21t  3242  r19.23t  3244  ralbidaOLD  3260  rexbida  3261  rexeq  3313  raleqbidvvOLD  3322  cbvraldva2  3336  cbvrexdva2OLD  3338  raleqf  3341  rexeqfOLD  3343  ralcom2  3365  rmobidva  3383  reubidva  3384  rmobida  3394  reubida  3395  rmoeq1  3406  reueq1  3407  rmoeq1OLD  3408  reueq1OLD  3409  rmoeq1f  3412  reueq1f  3413  dfsbcq  3772  sbceqbid  3777  sbcbid  3828  sbcbi2  3832  eqsbc2  3839  sbcrext  3860  sbcabel  3865  ss2abdv  4053  psseq1  4080  psseq2  4081  ssconb  4130  uneq1  4149  difin2  4284  rcompleq  4288  reuun2  4307  sbcnel12g  4404  sbnfc2  4429  reldisj  4444  reldisjOLD  4445  undif4  4459  disjssun  4460  pssdifcom1  4482  pssdifcom2  4483  sbcssg  4516  eltpg  4682  raltpg  4695  rextpg  4696  r19.12sn  4717  intmin4  4972  dfiun2g  5024  dfiun2gOLD  5025  iindif1  5069  iindif2  5071  iinin2  5072  disjprgw  5134  disjprg  5135  disjxun  5137  breq  5141  breq1  5142  breq2  5143  treq  5264  reusv2lem5  5391  rexxfrd  5398  rexxfr2d  5400  rexxfrd2  5402  rabxfrd  5406  opthg2  5470  oteqex2  5490  oteqex  5491  poeq1  5582  soeq1  5600  freq1  5637  weeq1  5655  weeq2  5656  opthprc  5731  wesn  5755  releq  5767  sbcrel  5771  eqrel  5775  eqrelrel  5788  xpiindi  5826  dmopab2rex  5908  dfres3  5977  brres  5979  resieq  5983  dmsnopg  6203  dfco2a  6236  dfpo2  6286  ordeq  6362  limeq  6367  ordunisssuc  6461  iotaeq  6499  sniota  6525  sbcfung  6563  imadif  6623  fneq1  6631  fneq2  6632  feq1  6689  feq2  6690  feq3  6691  sbcfng  6705  sbcfg  6706  f1eq1  6773  f1eq2  6774  f1eq3  6775  foeq1  6792  foeq2  6793  foeq3  6794  f1oeq1  6812  f1oeq2  6813  f1oeq3  6814  mpteqb  7008  rexrnmptw  7087  rexrnmpt  7089  dffo3  7094  dffo3f  7098  fmptco  7120  dff13  7247  f1imaeq  7257  f1imapss  7258  cbvexfo  7281  f1eqcocnv  7292  f1eqcocnvOLD  7293  fliftcnv  7301  isoeq1  7307  isoeq2  7308  isoeq3  7309  isoeq4  7310  isoeq5  7311  isomin  7327  isowe  7339  eqfunresadj  7350  imaeqsalv  7354  nfriotadw  7366  mpoeq123  7474  rexrnmpo  7541  iunpw  7752  tfinds  7843  fiun  7923  f1iun  7924  opiota  8039  xpord3pred  8133  ottpos  8217  dmtpos  8219  onoviun  8339  smoeq  8346  smoiso2  8365  tfr2b  8392  oarec  8558  oeeui  8598  nnacan  8624  nnmcan  8630  ereq1  8707  ereq2  8708  elecg  8743  ereldm  8748  ixpiin  8915  boxriin  8931  boxcutc  8932  omxpenlem  9070  enfiALT  9188  nnsdomo  9231  isfinite2  9298  ixpfi2  9347  elfi2  9406  fipwss  9421  ttrclse  9719  ennum  9939  cardsdom2  9980  aleph11  10076  alephiso  10090  fin23lem26  10317  compssiso  10366  isf34lem4  10369  isfin5-2  10383  fin1a2lem5  10396  brdom7disj  10523  brdom6disj  10524  fpwwe2lem7  10629  fpwwe2lem11  10633  fpwwe2lem12  10634  genpass  11001  ltasr  11092  axpre-lttri  11157  infm3  12171  creur  12204  eqreznegel  12916  rpneg  13004  ltxr  13093  icoshftf1o  13449  elfzm11  13570  elfzomelpfzo  13734  nn0ennn  13942  nnesq  14188  hashbclem  14409  hashf1lem1  14413  hashf1lem1OLD  14414  leiso  14418  fz1isolem  14420  pr2pwpr  14438  repsdf2  14726  dfrtrclrec2  15003  rexfiuz  15292  cau4  15301  ello1mpt2  15464  o1lo1  15479  fsumcom2  15718  incexc2  15782  fprodcom2  15926  dvdsflip  16259  bitsmod  16376  bitscmp  16378  smueqlem  16430  divgcdcoprm0  16601  hashdvds  16709  prmreclem2  16851  vdwapun  16908  vdwmc2  16913  imasaddfnlem  17475  comfeq  17651  oppcsect  17726  funcres2b  17848  funcpropd  17854  fullpropd  17874  fthpropd  17875  fthres2b  17884  fthres2c  17885  fullres2c  17893  ffthres2c  17894  fucsect  17929  fucinv  17930  setcsect  18043  pospropd  18284  tosso  18376  odulatb  18391  oduclatb  18464  odudlatb  18482  isipodrs  18494  mgmhmpropd  18623  issgrpv  18646  issgrpn0  18647  mndpropd  18684  mhmpropd  18714  issubm2  18721  efmnd1bas  18810  grppropd  18873  grpinvcnv  18928  conjghm  19166  conjnmzb  19170  ghmpropd  19173  gapm  19214  symg1bas  19302  pmtrfrn  19370  cmnpropd  19703  ablpropd  19704  eqgabl  19746  gsumcom2  19887  dmdprd  19912  dprdw  19924  subgdmdprd  19948  pgpfac1lem2  19989  pgpfac1lem4  19992  rngpropd  20071  ringpropd  20179  crngpropd  20180  crngunit  20272  unitpropd  20311  isnirred  20314  issubrng  20439  subrngpropd  20460  resrhm2b  20496  subrgpropd  20502  rhmpropd  20503  rngcsect  20524  ringcsect  20558  drngpropd  20616  fldpropd  20617  acsfn1p  20642  abvpropd  20677  lmodprop2d  20762  lsspropd  20857  lmhmpropd  20913  lbspropd  20939  lmhmlvec  20950  lvecprop2d  21009  lvecpropd  21010  df2idl2rng  21105  opprdomn  21205  fiidomfld  21213  pzriprnglem10  21347  phlpropd  21518  assapropd  21736  psrbagconf1o  21800  psrbagconf1oOLD  21801  mplmonmul  21903  ismhp3  21996  mat1dimbas  22298  tpspropd  22764  tgss2  22814  lmbr2  23087  ist1-2  23175  ist1-3  23177  subislly  23309  dissnlocfin  23357  iskgen3  23377  txcnmpt  23452  hausdiag  23473  hauseqlcld  23474  xkococnlem  23487  tgqtop  23540  txhmeo  23631  uffix2  23752  ufildr  23759  txflf  23834  tgphaus  23945  qustgplem  23949  qustgphaus  23951  xpsdsval  24211  blin  24251  blres  24261  xmeterval  24262  xmspropd  24303  mspropd  24304  setsms  24312  metequiv  24342  metustsym  24388  restmetu  24403  ngppropd  24470  xrtgioo  24646  metdsge  24689  icopnfcnv  24791  iccpnfcnv  24793  lmhmclm  24938  lmmbr  25110  equivcmet  25169  cmspropd  25201  iunmbl2  25410  ioombl1lem4  25414  mbfaddlem  25513  i1fmullem  25547  itg1mulc  25558  iblcnlem1  25641  iblrelem  25644  iblre  25647  iblcn  25652  limcun  25748  mvth  25849  ofmulrt  26138  resinf1o  26389  quad2  26690  1cubr  26693  dcubic  26697  wilthlem2  26920  dvdsflf1o  27038  dvdsflsumcom  27039  fsumvma  27065  vmasum  27068  logfac2  27069  logfaclbnd  27074  dchrelbas3  27090  lgsquadlem1  27232  lgsquadlem2  27233  eqscut2  27658  mulsrid  27932  readdscl  28146  ax5seg  28668  ushgredgedg  28958  ushgredgedgloop  28960  nbumgrvtx  29075  upgriswlk  29370  wspniunwspnon  29649  rusgrnumwwlkb0  29697  isclwwlknx  29761  clwwlknscsh  29787  clwwlknonel  29820  0trl  29847  0spth  29851  0clwlk  29855  0crct  29858  0cycl  29859  eupth2lem2  29944  eucrct2eupth  29970  fusgr2wsp2nb  30059  ocin  31021  chpsscon3  31228  chscllem2  31363  adjval  31615  pjimai  31901  mdsldmd1i  32056  elat2  32065  mdsymi  32136  sbceqbidf  32199  rmoxfrd  32205  rmounid  32207  disjxun0  32277  disjrdx  32294  eqrelrd2  32317  fmptcof2  32354  ofpreima  32362  funcnv5mpt  32365  ressupprn  32384  1stpreima  32400  2ndpreima  32401  fpwrelmapffslem  32429  qsxpid  32947  grplsm0l  32985  opprlidlabs  33071  ressply1mon1p  33127  algextdeglem6  33261  smatrcl  33268  locfinreflem  33312  zarcls  33346  zhmnrg  33439  qqhval2  33454  ismntop  33498  reprsuc  34118  reprdifc  34130  bnj919  34269  bnj956  34278  bnj976  34279  bnj1366  34331  bnj916  34435  satfvsucsuc  34847  satfdm  34851  dmopab3rexdif  34887  sscoid  35381  dfrdg4  35419  altopthbg  35436  broutsideof3  35594  bj-nnfbi  36094  bj-cbvexdv  36169  bj-sbievw  36217  mobidvALT  36227  bj-restuni  36469  bj-elid6  36542  cbveud  36744  cbvreud  36745  exrecfnlem  36751  wl-ifp-ncond2  36837  wl-ifpimpr  36838  wl-3xorbi123d  36847  wl-sb8eut  36936  wl-sb8mot  36937  wl-clabtv  36953  wl-clabt  36954  poimirlem17  36999  poimirlem19  37001  poimirlem20  37002  poimirlem25  37007  ftc1anclem5  37059  istotbnd3  37133  sstotbnd  37137  heibor  37183  isass  37208  isidlc  37377  smprngopr  37414  brvvdif  37625  elecALTV  37628  eqrel2  37662  dmecd  37667  relcnveq2  37686  elrelscnveq2  37857  extssr  37873  elrefrelsrel  37884  refreleq  37885  elcnvrefrelsrel  37900  elsymrelsrel  37921  symreleq  37922  eltrrelsrel  37945  trreleq  37946  eleqvrelsrel  37958  eqvreleq  37966  redundpim3  37994  erALTVeq1  38033  elfunsALTVfunALTV  38061  eldisjsdisj  38091  eldisjeq  38105  disjsuc  38123  parteq1  38138  parteq2  38139  islshpsm  38344  lcvexchlem1  38398  opcon1b  38562  isat3  38671  glbconN  38741  glbconNOLD  38742  cdleme32fva  39802  cdlemg2cex  39956  dibelval3  40512  dib1dim  40530  doch11  40738  dochsordN  40739  mapdordlem1a  40999  mapd11  41004  mapdsord  41020  mapdcnv11N  41024  mapd0  41030  sn-iotalem  41535  ricfld  41599  fsuppind  41655  mrefg2  41959  jm2.23  42249  wepwsolem  42298  dnwech  42304  islssfg2  42327  gicabl  42355  isdomn3  42460  onsupmaxb  42502  onsupeqnmax  42510  orddif0suc  42532  oadif1lem  42643  oadif1  42644  fzunt  42720  fzuntd  42721  fzunt1d  42722  fzuntgd  42723  ifpbi2  42732  ifpbi3  42733  ifpbi1  42742  ifpbi12  42753  ifpbi13  42754  ontric3g  42787  pwinfig  42826  inintabd  42844  cnvcnvintabd  42865  cnvintabd  42868  intimag  42921  briunov2  42947  heeq12  43041  sbcheg  43044  uneqsn  43290  ntrneineine0lem  43348  ntrneineine1lem  43349  ntrneik2  43357  ntrneix2  43358  ntrneik13  43363  ntrneix13  43364  ralbidar  43718  rexbidar  43719  trsbc  43815  iindif2f  44367  rnmptpr  44386  iccintsng  44746  xlimres  45047  fsetsniunop  46269  fsetsnprcnex  46275  fcoresf1ob  46293  f1cof1b  46295  f1ocof1ob  46299  dfateq12d  46344  aov0nbovbi  46413  fnotaovb  46416  ichbidv  46631  sprsymrelf  46673  prprsprreu  46697  prprreueq  46698  rngcsectALTV  47163  ringcsectALTV  47197  lindslinindsimp2lem5  47356  opndisj  47747  i0oii  47764  io1ii  47765  iscnrm3lem2  47779