Theorem 3bitr4g 315

Description: More general version of 3bitr4i 304. 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 284	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
4		3bitr4g.3	. 2 ⊢ (𝜏 ↔ 𝜒)
5	3, 4	bitr4di 290	1 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  bibi1d  344  pm5.32rd  583  orbi2d  921  orbi1d  922  ifpbi123d  1084  3orbi123d  1443  3anbi123d  1444  nanbi1  1508  nanbi2  1509  xorbi12d  1532  hadbi123d  1602  had0  1611  cadbi123d  1617  nfbiit  1858  nfbidv  1929  sbequ  2094  nfbidf  2236  drex1v  2378  drnf1v  2379  drex1  2449  drnf1  2451  sb4b  2483  drsb1  2503  eujustALT  2576  eubi  2588  eleq1ab  2719  eqeq1d  2741  eqeq1dALT  2742  eqeq2d  2750  abbi  2804  eleq1w  2822  eleq2w  2823  eleq1d  2824  eleq2d  2825  eleq2dALT  2826  eqabdv  2872  nfceqdf  2897  drnfc1  2920  drnfc2  2921  neleq12d  3043  ralbidv2  3158  rexbidv2  3159  r19.21t  3233  r19.23t  3235  rexbida  3251  rexeq  3293  cbvraldva2  3315  raleqf  3320  ralcom2  3341  rmobidva  3357  reubidva  3358  rmobida  3367  reubida  3368  rmoeq1  3375  reueq1  3376  reueqbidv  3380  rmoeq1f  3381  reueq1f  3382  dfsbcq  3725  sbceqbid  3730  sbcbid  3777  sbcbi2  3781  eqsbc2  3786  sbcrext  3805  sbcabel  3810  ralss  3988  rexss  3989  psseq1  4022  psseq2  4023  ssconb  4073  uneq1  4092  difin2  4230  rcompleq  4234  reuun2  4254  sbcnel12g  4343  sbnfc2  4368  reldisj  4382  undif4  4396  disjssun  4397  pssdifcom1  4418  pssdifcom2  4419  sbcssg  4450  eltpg  4619  raltpg  4631  rextpg  4632  r19.12sn  4653  intmin4  4908  dfiun2g  4960  iindif1  5005  iindif2  5007  iinin2  5008  disjprg  5069  disjxun  5071  breq  5075  breq1  5076  breq2  5077  treq  5187  reusv2lem5  5332  rexxfrd  5339  rexxfr2d  5341  rexxfrd2  5343  rabxfrd  5347  opthg2  5420  oteqex2  5441  oteqex  5442  poeq1  5530  soeq1  5548  freq1  5586  weeq1  5606  weeq2  5607  opthprc  5683  wesn  5708  releq  5721  sbcrel  5725  eqrel  5728  eqrelrel  5741  xpiindi  5778  dmopab2rex  5860  dfres3  5937  brres  5939  resieq  5943  dmsnopg  6165  dfco2a  6198  dfpo2  6248  ordeq  6318  limeq  6323  ordunisssuc  6419  iotaeq  6454  sniota  6477  sbcfung  6510  imadif  6570  fneq1  6577  fneq2  6578  feq1  6634  feq2  6635  feq3  6636  sbcfng  6653  sbcfg  6654  f1eq1  6719  f1eq2  6720  f1eq3  6721  foeq1  6736  foeq2  6737  foeq3  6738  f1oeq1  6756  f1oeq2  6757  f1oeq3  6758  mpteqb  6956  rexrnmptw  7037  rexrnmpt  7039  dffo3  7044  dffo3f  7048  fmptco  7072  rexima  7183  dff13  7199  f1imaeq  7210  f1imapss  7211  cbvexfo  7235  f1eqcocnv  7246  fliftcnv  7256  isoeq1  7262  isoeq2  7263  isoeq3  7264  isoeq4  7265  isoeq5  7266  isomin  7282  isowe  7294  eqfunresadj  7305  imaeqsalvOLD  7309  nfriotadw  7322  mpoeq123  7429  rexrnmpo  7497  iunpw  7715  tfinds  7801  resf1extb  7875  fiun  7886  f1iun  7887  opiota  8002  xpord3pred  8093  ottpos  8177  dmtpos  8179  onoviun  8274  smoeq  8281  smoiso2  8300  tfr2b  8326  oarec  8488  oeeui  8529  nnacan  8555  nnmcan  8561  ereq1  8642  ereq2  8643  elecg  8679  ereldm  8688  ixpiin  8863  boxriin  8879  boxcutc  8880  omxpenlem  9007  enfiALT  9113  nnsdomo  9144  isfinite2  9199  ixpfi2  9251  elfi2  9318  fipwss  9333  ttrclse  9640  ennum  9863  cardsdom2  9904  aleph11  9998  alephiso  10012  fin23lem26  10239  compssiso  10288  isf34lem4  10291  isfin5-2  10305  fin1a2lem5  10318  brdom7disj  10445  brdom6disj  10446  fpwwe2lem7  10552  fpwwe2lem11  10556  fpwwe2lem12  10557  genpass  10924  ltasr  11015  axpre-lttri  11080  infm3  12107  creur  12145  eqreznegel  12876  rpneg  12968  ltxr  13058  icoshftf1o  13419  elfzm11  13541  elfzomelpfzo  13719  nn0ennn  13933  nnesq  14181  hashbclem  14406  hashf1lem1  14409  leiso  14413  fz1isolem  14415  pr2pwpr  14433  repsdf2  14732  dfrtrclrec2  15012  rexfiuz  15302  cau4  15311  ello1mpt2  15476  o1lo1  15491  fsumcom2  15728  incexc2  15795  fprodcom2  15941  dvdsflip  16278  bitsmod  16397  bitscmp  16399  smueqlem  16451  divgcdcoprm0  16626  hashdvds  16737  prmreclem2  16880  vdwapun  16937  vdwmc2  16942  imasaddfnlem  17484  comfeq  17664  oppcsect  17737  funcres2b  17856  funcpropd  17861  fullpropd  17881  fthpropd  17882  fthres2b  17891  fthres2c  17892  fullres2c  17900  ffthres2c  17901  fucsect  17934  fucinv  17935  setcsect  18048  pospropd  18283  tosso  18375  odulatb  18392  oduclatb  18465  odudlatb  18483  isipodrs  18495  mgmhmpropd  18658  issgrpv  18681  issgrpn0  18682  mndpropd  18719  mhmpropd  18752  issubm2  18764  efmnd1bas  18853  grppropd  18919  grpinvcnv  18974  conjghm  19216  conjnmzb  19220  ghmpropd  19223  gapm  19273  symg1bas  19358  pmtrfrn  19425  cmnpropd  19758  ablpropd  19759  eqgabl  19801  gsumcom2  19942  dmdprd  19967  dprdw  19979  subgdmdprd  20003  pgpfac1lem2  20044  pgpfac1lem4  20047  rngpropd  20147  ringpropd  20261  crngpropd  20262  crngunit  20350  unitpropd  20389  isnirred  20392  nzrpropd  20493  issubrng  20520  subrngpropd  20541  resrhm2b  20575  subrgpropd  20581  rhmpropd  20582  rngcsect  20609  ringcsect  20643  isdomn3  20688  drngpropd  20742  fldpropd  20743  fiidomfld  20747  acsfn1p  20772  abvpropd  20808  lmodprop2d  20915  lsspropd  21008  lmhmpropd  21064  lbspropd  21090  lmhmlvec  21101  lvecprop2d  21160  lvecpropd  21161  df2idl2rng  21250  pzriprnglem10  21466  phlpropd  21631  assapropd  21847  psrbagconf1o  21905  mplmonmul  22013  ismhp3  22131  mat1dimbas  22456  tpspropd  22922  tgss2  22971  lmbr2  23243  ist1-2  23331  ist1-3  23333  subislly  23465  dissnlocfin  23513  iskgen3  23533  txcnmpt  23608  hausdiag  23629  hauseqlcld  23630  xkococnlem  23643  tgqtop  23696  txhmeo  23787  uffix2  23908  ufildr  23915  txflf  23990  tgphaus  24101  qustgplem  24105  qustgphaus  24107  xpsdsval  24365  blin  24405  blres  24415  xmeterval  24416  xmspropd  24457  mspropd  24458  setsms  24464  metequiv  24493  metustsym  24539  restmetu  24554  ngppropd  24621  xrtgioo  24791  metdsge  24834  icopnfcnv  24928  iccpnfcnv  24930  lmhmclm  25073  lmmbr  25244  equivcmet  25303  cmspropd  25335  iunmbl2  25543  ioombl1lem4  25547  mbfaddlem  25646  i1fmullem  25680  itg1mulc  25690  iblcnlem1  25774  iblrelem  25777  iblre  25780  iblcn  25785  limcun  25881  mvth  25978  ofmulrt  26267  resinf1o  26519  quad2  26822  1cubr  26825  dcubic  26829  wilthlem2  27051  dvdsflf1o  27169  dvdsflsumcom  27170  fsumvma  27195  vmasum  27198  logfac2  27199  logfaclbnd  27204  dchrelbas3  27220  lgsquadlem1  27362  lgsquadlem2  27363  eqcuts2  27797  mulsrid  28124  z12sge0  28494  readdscl  28510  ax5seg  29026  ushgredgedg  29317  ushgredgedgloop  29319  nbumgrvtx  29434  upgriswlk  29728  wspniunwspnon  30010  rusgrnumwwlkb0  30061  isclwwlknx  30125  clwwlknscsh  30151  clwwlknonel  30184  0trl  30211  0spth  30215  0clwlk  30219  0crct  30222  0cycl  30223  eupth2lem2  30308  eucrct2eupth  30334  fusgr2wsp2nb  30423  ocin  31386  chpsscon3  31593  chscllem2  31728  adjval  31980  pjimai  32266  mdsldmd1i  32421  elat2  32430  mdsymi  32501  sbceqbidf  32575  rmoxfrd  32581  rmounid  32583  disjxun0  32664  disjrdx  32681  eqrelrd2  32709  fmptcof2  32750  ofpreima  32758  funcnv5mpt  32760  ressupprn  32783  1stpreima  32800  2ndpreima  32801  fpwrelmapffslem  32825  cntrval2  33253  domnpropd  33359  idompropd  33360  subsdrg  33383  qsxpid  33446  grplsm0l  33487  opprlidlabs  33569  ressply1mon1p  33660  psrmonmul  33743  algextdeglem6  33915  smatrcl  33989  locfinreflem  34033  zarcls  34067  zhmnrg  34158  qqhval2  34175  ismntop  34219  reprsuc  34808  reprdifc  34820  bnj919  34959  bnj956  34968  bnj976  34969  bnj1366  35020  bnj916  35124  satfvsucsuc  35602  satfdm  35606  dmopab3rexdif  35642  rexxfr3dALT  35876  sscoid  36148  dfrdg4  36188  altopthbg  36205  broutsideof3  36363  rmoeqbidv  36450  sbequbidv  36451  disjeq12dv  36452  ixpeq12dv  36453  cbvmodavw  36487  cbveudavw  36488  cbvrmodavw  36489  cbvreudavw  36490  cbvsbdavw  36491  cbvsbdavw2  36492  cbvabdavw  36493  cbvsbcdavw  36494  cbvsbcdavw2  36495  cbvdisjdavw  36505  cbvrmodavw2  36520  cbvreudavw2  36521  cbvdisjdavw2  36526  bj-nnfbi  37099  bj-cbvexdv  37162  bj-sbievw  37209  mobidvALT  37219  bj-axreprepsep  37437  bj-restuni  37464  bj-elid6  37539  cbveud  37743  cbvreud  37744  exrecfnlem  37750  wl-ifp-ncond2  37836  wl-ifpimpr  37837  wl-3xorbi123d  37846  wl-sb8eut  37958  wl-sb8eutv  37959  wl-sb8mot  37960  wl-sb8motv  37961  wl-clabtv  37966  wl-clabt  37967  wl-eujustlem1  37968  poimirlem17  38013  poimirlem19  38015  poimirlem20  38016  poimirlem25  38021  ftc1anclem5  38073  istotbnd3  38147  sstotbnd  38151  heibor  38197  isass  38222  isidlc  38391  smprngopr  38428  brvvdif  38644  elecALTV  38647  eqrel2  38681  dmecd  38686  relcnveq2  38705  eldmxrncnvepres  38810  eldmxrncnvepres2  38811  extssr  38965  elrefrelsrel  38976  refreleq  38977  elcnvrefrelsrel  38992  elrelscnveq2  39005  elsymrelsrel  39017  symreleq  39018  eltrrelsrel  39041  trreleq  39042  eleqvrelsrel  39054  eqvreleq  39062  redundpim3  39090  erALTVeq1  39130  elfunsALTVfunALTV  39158  eldisjsdisj  39200  eldisjeq  39217  disjsuc  39235  parteq1  39253  parteq2  39254  islshpsm  39481  lcvexchlem1  39535  opcon1b  39699  isat3  39808  glbconN  39878  cdleme32fva  40938  cdlemg2cex  41092  dibelval3  41648  dib1dim  41666  doch11  41874  dochsordN  41875  mapdordlem1a  42135  mapd11  42140  mapdsord  42156  mapdcnv11N  42160  mapd0  42166  sn-iotalem  42717  ricfld  43025  fimgmcyc  43029  fsuppind  43049  mrefg2  43165  jm2.23  43450  wepwsolem  43496  dnwech  43502  islssfg2  43525  gicabl  43553  onsupmaxb  43693  onsupeqnmax  43701  orddif0suc  43722  oadif1lem  43833  oadif1  43834  fzunt  43908  fzuntd  43909  fzunt1d  43910  fzuntgd  43911  ifpbi2  43920  ifpbi3  43921  ifpbi1  43930  ifpbi12  43941  ifpbi13  43942  ontric3g  43975  pwinfig  44014  inintabd  44032  cnvcnvintabd  44053  cnvintabd  44056  intimag  44109  briunov2  44135  heeq12  44229  sbcheg  44232  uneqsn  44478  ntrneineine0lem  44536  ntrneineine1lem  44537  ntrneik2  44545  ntrneix2  44546  ntrneik13  44551  ntrneix13  44552  ralbidar  44897  rexbidar  44898  trsbc  44993  relpeq1  45397  relpeq2  45398  relpeq3  45399  relpeq4  45400  relpeq5  45401  n0abso  45429  modelaxreplem3  45433  iindif2f  45615  rnmptpr  45632  iccintsng  45976  xlimres  46272  fsetsniunop  47520  fsetsnprcnex  47526  fcoresf1ob  47544  f1cof1b  47548  f1ocof1ob  47552  dfateq12d  47597  aov0nbovbi  47666  fnotaovb  47669  ichbidv  47936  sprsymrelf  47978  prprsprreu  48002  prprreueq  48003  nprmmul1  48010  edgusgrclnbfin  48341  dfclnbgr6  48355  dfnbgr6  48356  isubgredg  48365  gpgnbgrvtx0  48573  gpgnbgrvtx1  48574  rngcsectALTV  48774  ringcsectALTV  48808  lindslinindsimp2lem5  48961  xpco2  49355  opndisj  49401  i0oii  49418  io1ii  49419  iscnrm3lem2  49433  uobffth  49716  uobeqw  49717  thincpropd  49940  termcpropd  50001