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  1438  3anbi123d  1439  nanbi1  1503  nanbi2  1504  xorbi12d  1527  hadbi123d  1597  had0  1606  cadbi123d  1612  nfbiit  1853  nfbidv  1924  sbequ  2089  nfbidf  2232  drex1v  2375  drnf1v  2376  drex1  2446  drnf1  2448  sb4b  2480  drsb1  2500  eujustALT  2573  eubi  2585  eleq1ab  2717  eqeq1d  2739  eqeq1dALT  2740  eqeq2d  2748  abbi  2802  eleq1w  2820  eleq2w  2821  eleq1d  2822  eleq2d  2823  eleq2dALT  2824  eqabdv  2870  nfceqdf  2895  drnfc1  2919  drnfc2  2920  neleq12d  3042  ralbidv2  3157  rexbidv2  3158  r19.21t  3232  r19.23t  3234  rexbida  3250  rexeq  3292  cbvraldva2  3314  raleqf  3319  ralcom2  3340  rmobidva  3356  reubidva  3357  rmobida  3366  reubida  3367  rmoeq1  3374  reueq1  3375  reueqbidv  3379  rmoeq1f  3380  reueq1f  3381  dfsbcq  3731  sbceqbid  3736  sbcbid  3784  sbcbi2  3788  eqsbc2  3793  sbcrext  3812  sbcabel  3817  ralss  3997  rexss  3998  psseq1  4031  psseq2  4032  ssconb  4083  uneq1  4102  difin2  4242  rcompleq  4246  reuun2  4266  sbcnel12g  4355  sbnfc2  4380  reldisj  4394  undif4  4408  disjssun  4409  pssdifcom1  4430  pssdifcom2  4431  sbcssg  4462  eltpg  4631  raltpg  4643  rextpg  4644  r19.12sn  4665  intmin4  4920  dfiun2g  4973  iindif1  5018  iindif2  5020  iinin2  5021  disjprg  5082  disjxun  5084  breq  5088  breq1  5089  breq2  5090  treq  5200  reusv2lem5  5341  rexxfrd  5348  rexxfr2d  5350  rexxfrd2  5352  rabxfrd  5356  opthg2  5429  oteqex2  5449  oteqex  5450  poeq1  5537  soeq1  5555  freq1  5593  weeq1  5613  weeq2  5614  opthprc  5690  wesn  5715  releq  5728  sbcrel  5732  eqrel  5735  eqrelrel  5748  xpiindi  5786  dmopab2rex  5868  dfres3  5945  brres  5947  resieq  5951  dmsnopg  6173  dfco2a  6206  dfpo2  6256  ordeq  6326  limeq  6331  ordunisssuc  6427  iotaeq  6462  sniota  6485  sbcfung  6518  imadif  6578  fneq1  6585  fneq2  6586  feq1  6642  feq2  6643  feq3  6644  sbcfng  6661  sbcfg  6662  f1eq1  6727  f1eq2  6728  f1eq3  6729  foeq1  6744  foeq2  6745  foeq3  6746  f1oeq1  6764  f1oeq2  6765  f1oeq3  6766  mpteqb  6963  rexrnmptw  7043  rexrnmpt  7045  dffo3  7050  dffo3f  7054  fmptco  7078  rexima  7188  dff13  7204  f1imaeq  7215  f1imapss  7216  cbvexfo  7240  f1eqcocnv  7251  fliftcnv  7261  isoeq1  7267  isoeq2  7268  isoeq3  7269  isoeq4  7270  isoeq5  7271  isomin  7287  isowe  7299  eqfunresadj  7310  imaeqsalvOLD  7314  nfriotadw  7327  mpoeq123  7434  rexrnmpo  7502  iunpw  7720  tfinds  7806  resf1extb  7880  fiun  7891  f1iun  7892  opiota  8007  xpord3pred  8097  ottpos  8181  dmtpos  8183  onoviun  8278  smoeq  8285  smoiso2  8304  tfr2b  8330  oarec  8492  oeeui  8533  nnacan  8559  nnmcan  8565  ereq1  8646  ereq2  8647  elecg  8683  ereldm  8692  ixpiin  8867  boxriin  8883  boxcutc  8884  omxpenlem  9011  enfiALT  9117  nnsdomo  9148  isfinite2  9203  ixpfi2  9255  elfi2  9322  fipwss  9337  ttrclse  9643  ennum  9866  cardsdom2  9907  aleph11  10001  alephiso  10015  fin23lem26  10242  compssiso  10291  isf34lem4  10294  isfin5-2  10308  fin1a2lem5  10321  brdom7disj  10448  brdom6disj  10449  fpwwe2lem7  10555  fpwwe2lem11  10559  fpwwe2lem12  10560  genpass  10927  ltasr  11018  axpre-lttri  11083  infm3  12110  creur  12148  eqreznegel  12879  rpneg  12971  ltxr  13061  icoshftf1o  13422  elfzm11  13544  elfzomelpfzo  13722  nn0ennn  13936  nnesq  14184  hashbclem  14409  hashf1lem1  14412  leiso  14416  fz1isolem  14418  pr2pwpr  14436  repsdf2  14735  dfrtrclrec2  15015  rexfiuz  15305  cau4  15314  ello1mpt2  15479  o1lo1  15494  fsumcom2  15731  incexc2  15798  fprodcom2  15944  dvdsflip  16281  bitsmod  16400  bitscmp  16402  smueqlem  16454  divgcdcoprm0  16629  hashdvds  16740  prmreclem2  16883  vdwapun  16940  vdwmc2  16945  imasaddfnlem  17487  comfeq  17667  oppcsect  17740  funcres2b  17859  funcpropd  17864  fullpropd  17884  fthpropd  17885  fthres2b  17894  fthres2c  17895  fullres2c  17903  ffthres2c  17904  fucsect  17937  fucinv  17938  setcsect  18051  pospropd  18286  tosso  18378  odulatb  18395  oduclatb  18468  odudlatb  18486  isipodrs  18498  mgmhmpropd  18661  issgrpv  18684  issgrpn0  18685  mndpropd  18722  mhmpropd  18755  issubm2  18767  efmnd1bas  18856  grppropd  18922  grpinvcnv  18977  conjghm  19219  conjnmzb  19223  ghmpropd  19226  gapm  19276  symg1bas  19361  pmtrfrn  19428  cmnpropd  19761  ablpropd  19762  eqgabl  19804  gsumcom2  19945  dmdprd  19970  dprdw  19982  subgdmdprd  20006  pgpfac1lem2  20047  pgpfac1lem4  20050  rngpropd  20150  ringpropd  20264  crngpropd  20265  crngunit  20353  unitpropd  20392  isnirred  20395  nzrpropd  20492  issubrng  20519  subrngpropd  20540  resrhm2b  20574  subrgpropd  20580  rhmpropd  20581  rngcsect  20608  ringcsect  20642  isdomn3  20687  drngpropd  20741  fldpropd  20742  fiidomfld  20746  acsfn1p  20771  abvpropd  20807  lmodprop2d  20914  lsspropd  21008  lmhmpropd  21064  lbspropd  21090  lmhmlvec  21101  lvecprop2d  21160  lvecpropd  21161  df2idl2rng  21250  pzriprnglem10  21484  phlpropd  21649  assapropd  21865  psrbagconf1o  21923  mplmonmul  22028  ismhp3  22122  mat1dimbas  22451  tpspropd  22917  tgss2  22966  lmbr2  23238  ist1-2  23326  ist1-3  23328  subislly  23460  dissnlocfin  23508  iskgen3  23528  txcnmpt  23603  hausdiag  23624  hauseqlcld  23625  xkococnlem  23638  tgqtop  23691  txhmeo  23782  uffix2  23903  ufildr  23910  txflf  23985  tgphaus  24096  qustgplem  24100  qustgphaus  24102  xpsdsval  24360  blin  24400  blres  24410  xmeterval  24411  xmspropd  24452  mspropd  24453  setsms  24459  metequiv  24488  metustsym  24534  restmetu  24549  ngppropd  24616  xrtgioo  24786  metdsge  24829  icopnfcnv  24923  iccpnfcnv  24925  lmhmclm  25068  lmmbr  25239  equivcmet  25298  cmspropd  25330  iunmbl2  25538  ioombl1lem4  25542  mbfaddlem  25641  i1fmullem  25675  itg1mulc  25685  iblcnlem1  25769  iblrelem  25772  iblre  25775  iblcn  25780  limcun  25876  mvth  25973  ofmulrt  26262  resinf1o  26517  quad2  26820  1cubr  26823  dcubic  26827  wilthlem2  27050  dvdsflf1o  27168  dvdsflsumcom  27169  fsumvma  27194  vmasum  27197  logfac2  27198  logfaclbnd  27203  dchrelbas3  27219  lgsquadlem1  27361  lgsquadlem2  27362  eqcuts2  27796  mulsrid  28123  z12sge0  28493  readdscl  28509  ax5seg  29025  ushgredgedg  29316  ushgredgedgloop  29318  nbumgrvtx  29433  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  32663  disjrdx  32680  eqrelrd2  32708  fmptcof2  32749  ofpreima  32757  funcnv5mpt  32759  ressupprn  32782  1stpreima  32799  2ndpreima  32800  fpwrelmapffslem  32824  cntrval2  33251  domnpropd  33357  idompropd  33358  subsdrg  33378  qsxpid  33441  grplsm0l  33482  opprlidlabs  33564  ressply1mon1p  33647  psrmonmul  33713  algextdeglem6  33886  smatrcl  33960  locfinreflem  34004  zarcls  34038  zhmnrg  34129  qqhval2  34146  ismntop  34190  reprsuc  34779  reprdifc  34791  bnj919  34930  bnj956  34939  bnj976  34940  bnj1366  34991  bnj916  35095  satfvsucsuc  35567  satfdm  35571  dmopab3rexdif  35607  rexxfr3dALT  35841  sscoid  36113  dfrdg4  36153  altopthbg  36170  broutsideof3  36328  rmoeqbidv  36415  sbequbidv  36416  disjeq12dv  36417  ixpeq12dv  36418  cbvmodavw  36452  cbveudavw  36453  cbvrmodavw  36454  cbvreudavw  36455  cbvsbdavw  36456  cbvsbdavw2  36457  cbvabdavw  36458  cbvsbcdavw  36459  cbvsbcdavw2  36460  cbvdisjdavw  36470  cbvrmodavw2  36485  cbvreudavw2  36486  cbvdisjdavw2  36491  bj-nnfbi  37064  bj-cbvexdv  37127  bj-sbievw  37174  mobidvALT  37184  bj-axreprepsep  37402  bj-restuni  37429  bj-elid6  37504  cbveud  37706  cbvreud  37707  exrecfnlem  37713  wl-ifp-ncond2  37799  wl-ifpimpr  37800  wl-3xorbi123d  37809  wl-sb8eut  37921  wl-sb8eutv  37922  wl-sb8mot  37923  wl-sb8motv  37924  wl-clabtv  37929  wl-clabt  37930  wl-eujustlem1  37931  poimirlem17  37976  poimirlem19  37978  poimirlem20  37979  poimirlem25  37984  ftc1anclem5  38036  istotbnd3  38110  sstotbnd  38114  heibor  38160  isass  38185  isidlc  38354  smprngopr  38391  brvvdif  38607  elecALTV  38610  eqrel2  38644  dmecd  38649  relcnveq2  38668  eldmxrncnvepres  38773  eldmxrncnvepres2  38774  extssr  38928  elrefrelsrel  38939  refreleq  38940  elcnvrefrelsrel  38955  elrelscnveq2  38968  elsymrelsrel  38980  symreleq  38981  eltrrelsrel  39004  trreleq  39005  eleqvrelsrel  39017  eqvreleq  39025  redundpim3  39053  erALTVeq1  39093  elfunsALTVfunALTV  39121  eldisjsdisj  39163  eldisjeq  39180  disjsuc  39198  parteq1  39216  parteq2  39217  islshpsm  39444  lcvexchlem1  39498  opcon1b  39662  isat3  39771  glbconN  39841  cdleme32fva  40901  cdlemg2cex  41055  dibelval3  41611  dib1dim  41629  doch11  41837  dochsordN  41838  mapdordlem1a  42098  mapd11  42103  mapdsord  42119  mapdcnv11N  42123  mapd0  42129  sn-iotalem  42680  ricfld  42993  fimgmcyc  42997  fsuppind  43041  mrefg2  43157  jm2.23  43446  wepwsolem  43492  dnwech  43498  islssfg2  43521  gicabl  43549  onsupmaxb  43689  onsupeqnmax  43697  orddif0suc  43718  oadif1lem  43829  oadif1  43830  fzunt  43904  fzuntd  43905  fzunt1d  43906  fzuntgd  43907  ifpbi2  43916  ifpbi3  43917  ifpbi1  43926  ifpbi12  43937  ifpbi13  43938  ontric3g  43971  pwinfig  44010  inintabd  44028  cnvcnvintabd  44049  cnvintabd  44052  intimag  44105  briunov2  44131  heeq12  44225  sbcheg  44228  uneqsn  44474  ntrneineine0lem  44532  ntrneineine1lem  44533  ntrneik2  44541  ntrneix2  44542  ntrneik13  44547  ntrneix13  44548  ralbidar  44893  rexbidar  44894  trsbc  44989  relpeq1  45393  relpeq2  45394  relpeq3  45395  relpeq4  45396  relpeq5  45397  n0abso  45425  modelaxreplem3  45429  iindif2f  45612  rnmptpr  45629  iccintsng  45975  xlimres  46271  fsetsniunop  47513  fsetsnprcnex  47519  fcoresf1ob  47537  f1cof1b  47541  f1ocof1ob  47545  dfateq12d  47590  aov0nbovbi  47659  fnotaovb  47662  ichbidv  47929  sprsymrelf  47971  prprsprreu  47995  prprreueq  47996  nprmmul1  48003  edgusgrclnbfin  48334  dfclnbgr6  48348  dfnbgr6  48349  isubgredg  48358  gpgnbgrvtx0  48566  gpgnbgrvtx1  48567  rngcsectALTV  48767  ringcsectALTV  48801  lindslinindsimp2lem5  48954  xpco2  49348  opndisj  49394  i0oii  49411  io1ii  49412  iscnrm3lem2  49426  uobffth  49709  uobeqw  49710  thincpropd  49933  termcpropd  49994