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	syl5bb 285	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
4		3bitr4g.3	. 2 ⊢ (𝜏 ↔ 𝜒)
5	3, 4	syl6bbr 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  346  pm5.32rd  580  orbi2d  912  orbi1d  913  ifpbi123d  1072  ifpbi123dOLD  1073  3orbi123d  1431  3anbi123d  1432  nanbi1  1491  nanbi2  1492  xorbi12d  1517  hadbi123d  1595  had0  1605  cadbi123d  1611  nfbiit  1851  nfbidv  1923  sbequ  2090  nfbidf  2226  drex1v  2388  drnf1v  2389  drex1  2463  drnf1  2465  sb4b  2499  sb4bOLD  2500  drsb1  2535  eujustALT  2657  eubi  2669  eleq1ab  2801  eqeq1d  2823  eqeq1dALT  2824  eqeq2d  2832  abbi1  2884  eleq1w  2895  eleq2w  2896  eleq1d  2897  eleq2d  2898  eleq2dALT  2899  abbi2dv  2950  nfceqdf  2972  drnfc1  2997  drnfc1OLD  2998  drnfc2  2999  neleq12d  3127  ralbidv2  3195  r19.21t  3214  ralbida  3230  rexbidv2  3295  r19.23t  3313  rexbida  3318  ralrexbid  3322  ralcom2  3363  reubida  3387  reubidva  3388  rmobida  3392  raleqf  3397  rexeqf  3398  reueq1f  3399  rmoeq1f  3400  reueq1  3407  rmoeq1  3408  cbvraldva2  3456  cbvrexdva2  3457  cbvrexdva2OLD  3458  dfsbcq  3774  sbceqbid  3779  sbcbid  3826  sbcbi2OLD  3832  eqsbc3r  3837  sbcrext  3856  sbcabel  3861  psseq1  4064  psseq2  4065  ssconb  4114  uneq1  4132  ineq1OLD  4182  difin2  4266  reuun2  4286  sbcnel12g  4363  sbnfc2  4388  reldisj  4402  undif4  4416  disjssun  4417  pssdifcom1  4435  pssdifcom2  4436  sbcssg  4463  eltpg  4623  raltpg  4634  rextpg  4635  r19.12sn  4656  intmin4  4905  dfiun2g  4955  dfiun2gOLD  4956  iindif1  4997  iindif2  4999  iinin2  5000  disjprgw  5061  disjprg  5062  disjxun  5064  breq  5068  breq1  5069  breq2  5070  treq  5178  reusv2lem5  5303  rexxfrd  5310  rexxfr2d  5312  rexxfrd2  5314  rabxfrd  5318  opthg2  5371  oteqex2  5389  oteqex  5390  poeq1  5477  soeq1  5494  freq1  5525  weeq1  5543  weeq2  5544  opthprc  5616  wesn  5640  releq  5651  sbcrel  5655  eqrel  5658  eqrelrel  5670  xpiindi  5706  dmopab2rex  5786  dfres3  5858  brres  5860  resieq  5864  dmsnopg  6070  dfco2a  6099  ordeq  6198  limeq  6203  ordunisssuc  6293  iotaeq  6326  sniota  6346  sbcfung  6379  imadif  6438  fneq1  6444  fneq2  6445  feq1  6495  feq2  6496  feq3  6497  sbcfng  6511  sbcfg  6512  f1eq1  6570  f1eq2  6571  f1eq3  6572  foeq1  6586  foeq2  6587  foeq3  6588  f1oeq1  6604  f1oeq2  6605  f1oeq3  6606  mpteqb  6787  rexrnmptw  6861  rexrnmpt  6863  dffo3  6868  fmptco  6891  dff13  7013  f1imaeq  7023  f1imapss  7024  cbvexfo  7046  f1eqcocnv  7057  fliftcnv  7064  isoeq1  7070  isoeq2  7071  isoeq3  7072  isoeq4  7073  isoeq5  7074  isomin  7090  isowe  7102  nfriotadw  7122  mpoeq123  7226  rexrnmpo  7290  iunpw  7493  tfinds  7574  fiun  7644  f1iun  7645  opiota  7757  ottpos  7902  dmtpos  7904  onoviun  7980  smoeq  7987  smoiso2  8006  tfr2b  8032  oarec  8188  oeeui  8228  nnacan  8254  nnmcan  8260  ereq1  8296  ereq2  8297  elecg  8332  ereldm  8337  ixpiin  8488  boxriin  8504  boxcutc  8505  omxpenlem  8618  nnsdomo  8713  enfi  8734  isfinite2  8776  ixpfi2  8822  elfi2  8878  fipwss  8893  ennum  9376  cardsdom2  9417  aleph11  9510  alephiso  9524  fin23lem26  9747  compssiso  9796  isf34lem4  9799  isfin5-2  9813  fin1a2lem5  9826  brdom7disj  9953  brdom6disj  9954  fpwwe2lem8  10059  fpwwe2lem12  10063  fpwwe2lem13  10064  genpass  10431  ltasr  10522  axpre-lttri  10587  infm3  11600  creur  11632  eqreznegel  12335  rpneg  12422  ltxr  12511  icoshftf1o  12861  elfzm11  12979  elfzomelpfzo  13142  nn0ennn  13348  nnesq  13589  hashbclem  13811  hashf1lem1  13814  leiso  13818  fz1isolem  13820  pr2pwpr  13838  repsdf2  14140  dfrtrclrec2  14416  rexfiuz  14707  cau4  14716  ello1mpt2  14879  o1lo1  14894  fsumcom2  15129  incexc2  15193  fprodcom2  15338  dvdsflip  15667  bitsmod  15785  bitscmp  15787  smueqlem  15839  divgcdcoprm0  16009  hashdvds  16112  prmreclem2  16253  vdwapun  16310  vdwmc2  16315  imasaddfnlem  16801  comfeq  16976  oppcsect  17048  funcres2b  17167  funcpropd  17170  fullpropd  17190  fthpropd  17191  fthres2b  17200  fthres2c  17201  fullres2c  17209  ffthres2c  17210  fucsect  17242  fucinv  17243  setcsect  17349  tosso  17646  pospropd  17744  odulatb  17753  oduclatb  17754  isipodrs  17771  odudlatb  17806  issgrpv  17903  issgrpn0  17904  mndpropd  17936  mhmpropd  17962  issubm2  17969  efmnd1bas  18058  grppropd  18118  grpinvcnv  18167  conjghm  18389  conjnmzb  18393  ghmpropd  18396  gapm  18436  symg1bas  18519  pmtrfrn  18586  cmnpropd  18916  ablpropd  18917  eqgabl  18955  gsumcom2  19095  dmdprd  19120  dprdw  19132  subgdmdprd  19156  pgpfac1lem2  19197  pgpfac1lem4  19200  ringpropd  19332  crngpropd  19333  crngunit  19412  unitpropd  19447  isnirred  19450  drngpropd  19529  fldpropd  19530  subrgpropd  19570  rhmpropd  19571  acsfn1p  19578  abvpropd  19613  lmodprop2d  19696  lsspropd  19789  lmhmpropd  19845  lbspropd  19871  lvecprop2d  19938  lvecpropd  19939  opprdomn  20074  fiidomfld  20081  assapropd  20101  psrbagconf1o  20154  mplmonmul  20245  phlpropd  20799  mat1dimbas  21081  tpspropd  21546  tgss2  21595  lmbr2  21867  ist1-2  21955  ist1-3  21957  subislly  22089  dissnlocfin  22137  iskgen3  22157  txcnmpt  22232  hausdiag  22253  hauseqlcld  22254  xkococnlem  22267  tgqtop  22320  txhmeo  22411  uffix2  22532  ufildr  22539  txflf  22614  tgphaus  22725  qustgplem  22729  qustgphaus  22731  xpsdsval  22991  blin  23031  blres  23041  xmeterval  23042  xmspropd  23083  mspropd  23084  setsms  23090  metequiv  23119  metustsym  23165  restmetu  23180  ngppropd  23246  xrtgioo  23414  metdsge  23457  icopnfcnv  23546  iccpnfcnv  23548  lmhmclm  23691  lmmbr  23861  equivcmet  23920  cmspropd  23952  iunmbl2  24158  ioombl1lem4  24162  mbfaddlem  24261  i1fmullem  24295  itg1mulc  24305  iblcnlem1  24388  iblrelem  24391  iblre  24394  iblcn  24399  limcun  24493  mvth  24589  ofmulrt  24871  resinf1o  25120  quad2  25417  1cubr  25420  dcubic  25424  wilthlem2  25646  dvdsflf1o  25764  dvdsflsumcom  25765  fsumvma  25789  vmasum  25792  logfac2  25793  logfaclbnd  25798  dchrelbas3  25814  lgsquadlem1  25956  lgsquadlem2  25957  ax5seg  26724  ushgredgedg  27011  ushgredgedgloop  27013  nbumgrvtx  27128  upgriswlk  27422  wspniunwspnon  27702  rusgrnumwwlkb0  27750  isclwwlknx  27814  clwwlknscsh  27841  clwwlknonel  27874  0trl  27901  0spth  27905  0clwlk  27909  0crct  27912  0cycl  27913  eupth2lem2  27998  eucrct2eupth  28024  fusgr2wsp2nb  28113  ocin  29073  chpsscon3  29280  chscllem2  29415  adjval  29667  pjimai  29953  mdsldmd1i  30108  elat2  30117  mdsymi  30188  sbceqbidf  30250  rmoxfrd  30257  rmounid  30259  disjxun0  30324  disjrdx  30341  eqrelrd2  30367  fmptcof2  30402  ofpreima  30410  funcnv5mpt  30413  1stpreima  30442  2ndpreima  30443  fpwrelmapffslem  30468  qsxpid  30927  smatrcl  31061  locfinreflem  31104  zhmnrg  31208  qqhval2  31223  ismntop  31267  reprsuc  31886  reprdifc  31898  bnj919  32038  bnj956  32048  bnj976  32049  bnj1366  32101  bnj916  32205  satfvsucsuc  32612  satfdm  32616  dmopab3rexdif  32652  dfpo2  32991  eqfunresadj  33004  sscoid  33374  dfrdg4  33412  altopthbg  33429  broutsideof3  33587  bj-nnfbi  34057  bj-cbvexdv  34122  bj-sbievw  34171  mobidvALT  34181  bj-restuni  34391  bj-elid6  34465  cbveud  34656  cbvreud  34657  exrecfnlem  34663  wl-hadbi123d  34752  wl-sb8eut  34828  wl-sb8mot  34829  wl-clabtv  34844  wl-clabt  34845  wl-dfralf  34854  wl-dfrexf  34862  wl-dfrmof  34870  wl-dfreuf  34874  wl-dfrabf  34879  poimirlem17  34924  poimirlem19  34926  poimirlem20  34927  poimirlem25  34932  ftc1anclem5  34986  istotbnd3  35064  sstotbnd  35068  heibor  35114  isass  35139  isidlc  35308  smprngopr  35345  brvvdif  35539  elecALTV  35542  eqrel2  35572  dmecd  35577  relcnveq2  35595  elrelscnveq2  35748  extssr  35764  elrefrelsrel  35774  refreleq  35775  elcnvrefrelsrel  35787  elsymrelsrel  35808  symreleq  35809  eltrrelsrel  35832  trreleq  35833  eleqvrelsrel  35844  eqvreleq  35852  redundpim3  35880  erALTVeq1  35918  elfunsALTVfunALTV  35945  eldisjsdisj  35975  eldisjeq  35989  islshpsm  36131  lcvexchlem1  36185  opcon1b  36349  isat3  36458  glbconN  36528  cdleme32fva  37588  cdlemg2cex  37742  dibelval3  38298  dib1dim  38316  doch11  38524  dochsordN  38525  mapdordlem1a  38785  mapd11  38790  mapdsord  38806  mapdcnv11N  38810  mapd0  38816  lmhmlvec  39197  mrefg2  39353  jm2.23  39642  wepwsolem  39691  dnwech  39697  islssfg2  39720  gicabl  39748  isdomn3  39853  ifpbi2  39881  ifpbi3  39882  ifpbi23  39887  ifpbi1  39892  ifpbi12  39903  ifpbi13  39904  ontric3g  39937  pwinfig  39969  inintabd  39988  cnvcnvintabd  40009  cnvintabd  40012  intimag  40050  briunov2  40076  heeq12  40171  sbcheg  40174  rcompleq  40419  uneqsn  40422  ntrneineine0lem  40482  ntrneineine1lem  40483  ntrneik2  40491  ntrneix2  40492  ntrneik13  40497  ntrneix13  40498  ralbidar  40826  rexbidar  40827  trsbc  40923  rnmptpr  41482  dffo3f  41487  iccintsng  41848  xlimres  42151  dfateq12d  43374  aov0nbovbi  43443  fnotaovb  43446  sprsymrelf  43706  prprsprreu  43730  prprreueq  43731  mgmhmpropd  44101  rngcsect  44300  rngcsectALTV  44312  ringcsect  44351  ringcsectALTV  44375  lindslinindsimp2lem5  44566