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  915  orbi1d  916  ifpbi123d  1078  3orbi123d  1437  3anbi123d  1438  nanbi1  1502  nanbi2  1503  xorbi12d  1526  hadbi123d  1596  had0  1605  cadbi123d  1611  nfbiit  1852  nfbidv  1923  sbequ  2088  nfbidf  2229  drex1v  2372  drnf1v  2373  drex1  2443  drnf1  2445  sb4b  2477  drsb1  2497  eujustALT  2570  eubi  2582  eleq1ab  2714  eqeq1d  2736  eqeq1dALT  2737  eqeq2d  2745  abbi  2799  eleq1w  2817  eleq2w  2818  eleq1d  2819  eleq2d  2820  eleq2dALT  2821  eqabdv  2867  nfceqdf  2892  drnfc1  2916  drnfc2  2917  neleq12d  3039  ralbidv2  3153  rexbidv2  3154  r19.21t  3228  r19.23t  3230  rexbida  3246  rexeq  3290  raleqbidvvOLD  3303  cbvraldva2  3316  raleqf  3323  rexeqfOLD  3325  ralcom2  3345  rmobidva  3361  reubidva  3362  rmobida  3371  reubida  3372  rmoeq1  3379  reueq1  3380  rmoeq1OLD  3381  reueq1OLD  3382  reueqbidv  3386  rmoeq1f  3387  reueq1f  3388  dfsbcq  3740  sbceqbid  3745  sbcbid  3793  sbcbi2  3797  eqsbc2  3802  sbcrext  3821  sbcabel  3826  ralss  4006  rexss  4007  psseq1  4040  psseq2  4041  ssconb  4092  uneq1  4111  difin2  4251  rcompleq  4255  reuun2  4275  sbcnel12g  4364  sbnfc2  4389  reldisj  4403  undif4  4417  disjssun  4418  pssdifcom1  4440  pssdifcom2  4441  sbcssg  4472  eltpg  4641  raltpg  4653  rextpg  4654  r19.12sn  4675  intmin4  4930  dfiun2g  4983  iindif1  5028  iindif2  5030  iinin2  5031  disjprg  5092  disjxun  5094  breq  5098  breq1  5099  breq2  5100  treq  5210  reusv2lem5  5345  rexxfrd  5352  rexxfr2d  5354  rexxfrd2  5356  rabxfrd  5360  opthg2  5425  oteqex2  5445  oteqex  5446  poeq1  5533  soeq1  5551  freq1  5589  weeq1  5609  weeq2  5610  opthprc  5686  wesn  5711  releq  5724  sbcrel  5728  eqrel  5731  eqrelrel  5744  xpiindi  5782  dmopab2rex  5864  dfres3  5941  brres  5943  resieq  5947  dmsnopg  6169  dfco2a  6202  dfpo2  6252  ordeq  6322  limeq  6327  ordunisssuc  6423  iotaeq  6458  sniota  6481  sbcfung  6514  imadif  6574  fneq1  6581  fneq2  6582  feq1  6638  feq2  6639  feq3  6640  sbcfng  6657  sbcfg  6658  f1eq1  6723  f1eq2  6724  f1eq3  6725  foeq1  6740  foeq2  6741  foeq3  6742  f1oeq1  6760  f1oeq2  6761  f1oeq3  6762  mpteqb  6958  rexrnmptw  7038  rexrnmpt  7040  dffo3  7045  dffo3f  7049  fmptco  7072  rexima  7182  dff13  7198  f1imaeq  7209  f1imapss  7210  cbvexfo  7234  f1eqcocnv  7245  fliftcnv  7255  isoeq1  7261  isoeq2  7262  isoeq3  7263  isoeq4  7264  isoeq5  7265  isomin  7281  isowe  7293  eqfunresadj  7304  imaeqsalvOLD  7308  nfriotadw  7321  mpoeq123  7428  rexrnmpo  7496  iunpw  7714  tfinds  7800  resf1extb  7874  fiun  7885  f1iun  7886  opiota  8001  xpord3pred  8092  ottpos  8176  dmtpos  8178  onoviun  8273  smoeq  8280  smoiso2  8299  tfr2b  8325  oarec  8487  oeeui  8528  nnacan  8554  nnmcan  8560  ereq1  8640  ereq2  8641  elecg  8677  ereldm  8686  ixpiin  8860  boxriin  8876  boxcutc  8877  omxpenlem  9004  enfiALT  9110  nnsdomo  9141  isfinite2  9196  ixpfi2  9248  elfi2  9315  fipwss  9330  ttrclse  9634  ennum  9857  cardsdom2  9898  aleph11  9992  alephiso  10006  fin23lem26  10233  compssiso  10282  isf34lem4  10285  isfin5-2  10299  fin1a2lem5  10312  brdom7disj  10439  brdom6disj  10440  fpwwe2lem7  10546  fpwwe2lem11  10550  fpwwe2lem12  10551  genpass  10918  ltasr  11009  axpre-lttri  11074  infm3  12099  creur  12137  eqreznegel  12845  rpneg  12937  ltxr  13027  icoshftf1o  13388  elfzm11  13509  elfzomelpfzo  13686  nn0ennn  13900  nnesq  14148  hashbclem  14373  hashf1lem1  14376  leiso  14380  fz1isolem  14382  pr2pwpr  14400  repsdf2  14699  dfrtrclrec2  14979  rexfiuz  15269  cau4  15278  ello1mpt2  15443  o1lo1  15458  fsumcom2  15695  incexc2  15759  fprodcom2  15905  dvdsflip  16242  bitsmod  16361  bitscmp  16363  smueqlem  16415  divgcdcoprm0  16590  hashdvds  16700  prmreclem2  16843  vdwapun  16900  vdwmc2  16905  imasaddfnlem  17447  comfeq  17627  oppcsect  17700  funcres2b  17819  funcpropd  17824  fullpropd  17844  fthpropd  17845  fthres2b  17854  fthres2c  17855  fullres2c  17863  ffthres2c  17864  fucsect  17897  fucinv  17898  setcsect  18011  pospropd  18246  tosso  18338  odulatb  18355  oduclatb  18428  odudlatb  18446  isipodrs  18458  mgmhmpropd  18621  issgrpv  18644  issgrpn0  18645  mndpropd  18682  mhmpropd  18715  issubm2  18727  efmnd1bas  18816  grppropd  18879  grpinvcnv  18934  conjghm  19176  conjnmzb  19180  ghmpropd  19183  gapm  19233  symg1bas  19318  pmtrfrn  19385  cmnpropd  19718  ablpropd  19719  eqgabl  19761  gsumcom2  19902  dmdprd  19927  dprdw  19939  subgdmdprd  19963  pgpfac1lem2  20004  pgpfac1lem4  20007  rngpropd  20107  ringpropd  20221  crngpropd  20222  crngunit  20312  unitpropd  20351  isnirred  20354  nzrpropd  20451  issubrng  20478  subrngpropd  20499  resrhm2b  20533  subrgpropd  20539  rhmpropd  20540  rngcsect  20567  ringcsect  20601  isdomn3  20646  drngpropd  20700  fldpropd  20701  fiidomfld  20705  acsfn1p  20730  abvpropd  20766  lmodprop2d  20873  lsspropd  20967  lmhmpropd  21023  lbspropd  21049  lmhmlvec  21060  lvecprop2d  21119  lvecpropd  21120  df2idl2rng  21209  pzriprnglem10  21443  phlpropd  21608  assapropd  21825  psrbagconf1o  21883  mplmonmul  21989  ismhp3  22083  mat1dimbas  22414  tpspropd  22880  tgss2  22929  lmbr2  23201  ist1-2  23289  ist1-3  23291  subislly  23423  dissnlocfin  23471  iskgen3  23491  txcnmpt  23566  hausdiag  23587  hauseqlcld  23588  xkococnlem  23601  tgqtop  23654  txhmeo  23745  uffix2  23866  ufildr  23873  txflf  23948  tgphaus  24059  qustgplem  24063  qustgphaus  24065  xpsdsval  24323  blin  24363  blres  24373  xmeterval  24374  xmspropd  24415  mspropd  24416  setsms  24422  metequiv  24451  metustsym  24497  restmetu  24512  ngppropd  24579  xrtgioo  24749  metdsge  24792  icopnfcnv  24894  iccpnfcnv  24896  lmhmclm  25041  lmmbr  25212  equivcmet  25271  cmspropd  25303  iunmbl2  25512  ioombl1lem4  25516  mbfaddlem  25615  i1fmullem  25649  itg1mulc  25659  iblcnlem1  25743  iblrelem  25746  iblre  25749  iblcn  25754  limcun  25850  mvth  25951  ofmulrt  26243  resinf1o  26499  quad2  26803  1cubr  26806  dcubic  26810  wilthlem2  27033  dvdsflf1o  27151  dvdsflsumcom  27152  fsumvma  27178  vmasum  27181  logfac2  27182  logfaclbnd  27187  dchrelbas3  27203  lgsquadlem1  27345  lgsquadlem2  27346  eqscut2  27774  mulsrid  28082  zs12ge0  28432  readdscl  28444  ax5seg  28960  ushgredgedg  29251  ushgredgedgloop  29253  nbumgrvtx  29368  upgriswlk  29663  wspniunwspnon  29945  rusgrnumwwlkb0  29996  isclwwlknx  30060  clwwlknscsh  30086  clwwlknonel  30119  0trl  30146  0spth  30150  0clwlk  30154  0crct  30157  0cycl  30158  eupth2lem2  30243  eucrct2eupth  30269  fusgr2wsp2nb  30358  ocin  31320  chpsscon3  31527  chscllem2  31662  adjval  31914  pjimai  32200  mdsldmd1i  32355  elat2  32364  mdsymi  32435  sbceqbidf  32510  rmoxfrd  32516  rmounid  32518  disjxun0  32598  disjrdx  32615  eqrelrd2  32643  fmptcof2  32684  ofpreima  32692  funcnv5mpt  32695  ressupprn  32718  1stpreima  32735  2ndpreima  32736  fpwrelmapffslem  32760  cntrval2  33202  domnpropd  33308  idompropd  33309  subsdrg  33329  qsxpid  33392  grplsm0l  33433  opprlidlabs  33515  ressply1mon1p  33598  algextdeglem6  33828  smatrcl  33902  locfinreflem  33946  zarcls  33980  zhmnrg  34071  qqhval2  34088  ismntop  34132  reprsuc  34721  reprdifc  34733  bnj919  34872  bnj956  34881  bnj976  34882  bnj1366  34934  bnj916  35038  satfvsucsuc  35508  satfdm  35512  dmopab3rexdif  35548  rexxfr3dALT  35782  sscoid  36054  dfrdg4  36094  altopthbg  36111  broutsideof3  36269  rmoeqbidv  36356  sbequbidv  36357  disjeq12dv  36358  ixpeq12dv  36359  cbvmodavw  36393  cbveudavw  36394  cbvrmodavw  36395  cbvreudavw  36396  cbvsbdavw  36397  cbvsbdavw2  36398  cbvabdavw  36399  cbvsbcdavw  36400  cbvsbcdavw2  36401  cbvdisjdavw  36411  cbvrmodavw2  36426  cbvreudavw2  36427  cbvdisjdavw2  36432  bj-nnfbi  36869  bj-cbvexdv  36944  bj-sbievw  36991  mobidvALT  37001  bj-restuni  37241  bj-elid6  37314  cbveud  37516  cbvreud  37517  exrecfnlem  37523  wl-ifp-ncond2  37609  wl-ifpimpr  37610  wl-3xorbi123d  37619  wl-sb8eut  37722  wl-sb8eutv  37723  wl-sb8mot  37724  wl-sb8motv  37725  wl-clabtv  37730  wl-clabt  37731  wl-eujustlem1  37732  poimirlem17  37777  poimirlem19  37779  poimirlem20  37780  poimirlem25  37785  ftc1anclem5  37837  istotbnd3  37911  sstotbnd  37915  heibor  37961  isass  37986  isidlc  38155  smprngopr  38192  brvvdif  38400  elecALTV  38403  eqrel2  38437  dmecd  38442  relcnveq2  38461  eldmxrncnvepres  38558  eldmxrncnvepres2  38559  extssr  38701  elrefrelsrel  38712  refreleq  38713  elcnvrefrelsrel  38728  elrelscnveq2  38741  elsymrelsrel  38753  symreleq  38754  eltrrelsrel  38777  trreleq  38778  eleqvrelsrel  38790  eqvreleq  38798  redundpim3  38826  erALTVeq1  38867  elfunsALTVfunALTV  38895  eldisjsdisj  38925  eldisjeq  38939  disjsuc  38957  parteq1  38972  parteq2  38973  islshpsm  39179  lcvexchlem1  39233  opcon1b  39397  isat3  39506  glbconN  39576  cdleme32fva  40636  cdlemg2cex  40790  dibelval3  41346  dib1dim  41364  doch11  41572  dochsordN  41573  mapdordlem1a  41833  mapd11  41838  mapdsord  41854  mapdcnv11N  41858  mapd0  41864  sn-iotalem  42419  ricfld  42727  fimgmcyc  42731  fsuppind  42775  mrefg2  42891  jm2.23  43180  wepwsolem  43226  dnwech  43232  islssfg2  43255  gicabl  43283  onsupmaxb  43423  onsupeqnmax  43431  orddif0suc  43452  oadif1lem  43563  oadif1  43564  fzunt  43638  fzuntd  43639  fzunt1d  43640  fzuntgd  43641  ifpbi2  43650  ifpbi3  43651  ifpbi1  43660  ifpbi12  43671  ifpbi13  43672  ontric3g  43705  pwinfig  43744  inintabd  43762  cnvcnvintabd  43783  cnvintabd  43786  intimag  43839  briunov2  43865  heeq12  43959  sbcheg  43962  uneqsn  44208  ntrneineine0lem  44266  ntrneineine1lem  44267  ntrneik2  44275  ntrneix2  44276  ntrneik13  44281  ntrneix13  44282  ralbidar  44627  rexbidar  44628  trsbc  44723  relpeq1  45127  relpeq2  45128  relpeq3  45129  relpeq4  45130  relpeq5  45131  n0abso  45159  modelaxreplem3  45163  iindif2f  45346  rnmptpr  45363  iccintsng  45711  xlimres  46007  fsetsniunop  47237  fsetsnprcnex  47243  fcoresf1ob  47261  f1cof1b  47265  f1ocof1ob  47269  dfateq12d  47314  aov0nbovbi  47383  fnotaovb  47386  ichbidv  47641  sprsymrelf  47683  prprsprreu  47707  prprreueq  47708  edgusgrclnbfin  48030  dfclnbgr6  48044  dfnbgr6  48045  isubgredg  48054  gpgnbgrvtx0  48262  gpgnbgrvtx1  48263  rngcsectALTV  48463  ringcsectALTV  48497  lindslinindsimp2lem5  48650  xpco2  49044  opndisj  49090  i0oii  49107  io1ii  49108  iscnrm3lem2  49122  uobffth  49405  uobeqw  49406  thincpropd  49629  termcpropd  49690