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  915  orbi1d  916  ifpbi123d  1078  3orbi123d  1434  3anbi123d  1435  nanbi1  1497  nanbi2  1498  xorbi12d  1521  hadbi123d  1591  had0  1600  cadbi123d  1606  nfbiit  1847  nfbidv  1919  sbequ  2080  nfbidf  2221  drex1v  2371  drnf1v  2372  drnf1vOLD  2373  drex1  2443  drnf1  2445  sb4b  2477  drsb1  2497  eujustALT  2569  eubi  2581  eleq1ab  2713  eqeq1d  2736  eqeq1dALT  2737  eqeq2d  2745  abbi  2804  eleq1w  2821  eleq2w  2822  eleq1d  2823  eleq2d  2824  eleq2dALT  2825  eqabdv  2872  nfceqdf  2898  drnfc1  2922  drnfc2  2923  neleq12d  3048  ralrexbidOLD  3104  ralbidv2  3171  rexbidv2  3172  r19.21t  3250  r19.23t  3252  ralbidaOLD  3268  rexbida  3269  rexeq  3319  raleqbidvvOLD  3332  cbvraldva2  3345  cbvrexdva2OLD  3347  raleqf  3350  rexeqfOLD  3352  ralcom2  3374  rmobidva  3392  reubidva  3393  rmobida  3403  reubida  3404  rmoeq1  3413  reueq1  3414  rmoeq1OLD  3415  reueq1OLD  3416  rmoeq1f  3420  reueq1f  3421  dfsbcq  3792  sbceqbid  3797  sbcbid  3849  sbcbi2  3853  eqsbc2  3859  sbcrext  3881  sbcabel  3886  psseq1  4099  psseq2  4100  ssconb  4151  uneq1  4170  difin2  4306  rcompleq  4310  reuun2  4330  sbcnel12g  4419  sbnfc2  4444  reldisj  4458  undif4  4472  disjssun  4473  pssdifcom1  4495  pssdifcom2  4496  sbcssg  4525  eltpg  4690  raltpg  4702  rextpg  4703  r19.12sn  4724  intmin4  4981  dfiun2g  5034  dfiun2gOLD  5035  iindif1  5079  iindif2  5081  iinin2  5082  disjprg  5143  disjxun  5145  breq  5149  breq1  5150  breq2  5151  treq  5272  reusv2lem5  5407  rexxfrd  5414  rexxfr2d  5416  rexxfrd2  5418  rabxfrd  5422  opthg2  5489  oteqex2  5508  oteqex  5509  poeq1  5599  soeq1  5617  freq1  5655  weeq1  5675  weeq2  5676  opthprc  5752  wesn  5776  releq  5788  sbcrel  5792  eqrel  5796  eqrelrel  5809  xpiindi  5848  dmopab2rex  5930  dfres3  6004  brres  6006  resieq  6010  dmsnopg  6234  dfco2a  6267  dfpo2  6317  ordeq  6392  limeq  6397  ordunisssuc  6491  iotaeq  6527  sniota  6553  sbcfung  6591  imadif  6651  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  7034  rexrnmptw  7114  rexrnmpt  7116  dffo3  7121  dffo3f  7125  fmptco  7148  rexima  7257  dff13  7274  f1imaeq  7284  f1imapss  7285  cbvexfo  7309  f1eqcocnv  7320  fliftcnv  7330  isoeq1  7336  isoeq2  7337  isoeq3  7338  isoeq4  7339  isoeq5  7340  isomin  7356  isowe  7368  eqfunresadj  7379  imaeqsalvOLD  7383  nfriotadw  7395  mpoeq123  7504  rexrnmpo  7572  iunpw  7789  tfinds  7880  fiun  7965  f1iun  7966  opiota  8082  xpord3pred  8175  ottpos  8259  dmtpos  8261  onoviun  8381  smoeq  8388  smoiso2  8407  tfr2b  8434  oarec  8598  oeeui  8638  nnacan  8664  nnmcan  8670  ereq1  8750  ereq2  8751  elecg  8787  ereldm  8793  ixpiin  8962  boxriin  8978  boxcutc  8979  omxpenlem  9111  enfiALT  9225  nnsdomo  9267  isfinite2  9331  ixpfi2  9387  elfi2  9451  fipwss  9466  ttrclse  9764  ennum  9984  cardsdom2  10025  aleph11  10121  alephiso  10135  fin23lem26  10362  compssiso  10411  isf34lem4  10414  isfin5-2  10428  fin1a2lem5  10441  brdom7disj  10568  brdom6disj  10569  fpwwe2lem7  10674  fpwwe2lem11  10678  fpwwe2lem12  10679  genpass  11046  ltasr  11137  axpre-lttri  11202  infm3  12224  creur  12257  eqreznegel  12973  rpneg  13064  ltxr  13154  icoshftf1o  13510  elfzm11  13631  elfzomelpfzo  13806  nn0ennn  14016  nnesq  14262  hashbclem  14487  hashf1lem1  14490  leiso  14494  fz1isolem  14496  pr2pwpr  14514  repsdf2  14812  dfrtrclrec2  15093  rexfiuz  15382  cau4  15391  ello1mpt2  15554  o1lo1  15569  fsumcom2  15806  incexc2  15870  fprodcom2  16016  dvdsflip  16350  bitsmod  16469  bitscmp  16471  smueqlem  16523  divgcdcoprm0  16698  hashdvds  16808  prmreclem2  16950  vdwapun  17007  vdwmc2  17012  imasaddfnlem  17574  comfeq  17750  oppcsect  17825  funcres2b  17947  funcpropd  17953  fullpropd  17973  fthpropd  17974  fthres2b  17983  fthres2c  17984  fullres2c  17992  ffthres2c  17993  fucsect  18028  fucinv  18029  setcsect  18142  pospropd  18384  tosso  18476  odulatb  18491  oduclatb  18564  odudlatb  18582  isipodrs  18594  mgmhmpropd  18723  issgrpv  18746  issgrpn0  18747  mndpropd  18784  mhmpropd  18817  issubm2  18829  efmnd1bas  18918  grppropd  18981  grpinvcnv  19036  conjghm  19279  conjnmzb  19283  ghmpropd  19286  gapm  19336  symg1bas  19422  pmtrfrn  19490  cmnpropd  19823  ablpropd  19824  eqgabl  19866  gsumcom2  20007  dmdprd  20032  dprdw  20044  subgdmdprd  20068  pgpfac1lem2  20109  pgpfac1lem4  20112  rngpropd  20191  ringpropd  20301  crngpropd  20302  crngunit  20394  unitpropd  20433  isnirred  20436  nzrpropd  20536  issubrng  20563  subrngpropd  20584  resrhm2b  20618  subrgpropd  20624  rhmpropd  20625  rngcsect  20652  ringcsect  20686  isdomn3  20731  drngpropd  20785  fldpropd  20786  fiidomfld  20791  acsfn1p  20816  abvpropd  20852  lmodprop2d  20938  lsspropd  21033  lmhmpropd  21089  lbspropd  21115  lmhmlvec  21126  lvecprop2d  21185  lvecpropd  21186  df2idl2rng  21283  pzriprnglem10  21518  phlpropd  21690  assapropd  21909  psrbagconf1o  21966  mplmonmul  22071  ismhp3  22163  mat1dimbas  22493  tpspropd  22959  tgss2  23009  lmbr2  23282  ist1-2  23370  ist1-3  23372  subislly  23504  dissnlocfin  23552  iskgen3  23572  txcnmpt  23647  hausdiag  23668  hauseqlcld  23669  xkococnlem  23682  tgqtop  23735  txhmeo  23826  uffix2  23947  ufildr  23954  txflf  24029  tgphaus  24140  qustgplem  24144  qustgphaus  24146  xpsdsval  24406  blin  24446  blres  24456  xmeterval  24457  xmspropd  24498  mspropd  24499  setsms  24507  metequiv  24537  metustsym  24583  restmetu  24598  ngppropd  24665  xrtgioo  24841  metdsge  24884  icopnfcnv  24986  iccpnfcnv  24988  lmhmclm  25133  lmmbr  25305  equivcmet  25364  cmspropd  25396  iunmbl2  25605  ioombl1lem4  25609  mbfaddlem  25708  i1fmullem  25742  itg1mulc  25753  iblcnlem1  25837  iblrelem  25840  iblre  25843  iblcn  25848  limcun  25944  mvth  26045  ofmulrt  26337  resinf1o  26592  quad2  26896  1cubr  26899  dcubic  26903  wilthlem2  27126  dvdsflf1o  27244  dvdsflsumcom  27245  fsumvma  27271  vmasum  27274  logfac2  27275  logfaclbnd  27280  dchrelbas3  27296  lgsquadlem1  27438  lgsquadlem2  27439  eqscut2  27865  mulsrid  28153  readdscl  28445  ax5seg  28967  ushgredgedg  29260  ushgredgedgloop  29262  nbumgrvtx  29377  upgriswlk  29673  wspniunwspnon  29952  rusgrnumwwlkb0  30000  isclwwlknx  30064  clwwlknscsh  30090  clwwlknonel  30123  0trl  30150  0spth  30154  0clwlk  30158  0crct  30161  0cycl  30162  eupth2lem2  30247  eucrct2eupth  30273  fusgr2wsp2nb  30362  ocin  31324  chpsscon3  31531  chscllem2  31666  adjval  31918  pjimai  32204  mdsldmd1i  32359  elat2  32368  mdsymi  32439  sbceqbidf  32514  rmoxfrd  32520  rmounid  32522  disjxun0  32593  disjrdx  32610  eqrelrd2  32635  fmptcof2  32673  ofpreima  32681  funcnv5mpt  32684  ressupprn  32704  1stpreima  32721  2ndpreima  32722  fpwrelmapffslem  32749  qsxpid  33369  grplsm0l  33410  opprlidlabs  33492  ressply1mon1p  33572  algextdeglem6  33727  smatrcl  33756  locfinreflem  33800  zarcls  33834  zhmnrg  33927  qqhval2  33944  ismntop  33988  reprsuc  34608  reprdifc  34620  bnj919  34759  bnj956  34768  bnj976  34769  bnj1366  34821  bnj916  34925  satfvsucsuc  35349  satfdm  35353  dmopab3rexdif  35389  rexxfr3dALT  35623  sscoid  35894  dfrdg4  35932  altopthbg  35949  broutsideof3  36107  rmoeqbidv  36194  reueqbidv  36195  sbequbidv  36196  disjeq12dv  36197  ixpeq12dv  36198  cbvmodavw  36232  cbveudavw  36233  cbvrmodavw  36234  cbvreudavw  36235  cbvsbdavw  36236  cbvsbdavw2  36237  cbvabdavw  36238  cbvsbcdavw  36239  cbvsbcdavw2  36240  cbvdisjdavw  36250  cbvrmodavw2  36265  cbvreudavw2  36266  cbvdisjdavw2  36271  bj-nnfbi  36707  bj-cbvexdv  36782  bj-sbievw  36829  mobidvALT  36839  bj-restuni  37079  bj-elid6  37152  cbveud  37354  cbvreud  37355  exrecfnlem  37361  wl-ifp-ncond2  37447  wl-ifpimpr  37448  wl-3xorbi123d  37457  wl-sb8eut  37558  wl-sb8eutv  37559  wl-sb8mot  37560  wl-sb8motv  37561  wl-clabtv  37577  wl-clabt  37578  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem25  37631  ftc1anclem5  37683  istotbnd3  37757  sstotbnd  37761  heibor  37807  isass  37832  isidlc  38001  smprngopr  38038  brvvdif  38244  elecALTV  38247  eqrel2  38280  dmecd  38285  relcnveq2  38304  elrelscnveq2  38474  extssr  38490  elrefrelsrel  38501  refreleq  38502  elcnvrefrelsrel  38517  elsymrelsrel  38538  symreleq  38539  eltrrelsrel  38562  trreleq  38563  eleqvrelsrel  38575  eqvreleq  38583  redundpim3  38611  erALTVeq1  38650  elfunsALTVfunALTV  38678  eldisjsdisj  38708  eldisjeq  38722  disjsuc  38740  parteq1  38755  parteq2  38756  islshpsm  38961  lcvexchlem1  39015  opcon1b  39179  isat3  39288  glbconN  39358  glbconNOLD  39359  cdleme32fva  40419  cdlemg2cex  40573  dibelval3  41129  dib1dim  41147  doch11  41355  dochsordN  41356  mapdordlem1a  41616  mapd11  41621  mapdsord  41637  mapdcnv11N  41641  mapd0  41647  sn-iotalem  42238  ricfld  42516  fimgmcyc  42520  fsuppind  42576  mrefg2  42694  jm2.23  42984  wepwsolem  43030  dnwech  43036  islssfg2  43059  gicabl  43087  onsupmaxb  43227  onsupeqnmax  43235  orddif0suc  43257  oadif1lem  43368  oadif1  43369  fzunt  43444  fzuntd  43445  fzunt1d  43446  fzuntgd  43447  ifpbi2  43456  ifpbi3  43457  ifpbi1  43466  ifpbi12  43477  ifpbi13  43478  ontric3g  43511  pwinfig  43550  inintabd  43568  cnvcnvintabd  43589  cnvintabd  43592  intimag  43645  briunov2  43671  heeq12  43765  sbcheg  43768  uneqsn  44014  ntrneineine0lem  44072  ntrneineine1lem  44073  ntrneik2  44081  ntrneix2  44082  ntrneik13  44087  ntrneix13  44088  ralbidar  44440  rexbidar  44441  trsbc  44537  modelaxreplem3  44944  iindif2f  45102  rnmptpr  45119  iccintsng  45475  xlimres  45776  fsetsniunop  46998  fsetsnprcnex  47004  fcoresf1ob  47022  f1cof1b  47026  f1ocof1ob  47030  dfateq12d  47075  aov0nbovbi  47144  fnotaovb  47147  ichbidv  47377  sprsymrelf  47419  prprsprreu  47443  prprreueq  47444  edgusgrclnbfin  47765  dfclnbgr6  47779  dfnbgr6  47780  isubgredg  47789  gpgnbgrvtx0  47964  gpgnbgrvtx1  47965  rngcsectALTV  48118  ringcsectALTV  48152  lindslinindsimp2lem5  48307  opndisj  48698  i0oii  48715  io1ii  48716  iscnrm3lem2  48730