Theorem 3bitr4g 306

Description: More general version of 3bitr4i 295. 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	syl5bb 275	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
4		3bitr4g.3	. 2 ⊢ (𝜏 ↔ 𝜒)
5	3, 4	syl6bbr 281	1 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  bibi1d  335  pm5.32rd  573  orbi2d  902  orbi1d  903  ifpbi123d  1061  3orbi123d  1508  3anbi123d  1509  nanbi1  1570  nanbi1OLD  1571  nanbi2  1572  xorbi12d  1596  hadbi123d  1653  had0  1662  cadbi123d  1668  nfbiit  1895  nfbidv  1965  19.23tOLD  2196  nfbidf  2210  drex1  2407  drnf1  2409  drsb1  2453  mobiOLD  2561  mobiOLDOLD  2562  mobidOLD  2566  eujustALT  2590  eubi  2604  eubidOLD  2608  eubidvOLD  2620  mobidvOLDOLD  2621  eubidOLDOLD  2627  mobidOLDOLD  2628  eqeq1d  2780  eqeq1dALT  2781  eqeq2d  2788  eleq1w  2842  eleq2w  2843  eleq1d  2844  eleq2d  2845  eleq2dALT  2846  abbi2dv  2897  abbilem  2903  nfceqdf  2930  drnfc1  2951  drnfc1OLD  2952  drnfc2  2953  neleq12d  3079  r19.21t  3137  ralbida  3164  ralbidv2  3166  r19.23t  3203  rexbida  3232  rexbidv2  3233  ralcom2  3290  reubida  3311  reubidva  3312  rmobida  3317  raleqf  3322  rexeqf  3323  reueq1f  3324  rmoeq1f  3325  reueq1  3332  rmoeq1  3333  cbvraldva2  3371  cbvrexdva2  3372  dfsbcq  3654  sbceqbid  3659  sbcbid  3701  sbcbi2OLD  3706  eqsbc3r  3711  sbcrext  3729  sbcabel  3734  psseq1  3916  psseq2  3917  ssconb  3966  uneq1  3983  ineq1  4030  difin2  4116  reuun2  4136  sbcnel12g  4210  sbnfc2  4233  reldisj  4245  undif4  4259  disjssun  4260  pssdifcom1  4278  pssdifcom2  4279  sbcssg  4306  eltpg  4454  raltpg  4465  rextpg  4466  r19.12sn  4487  intmin4  4739  dfiun2g  4785  iindif2  4822  iinin2  4823  disjprg  4882  disjxun  4884  breq  4888  breq1  4889  breq2  4890  treq  4993  reusv2lem5  5114  rexxfrd  5121  rexxfr2d  5123  rexxfrd2  5125  rabxfrd  5129  opthg2  5179  oteqex2  5194  oteqex  5195  poeq1  5277  soeq1  5294  freq1  5325  weeq1  5343  weeq2  5344  opthprc  5413  wesn  5438  releq  5449  sbcrel  5453  eqrel  5456  eqrelrel  5468  xpiindi  5503  dfres3  5647  brres  5649  brresgOLD2  5653  resieq  5657  dmsnopg  5860  dfco2a  5889  ordeq  5983  limeq  5988  ordunisssuc  6078  iotaeq  6107  sniota  6126  sbcfung  6159  imadif  6218  fneq1  6224  fneq2  6225  feq1  6272  feq2  6273  feq3  6274  sbcfng  6288  sbcfg  6289  f1eq1  6346  f1eq2  6347  f1eq3  6348  foeq1  6362  foeq2  6363  foeq3  6364  f1oeq1  6380  f1oeq2  6381  f1oeq3  6382  mpteqb  6560  rexrnmpt  6633  dffo3  6638  fmptco  6661  dff13  6784  f1imaeq  6794  f1imapss  6795  cbvexfo  6817  f1eqcocnv  6828  fliftcnv  6833  isoeq1  6839  isoeq2  6840  isoeq3  6841  isoeq4  6842  isoeq5  6843  isomin  6859  isowe  6871  mpt2eq123  6991  rexrnmpt2  7053  iunpw  7256  tfinds  7337  fun11iun  7405  opiota  7508  ottpos  7644  dmtpos  7646  onoviun  7723  smoeq  7730  smoiso2  7749  tfr2b  7775  oarec  7926  oeeui  7966  nnacan  7992  nnmcan  7998  ereq1  8033  ereq2  8034  elecg  8067  ereldm  8072  ixpiin  8220  boxriin  8236  boxcutc  8237  omxpenlem  8349  nnsdomo  8443  enfi  8464  isfinite2  8506  ixpfi2  8552  elfi2  8608  fipwss  8623  ennum  9106  cardsdom2  9147  aleph11  9240  alephiso  9254  fin23lem26  9482  compssiso  9531  isf34lem4  9534  isfin5-2  9548  fin1a2lem5  9561  brdom7disj  9688  brdom6disj  9689  fpwwe2lem8  9794  fpwwe2lem12  9798  fpwwe2lem13  9799  genpass  10166  ltasr  10257  axpre-lttri  10322  infm3  11336  creur  11368  eqreznegel  12081  rpneg  12171  ltxr  12260  icoshftf1o  12610  elfzm11  12729  elfzomelpfzo  12891  nn0ennn  13097  nnesq  13307  hashbclem  13550  hashf1lem1  13553  leiso  13557  fz1isolem  13559  pr2pwpr  13575  repsdf2  13924  dfrtrclrec2  14204  rexfiuz  14494  cau4  14503  ello1mpt2  14661  o1lo1  14676  fsumcom2  14910  incexc2  14974  fprodcom2  15117  dvdsflip  15446  bitsmod  15564  bitscmp  15566  smueqlem  15618  divgcdcoprm0  15784  hashdvds  15884  prmreclem2  16025  vdwapun  16082  vdwmc2  16087  imasaddfnlem  16574  comfeq  16751  oppcsect  16823  funcres2b  16942  funcpropd  16945  fullpropd  16965  fthpropd  16966  fthres2b  16975  fthres2c  16976  fullres2c  16984  ffthres2c  16985  fucsect  17017  fucinv  17018  setcsect  17124  tosso  17422  pospropd  17520  odulatb  17529  oduclatb  17530  isipodrs  17547  odudlatb  17582  issgrpv  17672  issgrpn0  17673  mndpropd  17702  mhmpropd  17727  issubm2  17734  grppropd  17824  grpinvcnv  17870  conjghm  18075  conjnmzb  18079  ghmpropd  18082  gapm  18122  symg1bas  18199  pmtrfrn  18261  cmnpropd  18588  ablpropd  18589  eqgabl  18626  gsumcom2  18760  dmdprd  18784  dprdw  18796  subgdmdprd  18820  pgpfac1lem2  18861  pgpfac1lem4  18864  ringpropd  18969  crngpropd  18970  crngunit  19049  unitpropd  19084  isnirred  19087  drngpropd  19166  fldpropd  19167  subrgpropd  19206  rhmpropd  19207  abvpropd  19234  lmodprop2d  19317  lsspropd  19412  lmhmpropd  19468  lbspropd  19494  lvecprop2d  19563  lvecpropd  19564  opprdomn  19698  fiidomfld  19705  assapropd  19724  psrbagconf1o  19771  mplmonmul  19861  phlpropd  20398  mat1dimbas  20683  tpspropd  21150  tgss2  21199  lmbr2  21471  ist1-2  21559  ist1-3  21561  subislly  21693  dissnlocfin  21741  iskgen3  21761  txcnmpt  21836  hausdiag  21857  hauseqlcld  21858  xkococnlem  21871  tgqtop  21924  txhmeo  22015  uffix2  22136  ufildr  22143  txflf  22218  tgphaus  22328  qustgplem  22332  qustgphaus  22334  xpsdsval  22594  blin  22634  blres  22644  xmeterval  22645  xmspropd  22686  mspropd  22687  setsms  22693  metequiv  22722  metustsym  22768  restmetu  22783  ngppropd  22849  xrtgioo  23017  metdsge  23060  icopnfcnv  23149  iccpnfcnv  23151  lmhmclm  23294  lmmbr  23464  equivcmet  23523  cmspropd  23555  iunmbl2  23761  ioombl1lem4  23765  mbfaddlem  23864  i1fmullem  23898  itg1mulc  23908  iblcnlem1  23991  iblrelem  23994  iblre  23997  iblcn  24002  limcun  24096  mvth  24192  ofmulrt  24474  resinf1o  24720  quad2  25017  1cubr  25020  dcubic  25024  wilthlem2  25247  dvdsflf1o  25365  dvdsflsumcom  25366  fsumvma  25390  vmasum  25393  logfac2  25394  logfaclbnd  25399  dchrelbas3  25415  lgsquadlem1  25557  lgsquadlem2  25558  ax5seg  26287  ushgredgedg  26575  ushgredgedgloop  26577  ushgredgedgloopOLD  26578  nbumgrvtx  26693  upgriswlk  26988  wspniunwspnon  27303  rusgrnumwwlkb0  27351  isclwwlknx  27425  clwwlknscsh  27460  clwwlknonel  27497  0trl  27525  0spth  27529  0clwlk  27533  0crct  27536  0cycl  27537  eupth2lem2  27623  eucrct2eupthOLD  27650  eucrct2eupth  27651  fusgr2wsp2nb  27742  ocin  28727  chpsscon3  28934  chscllem2  29069  adjval  29321  pjimai  29607  mdsldmd1i  29762  elat2  29771  mdsymi  29842  sbceqbidf  29893  rmoxfrd  29899  disjrdx  29967  eqrelrd2  29991  fmptcof2  30022  ofpreima  30030  funcnv5mpt  30033  1stpreima  30050  2ndpreima  30051  fpwrelmapffslem  30073  smatrcl  30460  locfinreflem  30505  zhmnrg  30609  qqhval2  30624  ismntop  30668  reprsuc  31295  reprdifc  31307  bnj919  31436  bnj956  31446  bnj976  31447  bnj1366  31499  bnj916  31602  dfpo2  32239  eqfunresadj  32252  sscoid  32609  dfrdg4  32647  altopthbg  32664  broutsideof3  32822  bj-ssbequ  33220  bj-cbvexdv  33321  bj-drex1v  33334  bj-drnf1v  33335  mobidvALT  33414  bj-ax8  33458  bj-restuni  33623  wl-sb8eut  33953  wl-sb8mot  33954  wl-clabtv  33968  wl-clabt  33969  wl-dfralf  33978  wl-dfrexf  33982  wl-dfrmof  33990  wl-dfreuf  33994  wl-dfrabf  33999  poimirlem17  34054  poimirlem19  34056  poimirlem20  34057  poimirlem25  34062  ftc1anclem5  34116  istotbnd3  34196  sstotbnd  34200  heibor  34246  isass  34271  isidlc  34440  smprngopr  34477  brvvdif  34664  elecALTV  34667  eqrel2  34701  dmecd  34706  relcnveq2  34724  elrelscnveq2  34873  extssr  34889  elrefrelsrel  34899  refreleq  34900  elcnvrefrelsrel  34912  elsymrelsrel  34933  symreleq  34934  eltrrelsrel  34957  trreleq  34958  eleqvrelsrel  34968  eqvreleq  34974  redpim3  35001  islshpsm  35136  lcvexchlem1  35190  opcon1b  35354  isat3  35463  glbconN  35533  cdleme32fva  36593  cdlemg2cex  36747  dibelval3  37303  dib1dim  37321  doch11  37529  dochsordN  37530  mapdordlem1a  37790  mapd11  37795  mapdsord  37811  mapdcnv11N  37815  mapd0  37821  cleljust2  38123  mrefg2  38234  jm2.23  38526  wepwsolem  38575  dnwech  38581  islssfg2  38604  gicabl  38632  acsfn1p  38732  isdomn3  38745  ifpbi2  38773  ifpbi3  38774  ifpbi23  38779  ifpbi1  38784  ifpbi12  38795  ifpbi13  38796  ifpbi123  38797  pwinfig  38827  inintabd  38846  cnvcnvintabd  38867  cnvintabd  38870  intimag  38909  briunov2  38935  heeq12  39030  sbcheg  39033  rcompleq  39278  uneqsn  39281  ntrneineine0lem  39341  ntrneineine1lem  39342  ntrneik2  39350  ntrneix2  39351  ntrneik13  39356  ntrneix13  39357  ralbidar  39607  rexbidar  39608  trsbc  39704  dffo3f  40291  iccintsng  40662  xlimres  40965  dfateq12d  42171  aov0nbovbi  42240  fnotaovb  42243  sprsymrelf  42438  prprsprreu  42462  prprreueq  42463  mgmhmpropd  42804  rngcsect  42999  rngcsectALTV  43011  ringcsect  43050  ringcsectALTV  43074  lindslinindsimp2lem5  43270