Theorem 3bitr4g 317

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bibi1d  346  pm5.32rd  589  orbi2d  929  orbi1d  930  ifpbi123d  1095  3orbi123d  1463  3anbi123d  1464  nanbi1  1530  nanbi2  1531  xorbi12d  1554  hadbi123d  1624  had0OLD  1635  cadbi123d  1642  nfbiit  1883  nfbidv  1956  sbequ  2121  nfbidf  2263  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  2847  eleq2w  2848  eleq1d  2849  eleq2d  2850  eleq2dALT  2851  eqabdv  2897  nfceqdf  2922  drnfc1  2945  drnfc2  2946  neleq12d  3070  ralbidv2  3185  rexbidv2  3186  r19.21t  3260  r19.23t  3262  rexbida  3278  rexeq  3319  cbvraldva2  3340  raleqf  3345  ralcom2  3366  rmobidva  3382  reubidva  3383  rmobida  3392  reubida  3393  rmoeq1  3400  reueq1  3401  reueqbidv  3405  rmoeq1f  3406  reueq1f  3407  dfsbcq  3744  sbceqbid  3749  sbcbid  3796  sbcbi2  3800  eqsbc2  3805  sbcrext  3824  sbcabel  3829  ralss  3986  rexss  3987  psseq1  4020  psseq2  4021  ssconb  4081  uneq1  4163  difin2  4249  rcompleq  4253  reuun2  4273  sbcnel12g  4375  sbnfc2  4400  reldisj  4409  undif4  4423  disjssun  4424  pssdifcom1  4448  pssdifcom2  4449  sbcssg  4480  eltpg  4647  raltpg  4659  rextpg  4660  r19.12sn  4681  intmin4  4940  dfiun2g  4991  iindif1  5038  iindif2  5040  iinin2  5041  disjprg  5102  disjxun  5104  breq  5108  breq1  5109  breq2  5110  treq  5222  reusv2lem5  5368  rexxfrd  5375  rexxfr2d  5377  rexxfrd2  5379  rabxfrd  5383  opthg2  5452  oteqex2  5475  oteqex  5476  poeq1  5566  soeq1  5584  freq1  5622  weeq1  5642  weeq2  5643  opthprc  5719  wesn  5745  releq  5758  sbcrel  5762  eqrel  5765  eqrelrel  5778  xpiindi  5817  dmopab2rex  5904  dfres3  5980  brres  5982  resieq  5986  cnveqb  6196  dmsnopg  6221  dfco2a  6254  dfpo2  6306  ordeq  6376  limeq  6381  ordunisssuc  6478  iotaeq  6513  sniota  6538  sbcfung  6572  sbcfungOLD  6573  imadif  6635  fneq1  6641  fneq2  6642  feq1  6698  feq2  6699  feq3  6700  sbcfng  6717  sbcfg  6718  f1eq1  6784  f1eq2  6785  f1eq3  6786  foeq1  6803  foeq2  6804  foeq3  6805  f1oeq1  6823  f1oeq2  6824  f1oeq3  6825  mpteqb  7024  rexrnmptw  7106  rexrnmpt  7108  dffo3  7113  dffo3f  7117  fmptco  7141  rexima  7254  dff13  7268  f1imaeq  7279  f1imapss  7280  cbvexfo  7308  f1eqcocnv  7319  fliftcnv  7329  isoeq1  7335  isoeq2  7336  isoeq3  7337  isoeq4  7338  isoeq5  7339  isomin  7355  isowe  7367  eqfunresadj  7380  nfriotadw  7395  mpoeq123  7502  rexrnmpo  7570  iunpw  7795  tfinds  7881  resf1extb  7956  fiun  7965  f1iun  7966  opiota  8081  xpord3pred  8182  ottpos  8267  dmtpos  8269  onoviun  8365  smoeq  8372  smoiso2  8391  tfr2b  8418  oarec  8584  oeeui  8625  nnacan  8651  nnmcan  8657  ereq1  8739  ereq2  8740  elecg  8776  ereldm  8785  ixpiin  8966  boxriin  8982  boxcutc  8983  omxpenlem  9111  enfiALT  9217  nnsdomo  9248  isfinite2  9304  ixpfi2  9353  elfi2  9419  fipwss  9434  ttrclse  9741  ennum  10041  cardsdom2  10082  aleph11  10176  alephiso  10190  fin23lem26  10416  compssiso  10465  isf34lem4  10468  isfin5-2  10482  fin1a2lem5  10495  brdom7disj  10623  brdom6disj  10624  fpwwe2lem7  10735  fpwwe2lem11  10739  fpwwe2lem12  10740  genpass  11107  ltasr  11198  axpre-lttri  11263  infm3  12289  creur  12327  eqreznegel  13074  rpneg  13167  ltxr  13257  icoshftf1o  13618  elfzm11  13742  elfzomelpfzo  13920  nn0ennn  14135  nnesq  14384  hashbclem  14610  hashf1lem1  14613  leiso  14617  fz1isolem  14619  pr2pwpr  14637  repsdf2  14943  dfrtrclrec2  15226  rexfiuz  15530  cau4  15539  ello1mpt2  15704  o1lo1  15719  fsumcom2  15955  incexc2  16022  fprodcom2  16166  dvdsflip  16502  bitsmod  16621  bitscmp  16623  smueqlem  16675  divgcdcoprm0  16855  hashdvds  16967  prmreclem2  17110  vdwapun  17167  vdwmc2  17172  imasaddfnlem  17715  comfeq  17895  oppcsect  17968  funcres2b  18087  funcpropd  18092  fullpropd  18112  fthpropd  18113  fthres2b  18122  fthres2c  18123  fullres2c  18131  ffthres2c  18132  fucsect  18165  fucinv  18166  setcsect  18279  pospropd  18514  tosso  18606  odulatb  18623  oduclatb  18696  odudlatb  18714  isipodrs  18726  mgmhmpropd  18902  issgrpv  18925  issgrpn0  18926  mndpropd  18966  mhmpropd  19002  issubm2  19014  efmnd1bas  19104  grppropd  19177  grpinvcnv  19232  qsxpid  19402  conjghm  19478  conjnmzb  19482  ghmpropd  19485  gapm  19535  symg1bas  19620  pmtrfrn  19687  cmnpropd  20020  ablpropd  20021  eqgabl  20063  gsumcom2  20204  dmdprd  20229  dprdw  20241  subgdmdprd  20265  pgpfac1lem2  20306  pgpfac1lem4  20309  rngpropd  20411  ringpropd  20534  crngpropd  20535  crngunit  20623  unitpropd  20662  isnirred  20665  nzrpropd  20786  issubrng  20814  subrngpropd  20835  resrhm2b  20869  subrgpropd  20875  rhmpropd  20876  rngcsect  20903  ringcsect  20937  isdomn3  20981  drngpropd  21042  fldpropd  21043  fiidomfld  21047  acsfn1p  21071  abvpropd  21107  lmodprop2d  21214  lsspropd  21307  lmhmpropd  21363  lbspropd  21389  lmhmlvec  21400  lvecprop2d  21459  lvecpropd  21460  df2idl2rng  21565  pzriprnglem10  21811  phlpropd  21976  assapropd  22194  psrbagconf1o  22252  mplmonmul  22360  ismhp3  22478  mat1dimbas  22802  tpspropd  23271  tgss2  23320  lmbr2  23592  ist1-2  23680  ist1-3  23682  subislly  23815  dissnlocfin  23863  iskgen3  23883  txcnmpt  23958  hausdiag  23979  hauseqlcld  23980  xkococnlem  23993  tgqtop  24046  txhmeo  24137  uffix2  24258  ufildr  24265  txflf  24340  tgphaus  24451  qustgplem  24455  qustgphaus  24457  xpsdsval  24715  blin  24755  blres  24765  xmeterval  24766  xmspropd  24807  mspropd  24808  setsms  24814  metequiv  24843  metustsym  24889  restmetu  24904  ngppropd  24971  xrtgioo  25141  metdsge  25184  icopnfcnv  25278  iccpnfcnv  25280  lmhmclm  25423  lmmbr  25594  equivcmet  25653  cmspropd  25685  iunmbl2  25893  ioombl1lem4  25897  mbfaddlem  25996  i1fmullem  26030  itg1mulc  26040  iblcnlem1  26123  iblrelem  26126  iblre  26129  iblcn  26134  limcun  26230  mvth  26327  ofmulrt  26615  resinf1o  26879  quad2  27182  1cubr  27185  dcubic  27189  wilthlem2  27411  dvdsflf1o  27529  dvdsflsumcom  27530  fsumvma  27555  vmasum  27558  logfac2  27559  logfaclbnd  27564  dchrelbas3  27580  lgsquadlem1  27722  lgsquadlem2  27723  eqcuts2  28187  mulsrid  28514  z12sge0  28884  readdscl  28900  elplng  29273  plngcplem  29278  ax5seg  29531  ushgredgedg  29825  ushgredgedgloop  29827  nbumgrvtx  29942  upgriswlk  30236  wspniunwspnon  30527  rusgrnumwwlkb0  30578  isclwwlknx  30642  clwwlknscsh  30668  clwwlknonel  30701  0trl  30728  0spth  30732  0clwlk  30736  0crct  30739  0cycl  30740  eupth2lem2  30835  eucrct2eupth  30861  fusgr2wsp2nb  30950  ocin  31913  chpsscon3  32120  chscllem2  32255  adjval  32507  pjimai  32793  mdsldmd1i  32948  elat2  32957  mdsymi  33028  sbceqbidf  33140  rmoxfrd  33146  rmounid  33148  disjxun0  33225  disjrdx  33242  eqrelrd2  33267  fmptcof2  33308  ofpreima  33316  funcnv5mpt  33318  ressupprn  33340  1stpreima  33357  2ndpreima  33358  fpwrelmapffslem  33380  cntrval2  33788  domnpropd  33897  idompropd  33898  subsdrg  33916  grplsm0l  34010  opprlidlabs  34065  ressply1mon1p  34156  psrmonmul  34238  algextdeglem6  34410  smatrcl  34484  locfinreflem  34528  zarcls  34562  zhmnrg  34653  qqhval2  34670  ismntop  34714  reprsuc  35300  reprdifc  35312  bnj919  35454  bnj956  35463  bnj976  35464  bnj1366  35515  bnj916  35619  fwfffunres  35774  satfvsucsuc  36254  satfdm  36258  dmopab3rexdif  36294  rexxfr3dALT  36528  sscoid  36805  dfrdg4  36845  altopthbg  36863  broutsideof3  37021  rmoeqbidv  37132  sbequbidv  37133  disjeq12dv  37134  ixpeq12dv  37135  cbvmodavw  37169  cbveudavw  37170  cbvrmodavw  37171  cbvreudavw  37172  cbvsbdavw  37173  cbvsbdavw2  37174  cbvabdavw  37175  cbvsbcdavw  37176  cbvsbcdavw2  37177  cbvdisjdavw  37187  cbvrmodavw2  37202  cbvreudavw2  37203  cbvdisjdavw2  37208  bj-nnfbi  37779  bj-cbvexdv  37842  bj-sbievw  37889  mobidvALT  37899  bj-axreprepsep  38133  bj-restuni  38160  bj-elid6  38234  cbveud  38438  cbvreud  38439  exrecfnlem  38445  wl-ifp-ncond2  38531  wl-ifpimpr  38532  wl-3xorbi123d  38541  wl-sb8eut  38653  wl-sb8eutv  38654  wl-sb8mot  38655  wl-sb8motv  38656  wl-clabtv  38661  wl-clabt  38662  wl-eujustlem1  38663  poimirlem17  38698  poimirlem19  38700  poimirlem20  38701  poimirlem25  38706  ftc1anclem5  38758  istotbnd3  38848  sstotbnd  38852  heibor  38898  isass  38923  isidlc  39092  smprngopr  39129  brvvdif  39343  elecALTV  39346  eqrel2  39380  dmecd  39385  relcnveq2  39404  eldmxrncnvepres  39509  eldmxrncnvepres2  39510  extssr  39664  elrefrelsrel  39675  refreleq  39676  elcnvrefrelsrel  39691  elrelscnveq2  39704  elsymrelsrel  39716  symreleq  39717  eltrrelsrel  39740  trreleq  39741  eleqvrelsrel  39753  eqvreleq  39761  redundpim3  39789  erALTVeq1  39829  elfunsALTVfunALTV  39857  eldisjsdisj  39899  eldisjeq  39916  disjsuc  39934  parteq1  39952  parteq2  39953  islshpsm  40180  lcvexchlem1  40234  opcon1b  40398  isat3  40507  glbconN  40577  cdleme32fva  41637  cdlemg2cex  41791  dibelval3  42347  dib1dim  42365  doch11  42573  dochsordN  42574  mapdordlem1a  42834  mapd11  42839  mapdsord  42855  mapdcnv11N  42859  mapd0  42865  sn-iotalem  43418  ricfld  43737  fimgmcyc  43741  fsuppind  43761  mrefg2  43861  jm2.23  44146  wepwsolem  44192  dnwech  44198  islssfg2  44216  gicabl  44244  onsupmaxb  44384  onsupeqnmax  44392  orddif0suc  44413  oadif1lem  44524  oadif1  44525  fzunt  44599  fzuntd  44600  fzunt1d  44601  fzuntgd  44602  ifpbi2  44611  ifpbi3  44612  ifpbi1  44621  ifpbi12  44632  ifpbi13  44633  ontric3g  44666  pwinfig  44705  inintabd  44723  cnvcnvintabd  44743  cnvintabd  44746  intimag  44799  briunov2  44825  heeq12  44919  sbcheg  44922  uneqsn  45168  ntrneineine0lem  45226  ntrneineine1lem  45227  ntrneik2  45235  ntrneix2  45236  ntrneik13  45241  ntrneix13  45242  ralbidar  45570  rexbidar  45571  trsbc  45665  cocan2g  46065  cocan1g  46067  relpeq1  46076  relpeq2  46077  relpeq3  46078  relpeq4  46079  relpeq5  46080  n0abso  46108  modelaxreplem3  46112  iindif2f  46317  rnmptpr  46334  iccintsng  46677  xlimres  46973  fsetsniunop  48261  fsetsnprcnex  48267  fcoresf1ob  48285  f1cof1b  48289  f1ocof1ob  48293  dfateq12d  48338  aov0nbovbi  48407  fnotaovb  48410  ichbidv  48677  sprsymrelf  48719  prprsprreu  48743  prprreueq  48744  nprmmul1  48751  edgusgrclnbfin  49082  dfclnbgr6  49096  dfnbgr6  49097  isubgredg  49106  gpgnbgrvtx0  49314  gpgnbgrvtx1  49315  rngcsectALTV  49514  ringcsectALTV  49548  lindslinindsimp2lem5  49716  xpco2  50110  opndisj  50159  i0oii  50176  io1ii  50177  iscnrm3lem2  50191  uobffth  50476  uobeqw  50477  thincpropd  50719  termcpropd  50780  alsbid  51115