Theorem 3bitr4g 316

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  bibi1d  345  pm5.32rd  586  orbi2d  926  orbi1d  927  ifpbi123d  1091  3orbi123d  1457  3anbi123d  1458  nanbi1  1522  nanbi2  1523  xorbi12d  1546  hadbi123d  1616  had0  1625  cadbi123d  1631  nfbiit  1872  nfbidv  1943  sbequ  2117  nfbidf  2260  drex1v  2402  drnf1v  2403  drex1  2473  drnf1  2475  sb4b  2507  drsb1  2527  eujustALT  2600  eubi  2612  eleq1ab  2743  eqeq1d  2765  eqeq1dALT  2766  eqeq2d  2774  abbi  2828  eleq1w  2846  eleq2w  2847  eleq1d  2848  eleq2d  2849  eleq2dALT  2850  eqabdv  2896  nfceqdf  2921  drnfc1  2944  drnfc2  2945  neleq12d  3067  ralbidv2  3182  rexbidv2  3183  r19.21t  3257  r19.23t  3259  rexbida  3275  rexeq  3317  cbvraldva2  3339  raleqf  3344  ralcom2  3365  rmobidva  3381  reubidva  3382  rmobida  3391  reubida  3392  rmoeq1  3399  reueq1  3400  reueqbidv  3404  rmoeq1f  3405  reueq1f  3406  dfsbcq  3747  sbceqbid  3752  sbcbid  3799  sbcbi2  3803  eqsbc2  3808  sbcrext  3827  sbcabel  3832  ralss  4010  rexss  4011  psseq1  4044  psseq2  4045  ssconb  4096  uneq1  4115  difin2  4254  rcompleq  4258  reuun2  4278  sbcnel12g  4369  sbnfc2  4394  reldisj  4408  undif4  4422  disjssun  4423  pssdifcom1  4444  pssdifcom2  4445  sbcssg  4476  eltpg  4646  raltpg  4658  rextpg  4659  r19.12sn  4680  intmin4  4936  dfiun2g  4988  iindif1  5033  iindif2  5035  iinin2  5036  disjprg  5097  disjxun  5099  breq  5103  breq1  5104  breq2  5105  treq  5215  reusv2lem5  5360  rexxfrd  5367  rexxfr2d  5369  rexxfrd2  5371  rabxfrd  5375  opthg2  5448  oteqex2  5469  oteqex  5470  poeq1  5559  soeq1  5577  freq1  5615  weeq1  5635  weeq2  5636  opthprc  5712  wesn  5737  releq  5750  sbcrel  5754  eqrel  5757  eqrelrel  5770  xpiindi  5808  dmopab2rex  5894  dfres3  5971  brres  5973  resieq  5977  dmsnopg  6201  dfco2a  6234  dfpo2  6284  ordeq  6354  limeq  6359  ordunisssuc  6455  iotaeq  6490  sniota  6513  sbcfung  6546  imadif  6606  fneq1  6613  fneq2  6614  feq1  6670  feq2  6671  feq3  6672  sbcfng  6689  sbcfg  6690  f1eq1  6756  f1eq2  6757  f1eq3  6758  foeq1  6775  foeq2  6776  foeq3  6777  f1oeq1  6795  f1oeq2  6796  f1oeq3  6797  mpteqb  6996  rexrnmptw  7077  rexrnmpt  7079  dffo3  7084  dffo3f  7088  fmptco  7112  rexima  7223  dff13  7239  f1imaeq  7250  f1imapss  7251  cbvexfo  7275  f1eqcocnv  7286  fliftcnv  7296  isoeq1  7302  isoeq2  7303  isoeq3  7304  isoeq4  7305  isoeq5  7306  isomin  7322  isowe  7334  eqfunresadj  7345  imaeqsalvOLD  7349  nfriotadw  7362  mpoeq123  7469  rexrnmpo  7537  iunpw  7755  tfinds  7841  resf1extb  7916  fiun  7925  f1iun  7926  opiota  8041  xpord3pred  8133  ottpos  8217  dmtpos  8219  onoviun  8315  smoeq  8322  smoiso2  8341  tfr2b  8368  oarec  8532  oeeui  8573  nnacan  8599  nnmcan  8605  ereq1  8687  ereq2  8688  elecg  8724  ereldm  8733  ixpiin  8907  boxriin  8923  boxcutc  8924  omxpenlem  9051  enfiALT  9157  nnsdomo  9188  isfinite2  9243  ixpfi2  9294  elfi2  9361  fipwss  9376  ttrclse  9683  ennum  9906  cardsdom2  9947  aleph11  10041  alephiso  10055  fin23lem26  10283  compssiso  10332  isf34lem4  10335  isfin5-2  10349  fin1a2lem5  10362  brdom7disj  10489  brdom6disj  10490  fpwwe2lem7  10596  fpwwe2lem11  10600  fpwwe2lem12  10601  genpass  10968  ltasr  11059  axpre-lttri  11124  infm3  12152  creur  12190  eqreznegel  12936  rpneg  13028  ltxr  13118  icoshftf1o  13479  elfzm11  13601  elfzomelpfzo  13779  nn0ennn  13993  nnesq  14241  hashbclem  14466  hashf1lem1  14469  leiso  14473  fz1isolem  14475  pr2pwpr  14493  repsdf2  14792  dfrtrclrec2  15072  rexfiuz  15376  cau4  15385  ello1mpt2  15550  o1lo1  15565  fsumcom2  15802  incexc2  15869  fprodcom2  16015  dvdsflip  16352  bitsmod  16471  bitscmp  16473  smueqlem  16525  divgcdcoprm0  16700  hashdvds  16811  prmreclem2  16954  vdwapun  17011  vdwmc2  17016  imasaddfnlem  17559  comfeq  17739  oppcsect  17812  funcres2b  17931  funcpropd  17936  fullpropd  17956  fthpropd  17957  fthres2b  17966  fthres2c  17967  fullres2c  17975  ffthres2c  17976  fucsect  18009  fucinv  18010  setcsect  18123  pospropd  18358  tosso  18450  odulatb  18467  oduclatb  18540  odudlatb  18558  isipodrs  18570  mgmhmpropd  18733  issgrpv  18756  issgrpn0  18757  mndpropd  18794  mhmpropd  18827  issubm2  18839  efmnd1bas  18928  grppropd  18994  grpinvcnv  19049  conjghm  19290  conjnmzb  19294  ghmpropd  19297  gapm  19347  symg1bas  19432  pmtrfrn  19499  cmnpropd  19832  ablpropd  19833  eqgabl  19875  gsumcom2  20016  dmdprd  20041  dprdw  20053  subgdmdprd  20077  pgpfac1lem2  20118  pgpfac1lem4  20121  rngpropd  20221  ringpropd  20339  crngpropd  20340  crngunit  20428  unitpropd  20467  isnirred  20470  nzrpropd  20571  issubrng  20598  subrngpropd  20619  resrhm2b  20653  subrgpropd  20659  rhmpropd  20660  rngcsect  20687  ringcsect  20721  isdomn3  20766  drngpropd  20820  fldpropd  20821  fiidomfld  20825  acsfn1p  20849  abvpropd  20885  lmodprop2d  20992  lsspropd  21085  lmhmpropd  21141  lbspropd  21167  lmhmlvec  21178  lvecprop2d  21237  lvecpropd  21238  df2idl2rng  21327  pzriprnglem10  21543  phlpropd  21708  assapropd  21924  psrbagconf1o  21982  mplmonmul  22090  ismhp3  22208  mat1dimbas  22533  tpspropd  22999  tgss2  23048  lmbr2  23320  ist1-2  23408  ist1-3  23410  subislly  23542  dissnlocfin  23590  iskgen3  23610  txcnmpt  23685  hausdiag  23706  hauseqlcld  23707  xkococnlem  23720  tgqtop  23773  txhmeo  23864  uffix2  23985  ufildr  23992  txflf  24067  tgphaus  24178  qustgplem  24182  qustgphaus  24184  xpsdsval  24442  blin  24482  blres  24492  xmeterval  24493  xmspropd  24534  mspropd  24535  setsms  24541  metequiv  24570  metustsym  24616  restmetu  24631  ngppropd  24698  xrtgioo  24868  metdsge  24911  icopnfcnv  25005  iccpnfcnv  25007  lmhmclm  25150  lmmbr  25321  equivcmet  25380  cmspropd  25412  iunmbl2  25620  ioombl1lem4  25624  mbfaddlem  25723  i1fmullem  25757  itg1mulc  25767  iblcnlem1  25851  iblrelem  25854  iblre  25857  iblcn  25862  limcun  25958  mvth  26055  ofmulrt  26344  resinf1o  26602  quad2  26905  1cubr  26908  dcubic  26912  wilthlem2  27134  dvdsflf1o  27252  dvdsflsumcom  27253  fsumvma  27278  vmasum  27281  logfac2  27282  logfaclbnd  27287  dchrelbas3  27303  lgsquadlem1  27445  lgsquadlem2  27446  eqcuts2  27880  mulsrid  28207  z12sge0  28577  readdscl  28593  elplng  28988  plngcplem  28993  ax5seg  29140  ushgredgedg  29431  ushgredgedgloop  29433  nbumgrvtx  29548  upgriswlk  29842  wspniunwspnon  30124  rusgrnumwwlkb0  30175  isclwwlknx  30239  clwwlknscsh  30265  clwwlknonel  30298  0trl  30325  0spth  30329  0clwlk  30333  0crct  30336  0cycl  30337  eupth2lem2  30422  eucrct2eupth  30448  fusgr2wsp2nb  30537  ocin  31500  chpsscon3  31707  chscllem2  31842  adjval  32094  pjimai  32380  mdsldmd1i  32535  elat2  32544  mdsymi  32615  sbceqbidf  32687  rmoxfrd  32693  rmounid  32695  disjxun0  32775  disjrdx  32792  eqrelrd2  32819  fmptcof2  32860  ofpreima  32868  funcnv5mpt  32870  ressupprn  32893  1stpreima  32910  2ndpreima  32911  fpwrelmapffslem  32935  cntrval2  33352  domnpropd  33462  idompropd  33463  subsdrg  33486  qsxpid  33549  grplsm0l  33590  opprlidlabs  33674  ressply1mon1p  33765  psrmonmul  33848  algextdeglem6  34020  smatrcl  34094  locfinreflem  34138  zarcls  34172  zhmnrg  34263  qqhval2  34280  ismntop  34324  reprsuc  34910  reprdifc  34922  bnj919  35064  bnj956  35073  bnj976  35074  bnj1366  35125  bnj916  35229  satfvsucsuc  35716  satfdm  35720  dmopab3rexdif  35756  rexxfr3dALT  35990  sscoid  36262  dfrdg4  36302  altopthbg  36319  broutsideof3  36477  rmoeqbidv  36574  sbequbidv  36575  disjeq12dv  36576  ixpeq12dv  36577  cbvmodavw  36611  cbveudavw  36612  cbvrmodavw  36613  cbvreudavw  36614  cbvsbdavw  36615  cbvsbdavw2  36616  cbvabdavw  36617  cbvsbcdavw  36618  cbvsbcdavw2  36619  cbvdisjdavw  36629  cbvrmodavw2  36644  cbvreudavw2  36645  cbvdisjdavw2  36650  bj-nnfbi  37223  bj-cbvexdv  37286  bj-sbievw  37333  mobidvALT  37343  bj-axreprepsep  37561  bj-restuni  37588  bj-elid6  37663  cbveud  37867  cbvreud  37868  exrecfnlem  37874  wl-ifp-ncond2  37960  wl-ifpimpr  37961  wl-3xorbi123d  37970  wl-sb8eut  38082  wl-sb8eutv  38083  wl-sb8mot  38084  wl-sb8motv  38085  wl-clabtv  38090  wl-clabt  38091  wl-eujustlem1  38092  poimirlem17  38137  poimirlem19  38139  poimirlem20  38140  poimirlem25  38145  ftc1anclem5  38197  istotbnd3  38271  sstotbnd  38275  heibor  38321  isass  38346  isidlc  38515  smprngopr  38552  brvvdif  38768  elecALTV  38771  eqrel2  38805  dmecd  38810  relcnveq2  38829  eldmxrncnvepres  38934  eldmxrncnvepres2  38935  extssr  39089  elrefrelsrel  39100  refreleq  39101  elcnvrefrelsrel  39116  elrelscnveq2  39129  elsymrelsrel  39141  symreleq  39142  eltrrelsrel  39165  trreleq  39166  eleqvrelsrel  39178  eqvreleq  39186  redundpim3  39214  erALTVeq1  39254  elfunsALTVfunALTV  39282  eldisjsdisj  39324  eldisjeq  39341  disjsuc  39359  parteq1  39377  parteq2  39378  islshpsm  39605  lcvexchlem1  39659  opcon1b  39823  isat3  39932  glbconN  40002  cdleme32fva  41062  cdlemg2cex  41216  dibelval3  41772  dib1dim  41790  doch11  41998  dochsordN  41999  mapdordlem1a  42259  mapd11  42264  mapdsord  42280  mapdcnv11N  42284  mapd0  42290  sn-iotalem  42841  ricfld  43149  fimgmcyc  43153  fsuppind  43173  mrefg2  43289  jm2.23  43574  wepwsolem  43620  dnwech  43626  islssfg2  43649  gicabl  43677  onsupmaxb  43817  onsupeqnmax  43825  orddif0suc  43846  oadif1lem  43957  oadif1  43958  fzunt  44032  fzuntd  44033  fzunt1d  44034  fzuntgd  44035  ifpbi2  44044  ifpbi3  44045  ifpbi1  44054  ifpbi12  44065  ifpbi13  44066  ontric3g  44099  pwinfig  44138  inintabd  44156  cnvcnvintabd  44177  cnvintabd  44180  intimag  44233  briunov2  44259  heeq12  44353  sbcheg  44356  uneqsn  44602  ntrneineine0lem  44660  ntrneineine1lem  44661  ntrneik2  44669  ntrneix2  44670  ntrneik13  44675  ntrneix13  44676  ralbidar  45021  rexbidar  45022  trsbc  45117  relpeq1  45521  relpeq2  45522  relpeq3  45523  relpeq4  45524  relpeq5  45525  n0abso  45553  modelaxreplem3  45557  iindif2f  45739  rnmptpr  45756  iccintsng  46100  xlimres  46396  fsetsniunop  47644  fsetsnprcnex  47650  fcoresf1ob  47668  f1cof1b  47672  f1ocof1ob  47676  dfateq12d  47721  aov0nbovbi  47790  fnotaovb  47793  ichbidv  48060  sprsymrelf  48102  prprsprreu  48126  prprreueq  48127  nprmmul1  48134  edgusgrclnbfin  48465  dfclnbgr6  48479  dfnbgr6  48480  isubgredg  48489  gpgnbgrvtx0  48697  gpgnbgrvtx1  48698  rngcsectALTV  48898  ringcsectALTV  48932  lindslinindsimp2lem5  49085  xpco2  49479  opndisj  49525  i0oii  49542  io1ii  49543  iscnrm3lem2  49557  uobffth  49840  uobeqw  49841  thincpropd  50064  termcpropd  50125